rh_from_ontological_dichotomy
plain-language theorem explainer
If every defect sensor physically exists then every sensor has charge zero. Researchers unifying the Riemann hypothesis with Recognition Science cite this as the physical-to-arithmetic direction of the equivalence. The proof is a one-line term application of the mpr direction of the ontological dichotomy theorem.
Claim. If every defect sensor has bounded T1 defect in its Euler ledger scalar state, then every defect sensor has charge zero.
background
The module builds a T1-bounded realizability architecture replacing earlier total-cost bounds. A DefectSensor records the multiplicity (charge) and real part of a hypothetical zeta zero. PhysicallyExists sensor means there exists K such that the defect of eulerLedgerScalarState sensor N stays bounded by K for all natural numbers N. The upstream ontological_dichotomy theorem states that charge equals zero if and only if the sensor physically exists, which is the RS ontological argument for RH.
proof idea
One-line term proof: introduce the sensor and the hypothesis that it physically exists, then apply the mpr direction of ontological_dichotomy to obtain the required falsehood from nonzero charge.
why it matters
This supplies the physical-existence-implies-RH direction inside rh_iff_all_physical, completing the machine-verified equivalence between the number-theoretic statement and the RS physical principle. It realizes the ontological argument for RH via T1-bounded cost scalars on the Euler carrier. The result sits inside the unification of the functional equation with the eight-tick octave and phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.