Verify YM C316 diagonal Gram coercivity firewall

[stevemoraco]

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

Finite scope only:

• rank-one Gram family: full Gram quadratic form can vanish while the diagonal/local form remains positive;
• naive |C_ij|/C_ii row ratios are generator-rescaling dependent;
• squared normalized correlation coefficient is rescaling invariant;
• a positive Riesz/coercivity margin is sufficient to convert a diagonal-relative debt into a physical-Gram-relative debt.

Failed-first provenance is preserved as non-evidence:

run/job: 32332661943 / 96316141924
AXLE compiled the declarations but the strict workflow failed because three trailing tactics remained after `field_simp` had already closed their goals.

No theorem statement changed. The dead tactics were removed.

Clean repaired replay:

head: c957026f2d717591a3dc2c592f31508f54fa52c1
run/job: 32332692484 / 96316226805
source SHA-256: cac236862ce9f84ba6858edfd2993b376b27cadf7e678a13d2c2a5b0c9fc89b0
AXLE Lean: 4.30.0
okay: true
cached_response: false
failed declarations: []
Lean errors/warnings: [] / []
tool errors/warnings: [] / []
axiom union: {propext, Classical.choice, Quot.sound}
artifact: 9393560849
artifact ZIP SHA-256: 0cc9cebd3efc6a3f8bdf0f3a8ca85529953e3a92d1481e8e321a7a866b1d294f

This does not formalize the Faizal–Shabir Yang-Mills connected-correlation row, a localized Riesz frame, regulator/volume/depth uniformity, AF/IR identification, continuum OS reconstruction, a physical mass gap, or the Clay theorem.

FIVE-ALARM OFF.