Verify YM C266 O4 Riemann normalization firewall

[stevemoraco]

Public exact-source verifier for RH-Lean C266.

The mirrored Lean file proves only the finite arithmetic firewall behind the Appendix Proposition 4.6 audit: a four-dimensional lattice-counting factor a^-4 multiplied by an O(a) continuum integral has scale a^-3, together with a dyadic witness. It does not formalize O(4) restoration, OS reconstruction, Yang–Mills, a mass gap, or a Clay theorem.

The workflow rejects sorry, admit, sorryAx, custom axioms, unsafe/native-decide shortcuts, and fails on any AXLE Lean error or warning.

Clean guarded replay

verified head: 34e9754a4c665f291fd8477e1658c5b4f628f00d
run/job: 32216899901 / 95960004745
AXLE: Lean 4.30.0
source SHA-256: 3bdafe6b3f7631291c34cdd07f0aad49afdbb63ee85c9bef163a30a4856643f6
okay: true
cached_response: true
failed declarations: []
Lean errors/warnings: [] / []
tool errors/warnings: [] / []
axiom union: {propext, Classical.choice, Quot.sound}
artifact: 9352631783
artifact ZIP SHA-256: 8a4715c809961a6e6d4b70f9f6deff626c2bce73dcef56d1f5d8101543e17fb9

The cached status is explicitly disclosed. FIVE-ALARM OFF.