mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
zeekayandHanzo Dev
a94116d3ff
`HardnessAdvantage` was `opaque HardnessAdvantage : Type := Unit`. In a one-element type every advantage equals every other, so no bound of the form `adv ≤ a + b + c + d` is expressible — which is why `MagnetarTSUFBound` concluded `True` while its docstring described a four-way decomposition, and why `magnetar_tsuf` and `magnetar_tsuf_n_independent` established nothing. It is now a nonnegative quantity, ordered and additive. `MagnetarTSUFBound fp` is the sum of the four named advantages: SHAKE collision, SHAKE preimage, FIPS 205 EUF-CMA, and the aggregator-TCB caveat. It takes no `ThresholdParams`, which is the substance of n-independence — that theorem now follows from the bound's shape instead of re-wrapping its hypothesis. `magnetar_tsuf` is an axiom rather than a theorem, because that is what an unmechanised reduction is. `magnetar/PROOF-CLAIMS.md` §0 states "Magnetar has no mechanized proof of any threshold property"; this corpus was claiming one, so magnetar was the honest side of the disagreement. `magnetar_hardness_disjoint_from_lattice` was `(h : Bound) : Bound := h` — it returned its own hypothesis. Family disjointness quantifies over adversaries and reductions between problems, and this model has neither; the bound's freedom from lattice hardness is visible in its definition, so that is where it is stated. Three citations named `Crypto/Magnetar_MPC.lean` as the home of the mechanised GKMM 2024/447 reduction. No such file exists in any of the three proof repositories. They now point at `magnetar/PROOF-CLAIMS.md`, and the reference to `threshold/study/magnetar.md`, which is also absent, is gone. Zero Magnetar declarations are now reported as carrying no content, down from one; corpus total 62 to 61. Co-authored-by: Hanzo Dev <[email protected]>