Verify YM C313 discrete two-loop invariant firewall

[stevemoraco]

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

Formalized scope only:

• exact counterterm-subtracted recurrence algebra;
• finite telescoping of the residual after subtracting one-loop drift and a declared correction channel;
• specialization to the harmonic two-loop channel B / h_n;
• two-trajectory invariant-difference step.

This does not identify the Yang-Mills two-loop coefficient, prove the post-two-loop residual summable, construct Lambda_YM, identify AF and IR, prove a mass gap, or formalize continuum OS reconstruction.

FIVE-ALARM OFF.