zeroInducedBridge_iff_no_strip_zeros
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove or disprove the Riemann hypothesis.
- Does not construct or locate any specific zeta zeros.
- Does not apply to zeros with real part exactly 1/2 or outside (0,1).
- Does not generalize beyond the Riemann zeta function.
Lean usage
rw [zeroInducedBridge_iff_no_strip_zeros]formal statement (Lean)
137theorem zeroInducedBridge_iff_no_strip_zeros :
138 ZeroInducedProxyPhysicalizationBridge ↔
139 (∀ ρ : ℂ, riemannZeta ρ = 0 → 1/2 < ρ.re → ρ.re < 1 → False) := by
proof body
Term-mode proof.
140 constructor
141 · intro hzipb ρ hzero hlo hhi
142 exact not_proxyPhysicalizationBridge_of_charge_ne_zero
143 (zetaDefectSensor ρ.re ⟨hlo, hhi⟩ 1)
144 (zetaDefectSensor_charge_ne_zero ρ.re ⟨hlo, hhi⟩)
145 (hzipb ρ hzero hlo hhi)
146 · intro hno ρ hzero hlo hhi
147 exact (hno ρ hzero hlo hhi).elim
148
149/-- Mathlib's `RiemannHypothesis` implies `ZeroInducedProxyPhysicalizationBridge`.
150Any strip zero would violate `Re(ρ) = 1/2`, so the bridge holds vacuously. -/