Verify RH Run10bzEC Bezout two-lift core

[stevemoraco]

Public guarded replay for RH-Lean #2201 / RH #2012.

The flattened source verifies only the finite integer algebra of the reduced two-band system: exact Bezout two-lift parameterization, converse, recovery, and determinant identity D=h(t+u).

Final guarded replay:

run/job: 32257047665 / 96081057377
head source commit: 825136bc64813fe22a46fc19fbe7d46b4df8bbca
Lean environment: 4.30.0
source SHA-256: a8c77d5856776d585e25486722fe4d26ecf860ef0fb7878a629e2e2869f61181
okay: true
failed declarations: []
Lean errors/warnings: [] / []
tool errors/warnings: [] / []
axiom union: {propext, Classical.choice, Quot.sound}
request id: 38f0312e-3b7d-4e4c-9360-953c619b6f6c
cached_response: true
artifact: 9366687381
artifact ZIP SHA-256: be29d7c2f17c8f1e69dcf00fe88e1edebffe372ab035314b0a334f1633c8ed76

Failed-first runs are preserved as non-evidence: run 32256704538 exposed redundant proof-script tactics; run 32256937369 exposed the complementary calc-step mistake. The theorem statement did not change. The repaired source above passed the strict no-hole/no-custom-axiom wrapper.

It does not formalize Heath--Brown identities, source band boxes, signed-residue dispersion, Suzuki's criterion, zeta, or RH.

FIVE-ALARM OFF.