Verify YM C292 coarse-frame dual operatorization

[stevemoraco]

Public guarded theorem-equivalent replay for RH-Lean C292.

Formalized scope only:

• naive reconstruction from matrix elements using the same non-normalized vector scales quartically under basis rescaling;
• concrete identity-operator witness gives 16 rather than 1 at basis vector 2;
• one-dimensional dual/Gram correction reconstructs the scalar operator exactly;
• corrected reconstruction is invariant under nonzero basis rescaling.

Failed-first provenance

Run/job 32276622126 / 96145462023 is non-evidence. AXLE reported no failed theorem declarations, but the definition dualReconstruction depended on real division and needed to be marked noncomputable; the strict workflow therefore failed on lean.dependsOnNoncomputable. No theorem statement changed.

The repaired exact source at head 205eaebeac4bf563ee3e81cb24c032a2b6eee818 passed run/job 32277011684 / 96146703660:

AXLE Lean 4.30.0
source SHA-256: bb46aac6825f3af0256261297be39dca5a21e2ee9ef2915840e2edca042857b2
okay: true
cached_response: true
failed declarations: []
Lean errors/warnings: [] / []
tool errors/warnings: [] / []
axiom union: {propext, Classical.choice, Quot.sound}
artifact: 9374375821
artifact ZIP SHA-256: e0ddd4da804686c4f6cc465b6c3d5c042904e1de9a4b6471bb0f6e78834d2039

This is finite real algebra only. It does not formalize OS Hilbert spaces, localized frames, inverse-Gram decay, a canonical support-masked mixed form, the Yang-Mills mixed operator, regulator/volume uniformity, AF/IR identification, continuum OS reconstruction, a physical mass gap, or the Clay theorem.

FIVE-ALARM OFF.