ontological_dichotomy
plain-language theorem explainer
The theorem establishes that for any DefectSensor its charge vanishes if and only if the Euler ledger scalar states have uniformly bounded T1 defect. Researchers deriving the Riemann hypothesis inside Recognition Science cite this as the unconditional mathematical core of the ontological argument. The tactic proof splits the biconditional with constructor, applies charge_zero_cost_scalar_t1_bounded forward, and reaches a contradiction via state rewriting plus direct_t1_exclusion in the converse direction.
Claim. For any DefectSensor $s$, the charge of $s$ equals zero if and only if there exists a real constant $K$ such that the T1 defect of the Euler ledger scalar state of $s$ at every natural number $N$ is at most $K$.
background
The Unified RH module replaces earlier total-cost assertions with a three-component architecture: CostDivergent for nonzero charge, EulerTraceAdmissible for the convergent Euler carrier, and PhysicallyRealizableLedger whose scalar proxy stays T1-bounded. A DefectSensor is a structure carrying an integer charge together with real parameters; eulerLedgerScalarState produces the associated ledger state at each natural number. The defect function is taken from LawOfExistence. PhysicallyExists is defined precisely as the existence of a uniform bound $K$ on these defects. The module doc states that this structure relies on proved Euler carrier instances and external bridge hypotheses for boundary transport.
proof idea
The proof applies the constructor tactic to split the biconditional. The forward direction invokes the lemma charge_zero_cost_scalar_t1_bounded. The converse assumes a bound $K$, derives a contradiction from nonzero charge by rewriting every ledger state to the realized defect collapse form via eulerLedgerScalarState_eq_collapse, then applies direct_t1_exclusion to the resulting bounded-defect hypothesis.
why it matters
This supplies the machine-verified step in the Recognition Science ontological argument for the Riemann hypothesis: charge zero if and only if T1-bounded if and only if physically realizable. It is invoked directly by charge_zero_iff_physicallyExists, nonzero_charge_not_physical, and all_physicallyExist_of_rh. The module doc positions it as the mathematical content of step 1 in the RH derivation, with the physical claim that zeta zeros are T1-bounded supplied externally. It closes the dichotomy without custom axioms and links to the T1 cost barrier in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.