zeroInducedBridge_iff_no_strip_zeros
plain-language theorem explainer
The zero-induced proxy physicalization bridge holds exactly when the Riemann zeta function has no zeros with real part strictly between one half and one. Researchers linking Recognition Science physicalization to the Riemann hypothesis cite this to equate the bridge condition with the classical absence of strip zeros. The term-mode proof splits the biconditional and invokes the nonzero-charge failure lemma together with the sensor charge lemma in the forward direction.
Claim. The proposition that every strip zero of the Riemann zeta function induces a defect sensor for which the proxy physicalization bridge holds is equivalent to the statement that the Riemann zeta function has no zeros $ρ$ satisfying $1/2 < Re(ρ) < 1$.
background
This declaration sits in the Proxy Physicalization Bridge module, which addresses the remaining transport from the bounded proxy state in PhysicallyRealizableLedger to the PhysicallyExists predicate defined via eulerLedgerScalarState. The zero-induced bridge is the universal statement over all complex zeros of zeta in the critical strip, requiring the proxy bridge for each associated charge-one defect sensor constructed by zetaDefectSensor. Upstream, the classical bridge packs models into CPMBridge structures, while zetaDefectSensor builds the sensor from real part and strip bounds, and the failure theorem shows the proxy bridge cannot hold for nonzero charge sensors.
proof idea
Constructor splits the equivalence into two implications. Forward: given the bridge and a strip zero at rho, instantiate the sensor with charge one, apply the charge nonzero theorem to obtain the failure of the proxy bridge, then contradict the assumed bridge instance. Reverse: given no strip zeros, the antecedent is false so the implication holds by elimination.
why it matters
It supplies the key equivalence used by zeroInducedBridge_iff_rh to identify the zero-induced bridge with the Riemann hypothesis. The module documentation notes that supplying this bridge for zeta-zero sensors yields the RS Physical Thesis. Within the Recognition Science framework it closes the reduction of the physicalization gap precisely to the classical Riemann hypothesis, confirming that the directed Euler ledger infrastructure isolates exactly that gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.