Verify YM C310 coherent shooting trajectory firewall

[stevemoraco]

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

Formalized scope only:

• two affine center functions can have the same small reference-value scale and the same exact linear-response scale while their tuned roots remain order-one separated;
• a finite-depth shooting root is quantitatively localized near a coercive limiting shooting zero whenever the finite-depth and limiting shooting functions are uniformly close at that root.

This is the finite firewall behind C310's source result that per-depth entry roots at the Appendix-A scale do not by themselves define a coherent bare-coupling trajectory. It does not formalize the Yang-Mills Banach RG, uniform shooting-function convergence/simple-zero theorem, AF/IR identity, continuum OS reconstruction, or a mass gap.

Guarded replay

qs head: fec6522f17ec77e613188554740dee76a914962a
run/job: 32308898598 / 96247584148
AXLE Lean: 4.30.0
source SHA-256: 39ca3571924e126251a645a829924b65e465d1118ebdbb07ac431b5cdbe6171b
okay: true
cached_response: true
failed declarations: []
Lean errors/warnings: [] / []
tool errors/warnings: [] / []
axiom union: {propext, Classical.choice, Quot.sound}
artifact: 9385701052
artifact ZIP SHA-256: 1d3a3bc4f80e889f86b469ea0608ac23de2a31ab8d960a436506246259bc7bd5

FIVE-ALARM OFF.