no_strip_zeros_of_decomposed_data
plain-language theorem explainer
Given the decomposed RSPhysicalThesisData bundle, the Riemann zeta function has no zeros with real part strictly between 1/2 and 1. Researchers deriving the Riemann hypothesis inside Recognition Science cite this to close the arithmetic ledger side of the argument. The proof instantiates a DefectSensor from the hypothetical zero, extracts nonzero charge to obtain CostDivergent, and reaches contradiction via the boundary transport certificate.
Claim. Let $D$ be an instance of the decomposed data bundle. Then for every complex number $ρ$, if the Riemann zeta function satisfies $ζ(ρ)=0$ and $1/2 < Re(ρ) < 1$, a contradiction follows.
background
RSPhysicalThesisData is the explicit structure bundling prime ledger certificate, Euler ledger partition certificate, completed zeta ledger certificate, argument principle sensor certificate, Euler realizable ledger certificate, boundary transport certificate, and T1 boundary exclusion certificate. The module replaces the single opaque RSPhysicalThesis proposition (which required every nontrivial zero in the strip to correspond to a physical recognition event, hence PhysicallyExists on its DefectSensor) with this concrete bundle of arithmetic and physical certificates.
proof idea
The tactic proof assumes a zero ρ together with the strip bounds. It builds the sensor via zetaDefectSensor at ρ.re with the given interval and multiplicity 1. It obtains nonzero charge from zetaDefectSensor_charge_ne_zero, derives CostDivergent via nonzero_charge_cost_divergent, and applies no_cost_divergent_sensor_of_boundary_transport to the boundaryTransport field of the data and the sensor to reach falsehood.
why it matters
This theorem shows that the decomposed data implies absence of right-half strip zeros, which makes the original RSPhysicalThesis hold vacuously. It is invoked by rsPhysicalThesis_of_data to recover the old interface from the new data bundle. In the Recognition Science framework it advances the physical thesis decomposition by using boundary transport to exclude right-half zeros, consistent with the forcing chain and the replacement of the single non-mechanical ingredient by explicit certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.