Skip to content

A slot left free absorbs the data, and the relation cannot fail - #164

Open
sotashimozono wants to merge 1 commit into
mainfrom
fix/free-slots-are-not-checks
Open

sotashimozono wants to merge 1 commit into
mainfrom
fix/free-slots-are-not-checks

Conversation

@sotashimozono

Copy link
Copy Markdown
Member

Five relations 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; π²/3 appears nowhere in it.

The Lorenz number is a constant

L0 now defaults to π²/3, so omitting it tests the law. Supplying it is still allowed (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. solve-for-L0 is untouched: extracting that ratio from a measurement is the honest use. MottFormula, which hardcodes π²/3, was the exemplar already in the file.

The statistics sign takes two values

ζ = G^</(e^{−βω} G^>) zeroes the residual for every pair, so the KMS condition could never fail. Refused outside {+1,−1}. The condition still bites at a legal ζ, 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 holds out of equilibrium by construction. What was absent is the claim that makes it a theorem. The package already had keldysh_distribution, whose own docstring says it is "the function multiplying the spectral weight in the FDT" — and no relation used it.

KeldyshFDT KeldyshDistributionEquilibrium (new)
equilibrium true true
non-equilibrium true false
wrong statistics declared n/a false

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, and what it costs

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.

What I could not establish

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.

🤖 Generated with Claude Code

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^</(e^{-βω} 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) <noreply@anthropic.com>
@github-actions

Copy link
Copy Markdown
Contributor

📚 Docs preview: https://qatlashub.github.io/AbstractQAtlas.jl/previews/PR164/

(updates on each push to this PR)

@codecov

codecov Bot commented Sep 16, 2026

Copy link
Copy Markdown

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant