Corona is Module-LWE (threshold-Raccoon/Ringtail), NOT Ring-LWE. Confirmed in code: sign/sign.go samples A in R_q^{8x7} (sign.go:87 SamplePolyMatrix M=8,N=7), secret s a rank-7 ring vector, b=A*s+e (sign.go:106-107) over R_q=Z_q[X]/(X^256+1) (LogN=8), q=0x1000000004A01 -- rank>1 module structure, not rank-1 ring-LWE. threshold/threshold.go:4-5 already said Module-LWE.
Fixed the family label across README, SPEC, SUBMISSION, NIST-SUBMISSION, PATENTS, LLM, CONTRIBUTING, SECURITY, CHANGELOG, DEPLOYMENT-RUNBOOK, Makefile, AXIOM-INVENTORY, PROOF-CLAIMS, BLOCKERS, CRYPTOGRAPHER-SIGN-OFF, FIPS-TRACEABILITY, TRUSTED-COMPUTING-BASE, AUDIT-2026-05/06, docs/mptc/*, jasmin/README, 3 Go comments + cli help string.
Also corrected the downstream false claim that Corona (Ring-LWE) and Pulsar (Module-LWE) are 'different lattice families' giving 'structural/family diversity': both are Module-LWE, so the Double-Lattice defense is construction/implementation diversity (threshold-Raccoon vs ML-DSA), not hardness-family diversity; a Module-LWE break affects both legs (hash-based Magnetar is the assumption-diversifier). Fixed companion R-SIS -> Module-SIS where it was the module scheme's SIS assumption; added the Langlois-Stehle (DCC 2015) Module-LWE citation alongside LPR 2010.
Delicate artifacts: proof identifiers (rlwe_sign_op, RLWE_Functional theory/file, *_eq_rlwe bridges, CentralRLWESign, RLWESign, rlwe_compute_*) were NOT renamed -- EasyCrypt/jasmin toolchains are absent here so a rename cannot be compile-verified, and .assurance/ gates parse those names. Added clarifying naming notes to the 5 prominent .ec files, proofs/easycrypt/README.md, AXIOM-INVENTORY.md, and jasmin/rlwe/sign.jazz. .assurance/*.txt left untouched (already say Module-LWE/Module-SIS; rlwe tokens are gate-parsed identifiers). Left AUDIT-2026-06.md:463 historical rename-log and the ProtoStar-LWE paper-title substring untouched.
go build ./... and go test ./... green (GOWORK=off; all packages ok).
The EC byte-equality (corona_n1_byte_equality) proved the threshold combine
bit-equals CombineAbs, whose sign_abs_op_lifted_eq_rlwe bridge pins it to
rlwe_sign_op on the LAGRANGE-RECONSTRUCTED master secret -- exactly the path
the Boschini/Raccoon production combine must never take (CORONA-EC-RECON-MODEL).
This pass re-scopes that cone as IDEALISED CORRECTNESS and adds the HONEST
production model whose residual is a STANDARD Module-LWE/MSIS reduction.
New proofs/easycrypt/Corona_N1_NoLeak.ec (written; machine-recheck pending
EasyCrypt -- no `ec` on host, scripts/checks/ec-compile.sh is the CI gate):
- mask_telescope_zero [B, Lean-backed]: Sum_i (maskPrime_i - mask_i) = 0 --
the pairwise-PRF masks (z_i = R_i*u + maskPrime_i + c*lambda_i*s_i - mask_i)
are the same double sum reindexed (Fubini), so they cancel on aggregation.
Machine-checked in Lean as pairwise_mask_telescopes.
- no_leak_z_aggregate: the surviving aggregate is R*u + c*s by Lagrange-at-0
WITHOUT forming the master secret and with no per-party c*s_i ever exposed.
- no_leak_reduction [C-standard, OPEN]: under Module-LWE + Module-SIS the
public transcript leaks nothing about s beyond one Boschini signature. The
honest replacement for sign_abs_op_lifted_eq_rlwe -- a reduction to the SAME
substrate AXIOM-INVENTORY.md §1 already lists, secret NEVER reconstructed.
The CORRECTNESS CORE is machine-checked in Lean 4 + Mathlib on this host
(luxfi/proofs: Crypto.Corona.NoLeakAggregate / Threshold_Lagrange; lake build
green, #print axioms shows no sorryAx).
Disclosure updated to match reality: AXIOM-INVENTORY (new Bucket C-standard +
"A is machine-checked in Lean"), PROOF-CLAIMS (two models, §0 Disclosure 1),
BLOCKERS (CORONA-EC-RECON-MODEL re-scoped, first criterion now [x]), budget
AXIOM 56->58. Framework gate PASS (all 5 checks); go build + full test suite green.
5-axiom Lean-to-EasyCrypt correspondence for Corona, mirroring Pulsar's
structure:
lagrange_inverse_eval (Corona_N1.ec)
-> Crypto.Corona.Shamir.shamir_correct_at_target
threshold_partial_response_identity (Corona_N1.ec)
-> Crypto.Threshold.Lagrange.threshold_partial_response_identity
add_share_zeroR (Corona_N4.ec)
-> Mathlib AddCommMonoid instance
reconstruct_linear (Corona_N4.ec)
-> Crypto.Threshold.Lagrange.combine_distributes_over_sum
shamir_correct (Corona_N4.ec)
-> Crypto.Corona.Shamir.shamir_correct_at_target
CI guard `scripts/check-lean-bridge.sh` verifies for every EC axiom
that (1) the axiom still exists as `axiom` (not silently demoted to
`lemma`), (2) it carries an inline citation comment naming the Lean
theorem, (3) the Lean theorem still exists at the named path. It also
checks that every EC file mentioned in the bridge doc exists on disk.
Auto-detects the Lean repo at ~/work/lux/proofs/lean or sibling
locations. Skips Lean-side existence checks if no Lean repo is on disk.
Mirrors ~/work/lux/pulsar/scripts/check-lean-bridge.sh exactly.
zeekay