rsPhysicalThesis_of_no_strip_zeros
plain-language theorem explainer
The theorem shows that the non-existence of Riemann zeta zeros with real part strictly between 1/2 and 1 implies the RS Physical Thesis holds vacuously. Researchers deriving the Riemann Hypothesis from Recognition Science arithmetic would cite it to eliminate the need for explicit physical recognition events when the strip is empty. The proof is a direct term-mode reduction that assumes a zero and applies falsehood elimination to the input hypothesis.
Claim. If the Riemann zeta function has no zeros satisfying $1/2 < {Re}(ρ) < 1$, then every nontrivial zero $ρ$ in that strip corresponds to a physical recognition event, i.e., PhysicallyExists holds for the associated zeta defect sensor.
background
The RS Physical Thesis is defined in ZetaLedgerBridge as the single non-mechanical ingredient of the Recognition Science argument for the Riemann Hypothesis. It asserts that every nontrivial zero of riemannZeta in the critical strip corresponds to a physical recognition event on the arithmetic ledger, so the associated zetaDefectSensor must satisfy PhysicallyExists. The module replaces the opaque RSPhysicalThesis dependency with a structured bundle of the exact ingredients needed for the RH proof.
proof idea
The proof is a term-mode proof. It introduces the variables for a supposed zero ρ together with the zero and strip hypotheses, then applies False.elim directly to the input hypothesis that no such zero exists.
why it matters
This result bridges the no-strip-zeros assumption to the RS Physical Thesis and is invoked by rsPhysicalThesis_of_data to obtain the thesis from decomposed data. It fills the §3 bridge in ZetaLedgerBridge from the arithmetic ledger to physical recognition events, supporting the overall Recognition Science chain toward the Riemann Hypothesis. It touches the open question of whether the physical thesis can be fully discharged by data or remains an interface hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.