From b3df1753c76901a8ec34bffd49627541fd9e738c Mon Sep 17 00:00:00 2001 From: sotashimozono Date: Wed, 16 Sep 2026 05:57:41 +0000 Subject: [PATCH] A slot left free absorbs the data, and the relation cannot fail MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Five relations in the registry pass for any input, because a value the physics fixes is written as a caller-supplied slot with nothing pinning it. Measured before the fix: | relation | free slot | should be | passed with | |---|---|---|---| | WiedemannFranz | L0 | π²/3 = 3.2899 | 3289.87, and -3.29 (negative κ) | | RighiLeduc | L0 | π²/3 | 3.29e6 | | KMSGreaterLesser | ζ | +1 or -1 only | 7.3 | | KeldyshFDT | h | coth(βω/2) in equilibrium | 0.017, fully non-equilibrium | | SelfEnergyKeldyshFDT | h | the same | the same | `WiedemannFranz`'s docstring claimed the ratio was "checked against the Sommerfeld constant". The kernel is `κ - L0*σ*T` and π²/3 appears nowhere in it. THE LORENZ NUMBER IS A CONSTANT `L0` now defaults to π²/3, so omitting it tests the law: a material off by 1000, or with negative thermal conductivity, fails. Supplying it is still allowed, because a non-Fermi liquid does have its own Lorenz number, and the docstring now says what a self-derived `L0` is worth instead of claiming a check it never made. Solving FOR `L0` is untouched: extracting that ratio from a measurement is the honest use. `MottFormula`, which hardcodes π²/3, was the exemplar. `RighiLeduc`'s `L0` moves last to carry the default. Relations are called by keyword, so the order is not a caller-visible break; `variables()` no longer lists `L0` for either, matching how `FSumRule`'s `N=1` already behaved. THE STATISTICS SIGN TAKES TWO VALUES `ζ` names the exchange statistics. Left free it absorbs any ratio, since `ζ = G^)` zeroes the residual for every pair. Refused outside {+1,-1}. The condition still bites at a legal ζ: a pair off the KMS ratio fails, which is what says the guard did not swap one tautology for another. THE FDT WAS MISSING ITS OTHER HALF `GK - h*(GR-GA)` is not wrong: it is the definition of `h`, and it holds out of equilibrium by construction. What was absent is the claim that makes it a theorem, `h = coth(βω/2)` (bosonic) or `tanh(βω/2)` (fermionic). The package already had `keldysh_distribution` and its docstring already said it is "the function multiplying the spectral weight in the FDT"; no relation used it. `KeldyshDistributionEquilibrium` is that half, and it fails on a non-equilibrium `h`, on a sign-flipped one, and on a declared statistics that does not match. `SelfEnergyKeldyshFDT` shares the same `h`, so one relation covers both. Mutation, against test/relations/test_free_slots.jl (27 assertions): | mutation | assertions failed | |---|---| | remove WiedemannFranz's default (the bug above) | 3 | | RighiLeduc's constant set to 1.0 | 1 | | the statistics guard never fires | 2 | | KeldyshDistributionEquilibrium made vacuous | 5 | Breaking, so 0.7.17 -> 0.8.0: `variables()` changes for two relations and a previously accepted ζ is refused. The three in-tree dependents pin 0.6.x/0.7 and none of them call any of the five. Four mechanical sweeps for other instances all failed. The broad one returned 37 with mostly false positives; the tightened one returned 18 of which 14 were false positives AND it missed the two confirmed `L₀` cases, because the docstrings write the subscript `L₀` while the slot is `L0`. All five were found by reading. There is no basis here for claiming the registry holds no others. Co-Authored-By: Claude Opus 5 (1M context) --- Project.toml | 2 +- src/relations/keldysh.jl | 47 ++++++++++++++++- src/relations/transport.jl | 24 ++++++--- test/relations/test_free_slots.jl | 88 +++++++++++++++++++++++++++++++ test/relations/test_interface.jl | 4 +- test/relations/test_keldysh.jl | 6 ++- test/relations/test_transport.jl | 6 ++- 7 files changed, 162 insertions(+), 15 deletions(-) create mode 100644 test/relations/test_free_slots.jl diff --git a/Project.toml b/Project.toml index ac7bcb2c..697f0640 100644 --- a/Project.toml +++ b/Project.toml @@ -1,6 +1,6 @@ name = "AbstractQAtlas" uuid = "dcea2817-62f8-4a75-b498-1b50a9ed1e4d" -version = "0.7.17" +version = "0.8.0" authors = ["sota shimozono "] [deps] diff --git a/src/relations/keldysh.jl b/src/relations/keldysh.jl index 48c9f283..e4cbee83 100644 --- a/src/relations/keldysh.jl +++ b/src/relations/keldysh.jl @@ -65,6 +65,21 @@ Variables: `GA`, `GR`. (Complex-valued residual.) GA::AdvancedGreensFunction, GR::RetardedGreensFunction ) = GA - conj(GR) +# `ζ` names the exchange statistics, so it takes two values and no others. Left +# unconstrained it absorbs whatever ratio the data happens to have: setting it to +# `G^)` zeroes the residual for any pair, so the KMS condition can +# never fail and a pass reports nothing. Measured before this guard: ζ = 7.3 passed. +function _require_statistics_sign(what::Symbol, ζ) + ζ == 1 || + ζ == -1 || + error( + "$what: ζ is the exchange-statistics sign, +1 (bosonic) or -1 (fermionic); " * + "got $ζ. A free ζ makes the residual vanish for any G^≷ pair, so the " * + "condition would pass without being tested.", + ) + return nothing +end + """ KeldyshFDT <: AbstractRelation @@ -79,12 +94,39 @@ with `h = coth(βω/2)` (bosons) or `tanh(βω/2)` (fermions), supplied by dissipation (`G^R − G^A ∝ Im G^R`) on the right — the two are not independent in thermal equilibrium. +Supplied-`h` convention, and the caveat that comes with it: `h` here is whatever +the caller says the distribution is, so this tests the FDT only when `h` was +obtained independently. Setting `h = G^K/(G^R − G^A)` zeroes the residual for +ANY state, a fully non-equilibrium one included, since that is the definition of +`h` rather than a law about it. [`KeldyshDistributionEquilibrium`](@ref) is the +half this one does not carry: it pins `h` to `keldysh_distribution`, and the two +together are the theorem. + Variables: `GK`, `h`, `GR`, `GA`. """ @relation :keldysh KeldyshFDT( GK::KeldyshGreensFunction, h, GR::RetardedGreensFunction, GA::AdvancedGreensFunction ) = GK - h * (GR - GA) +""" + KeldyshDistributionEquilibrium <: AbstractRelation + +The equilibrium value of the Keldysh distribution function, + +`h(ω) = coth(βω/2)` (bosonic) or `tanh(βω/2)` (fermionic), + +i.e. [`keldysh_distribution`](@ref) written as a relation so a supplied `h` can +be checked rather than assumed. + +[`KeldyshFDT`](@ref) alone cannot do this. It reads `h` as given, so it holds out +of equilibrium by construction; this one is what makes "the system is thermal" a +falsifiable claim about the same `h`. + +Variables: `h`, `ω`, `β` (or `T`), `stat` ([`Fermionic`](@ref) / [`Bosonic`](@ref)). +""" +@relation :keldysh KeldyshDistributionEquilibrium(h, ω, β::InverseTemperature, stat) = + h - keldysh_distribution(stat, ω; β=β) + """ KMSGreaterLesser <: AbstractRelation @@ -104,7 +146,10 @@ Variables: `Gles`, `Ggtr`, `ζ`, `ω`, and `β` (or `T`). """ @relation :keldysh KMSGreaterLesser( Gles::LesserGreensFunction, Ggtr::GreaterGreensFunction, ζ, ω, β::InverseTemperature -) = Gles - ζ * exp(-β * ω) * Ggtr +) = begin + _require_statistics_sign(:KMSGreaterLesser, ζ) + Gles - ζ * exp(-β * ω) * Ggtr +end """ SpectralFromKeldysh <: AbstractRelation diff --git a/src/relations/transport.jl b/src/relations/transport.jl index eb30f9c8..7a8e80fd 100644 --- a/src/relations/transport.jl +++ b/src/relations/transport.jl @@ -31,14 +31,18 @@ conductivity is the temperature times the Lorenz number, `κ = L₀ · σ · T`, with the Sommerfeld value `L₀ = π²/3` (in units `k_B = e = 1`; i.e. -`π²k_B²/3e²`). A diagonal-component statement (`κ_xx`, `σ_xx`); the ratio -`κ/(σT)` is the caller-supplied Lorenz number `L0`, checked against the -Sommerfeld constant. +`π²k_B²/3e²`), which is `L0`'s DEFAULT: omit it and this tests the law. -Variables: `κ`, `σ`, `T`, `L0`. +Supplying `L0` does not test the law, it asserts a different Lorenz number, as a +non-Fermi liquid has. Supplying `κ/(σT)` in particular makes the residual zero +for any material, including one whose thermal conductivity is negative, so a +pass there says nothing. Solving FOR `L0` is the honest way to get that ratio +out of a measurement. + +Variables: `κ`, `σ`, `T`, `L0` (default `π²/3`). """ @relation :transport WiedemannFranz( - κ::ThermalConductivity{(:x, :x)}, σ::Conductivity{(:x, :x)}, T::Temperature, L0 + κ::ThermalConductivity{(:x, :x)}, σ::Conductivity{(:x, :x)}, T::Temperature, L0=π^2 / 3 ) = κ - L0 * σ * T """ @@ -236,12 +240,16 @@ conductivities obey the Wiedemann–Franz law in the transverse channel, `κ_xy = L₀ · T · σ_xy`, -the off-diagonal companion of [`WiedemannFranz`](@ref) (`L₀ = π²/3`). +the off-diagonal companion of [`WiedemannFranz`](@ref); `L0` defaults to the +same Sommerfeld `π²/3`, and supplying it carries the same caveat. -Variables: `κxy`, `L0`, `T`, `σxy`. +Variables: `κxy`, `T`, `σxy`, `L0` (default `π²/3`). """ @relation :transport RighiLeduc( - κxy::ThermalConductivity{(:x, :y)}, L0, T::Temperature, σxy::Conductivity{(:x, :y)} + κxy::ThermalConductivity{(:x, :y)}, + T::Temperature, + σxy::Conductivity{(:x, :y)}, + L0=π^2 / 3, ) = κxy - L0 * T * σxy """ diff --git a/test/relations/test_free_slots.jl b/test/relations/test_free_slots.jl new file mode 100644 index 00000000..a7bb94fa --- /dev/null +++ b/test/relations/test_free_slots.jl @@ -0,0 +1,88 @@ +# A slot left free absorbs the data, and the relation then cannot fail. +# +# Each case below was MEASURED passing before the fix, on inputs that violate the +# law by orders of magnitude. The pattern is the registry's own: a value the +# physics fixes (a universal constant, a two-valued label, an equilibrium +# distribution) written as a caller-supplied slot with nothing pinning it. + +using AbstractQAtlas +using Test: @test, @test_throws, @testset + +const L_SOMMERFELD = π^2 / 3 + +why(f) = + try + f() + "" + catch e + sprint(showerror, e) + end + +@testset "the Lorenz number is a constant, so omitting it tests the law" begin + σ, T = 2.0, 300.0 + obeys = L_SOMMERFELD * σ * T + # Omitted: the default IS the law, so a material off by 1000 fails. + @test check(WiedemannFranz(); κ=obeys, σ=σ, T=T) + @test !check(WiedemannFranz(); κ=1000 * obeys, σ=σ, T=T) + @test !check(WiedemannFranz(); κ=(-obeys), σ=σ, T=T) # negative κ is not a metal + # Supplied: still accepted, because a non-Fermi liquid has its own Lorenz + # number. The docstring says so, and says what a self-derived L0 is worth. + @test check(WiedemannFranz(); κ=1000 * obeys, σ=σ, T=T, L0=1000 * L_SOMMERFELD) + # Solving FOR it is the honest way to get the ratio out of a measurement. + @test solve(WiedemannFranz(), Val(:L0); κ=obeys, σ=σ, T=T) ≈ L_SOMMERFELD + + xy = L_SOMMERFELD * T * 0.5 + @test check(RighiLeduc(); κxy=xy, T=T, σxy=0.5) + @test !check(RighiLeduc(); κxy=1e6 * xy, T=T, σxy=0.5) +end + +@testset "the statistics sign takes two values, so a third is refused" begin + β, ω, Ggtr = 1.0, 2.0, 1.0 + kms(ζ) = + check(KMSGreaterLesser(); Gles=ζ * exp(-β * ω) * Ggtr, Ggtr=Ggtr, ζ=ζ, ω=ω, β=β) + @test kms(+1) + @test kms(-1) + # Free, ζ absorbs any ratio: `ζ = G^)` zeroes the residual for + # every pair, so the KMS condition could never fail. 7.3 passed before this. + @test occursin("exchange-statistics sign", why(() -> kms(7.3))) + @test occursin("pass without being tested", why(() -> kms(0))) + # And the condition itself still bites: a pair off the KMS ratio fails at a + # legal ζ, which is what says the guard did not simply replace one tautology + # with another. + @test !check( + KMSGreaterLesser(); Gles=5.0 * exp(-β * ω) * Ggtr, Ggtr=Ggtr, ζ=1, ω=ω, β=β + ) +end + +@testset "the FDT needs the half that pins h" begin + β, ω = 1.0, 2.0 + GR, GA = 1.0 + 2.0im, 1.0 - 2.0im + for stat in (Bosonic(), Fermionic()) + h_eq = keldysh_distribution(stat, ω; β=β) + # `KeldyshFDT` reads h as given, so it holds for ANY state. That is not a + # defect to fix in it: `G^K = h(G^R-G^A)` is the definition of h. + for h in (h_eq, 0.017, -h_eq) + @test check(KeldyshFDT(); GK=h * (GR - GA), h=h, GR=GR, GA=GA) + end + # The claim "this system is thermal" lives in the other half, and it fails. + eq(h) = + check(KeldyshDistributionEquilibrium(); h=h, ω=ω, β=β, stat=stat, atol=1e-10) + @test eq(h_eq) + @test !eq(0.017) + @test !eq(-h_eq) + # The self-energy mirror shares the same h, so one relation covers both. + ΣR, ΣA = 0.3 + 0.7im, 0.3 - 0.7im + @test check( + SelfEnergyKeldyshFDT(); SigmaK=h_eq * (ΣR - ΣA), h=h_eq, SigmaR=ΣR, SigmaA=ΣA + ) + end + # Bosonic and fermionic h differ, so declaring the wrong statistics is caught. + @test !check( + KeldyshDistributionEquilibrium(); + h=keldysh_distribution(Bosonic(), ω; β=β), + ω=ω, + β=β, + stat=Fermionic(), + atol=1e-10, + ) +end diff --git a/test/relations/test_interface.jl b/test/relations/test_interface.jl index 9b3f0412..e3aae0e7 100644 --- a/test/relations/test_interface.jl +++ b/test/relations/test_interface.jl @@ -18,14 +18,14 @@ AbstractQAtlas.domain(::_NonAffineDemo) = :test_only # domain that has no line here shows up as a mismatch in this number alone. # Universal-only: the model-specific relations (spin glass, Drude mobility, # single-band Hall) live in QAtlas. - @test length(rels) == 173 + @test length(rels) == 174 @test allunique(typeof.(rels)) @test length(all_relations(; domain=:scaling)) == 33 # +ActivatedDynamicalScaling, ActivatedFiniteSizeScaling, +14 Appendix-A scaling types, +WeinribHalperinExponent, +QuantumHyperscaling; +TypicalCorrelationLength, GriffithsExponentDivergence, GriffithsSusceptibility, GriffithsSpecificHeat, ActivatedMomentGrowth; +CriticalCorrelationDecay, ActivatedCriticalCorrelation (#158); +3 self-averaging @test length(all_relations(; domain=:thermodynamic)) == 15 @test length(all_relations(; domain=:fundamental)) == 9 # +GrandPotentialLegendre, ParticleNumberResponse (grand-canonical); +ElectricCurrentResponse (j = −∂H/∂A) @test length(all_relations(; domain=:topology)) == 3 @test length(all_relations(; domain=:spectral)) == 15 # +MassGapPositivity - @test length(all_relations(; domain=:keldysh)) == 15 + @test length(all_relations(; domain=:keldysh)) == 16 # +KeldyshDistributionEquilibrium: the half that pins h @test length(all_relations(; domain=:transport)) == 18 @test length(all_relations(; domain=:quantum)) == 18 # +VelocityPositivity # +LoschmidtRate (λ = −log L / N); +7 of the 8 universal bounds @test length(all_relations(; domain=:holographic)) == 1 # BekensteinEntropyBound — the one non-quantum universal bound diff --git a/test/relations/test_keldysh.jl b/test/relations/test_keldysh.jl index 6c5cd674..b94a909a 100644 --- a/test/relations/test_keldysh.jl +++ b/test/relations/test_keldysh.jl @@ -290,6 +290,8 @@ end @testset "Keldysh relations register under :keldysh" begin # 6 equilibrium RAK + 4 Langreth + KineticLesser (#101) + 4 non-equilibrium (#64): - # SelfEnergyKeldyshFDT, KeldyshKineticGreater, NonequilibriumDistribution, TwoTerminalDistribution - @test length(all_relations(; domain=:keldysh)) == 15 + # SelfEnergyKeldyshFDT, KeldyshKineticGreater, NonequilibriumDistribution, + # TwoTerminalDistribution + KeldyshDistributionEquilibrium, which pins the `h` + # that KeldyshFDT reads as given. + @test length(all_relations(; domain=:keldysh)) == 16 end diff --git a/test/relations/test_transport.jl b/test/relations/test_transport.jl index c240394c..d69cad3b 100644 --- a/test/relations/test_transport.jl +++ b/test/relations/test_transport.jl @@ -71,7 +71,11 @@ end @test domain(WiedemannFranz()) == :transport @test domain(OpticalSumRule()) == :transport @test domain(CurrentNoiseFDT()) == :transport - @test variables(WiedemannFranz()) == (:κ, :σ, :T, :L0) + # `L0` carries the Sommerfeld default, and a defaulted slot is not a variable + # a caller must supply, the same as `FSumRule`'s `N=1`. + @test variables(WiedemannFranz()) == (:κ, :σ, :T) + @test solve(WiedemannFranz(), Val(:L0); κ=π^2 / 3, σ=1.0, T=1.0) ≈ π^2 / 3 + @test variables(RighiLeduc()) == (:κxy, :T, :σxy) @test variables(MottFormula()) == (:S, :dlnσ_dε, :T) @test variables(KelvinRelation()) == (:Π, :S, :T) end