ontological_dichotomy
For any defect sensor the charge vanishes exactly when the cost scalar stays uniformly bounded under the T1 defect. Researchers deriving the Riemann hypothesis inside Recognition Science cite the result as the unconditional mathematical core of the ontological argument. The tactic proof splits the biconditional, applies the zero-charge boundedness lemma forward, and reaches a contradiction via scalar-state collapse and direct T1 exclusion in the reverse direction.
claimFor every defect sensor $s$, the charge of $s$ equals zero if and only if there exists a real number $K$ such that, for every natural number $N$, the T1 defect of the Euler ledger scalar state of $s$ at $N$ is at most $K$.
background
A DefectSensor carries an integer charge together with parameters that index an arithmetic ledger. The T1 defect is the defect function supplied by the Law of Existence applied to scalar states on that ledger. The Euler ledger scalar state is the concrete realization of the sensor inside the Euler carrier. PhysicallyExists is defined exactly as the existence of a uniform real bound $K$ on these defects for all $N$ (see the sibling definition in the same module).
proof idea
The proof opens with the constructor tactic to split the biconditional. The forward direction invokes the lemma charge_zero_cost_scalar_t1_bounded directly. The reverse direction assumes a bound $K$, supposes the charge is nonzero, rewrites every scalar state to the corresponding realized defect collapse state, transfers the bound, and applies direct_t1_exclusion to obtain the contradiction.
why it matters in Recognition Science
This theorem supplies the central equivalence of the RS ontological argument for the Riemann hypothesis: charge zero is equivalent to T1-bounded physical realizability. It is invoked by nonzero_charge_not_physical to exclude nonzero-charge sensors from the physical predicate, by charge_zero_iff_physicallyExists as an immediate restatement, and by all_physicallyExist_of_rh to obtain the converse under RH. The result completes the mathematical half of the three-component architecture (cost divergence, Euler trace admissibility, T1-bounded ledger) described in the module documentation and advances the chain from Euler instantiation to the physical-existence criterion.
scope and limits
- Does not assert that every defect sensor has zero charge.
- Does not prove the Riemann hypothesis itself.
- Does not rely on any custom axioms beyond the T1 properties.
- Applies only to the Euler-carrier instantiation of the ledger.
- Does not address annular cost bounds.
Lean usage
theorem charge_zero_implies_physical (sensor : DefectSensor) : sensor.charge = 0 → PhysicallyExists sensor := (ontological_dichotomy sensor).mpformal statement (Lean)
873theorem ontological_dichotomy (sensor : DefectSensor) :
874 (sensor.charge = 0) ↔
875 ∃ K : ℝ, ∀ N : ℕ,
876 IndisputableMonolith.Foundation.LawOfExistence.defect
877 (eulerLedgerScalarState sensor N) ≤ K := by
proof body
Tactic-mode proof.
878 constructor
879 · exact charge_zero_cost_scalar_t1_bounded sensor
880 · intro ⟨K, hK⟩
881 by_contra hm
882 have : ∀ N, eulerLedgerScalarState sensor N =
883 realizedDefectCollapseScalar sensor hm N := by
884 intro N; exact eulerLedgerScalarState_eq_collapse sensor hm N
885 have hK' : ∀ N,
886 IndisputableMonolith.Foundation.LawOfExistence.defect
887 (realizedDefectCollapseScalar sensor hm N) ≤ K := by
888 intro N; rw [← this N]; exact hK N
889 exact direct_t1_exclusion sensor hm ⟨K, hK'⟩
890
891/-! ### §11c. Physical Existence — the Sound Formalization
892
893A `DefectSensor` is a mathematical structure that can be constructed with
894any integer charge. In particular, `{ charge := 1, realPart := 3/4, ... }`
895is a valid Lean term. Therefore the statement `∀ sensor, charge = 0` is
896**false** in Lean — it is refuted by construction.
897
898The RS ontological argument does NOT claim that all `DefectSensor` structures
899have charge `0`. It claims that all **physically realizable** sensors have
900charge `0` — where physical realizability means the cost scalar has bounded
901T1 defect.
902
903`ontological_dichotomy` proves **unconditionally**:
904
905 `charge = 0 ↔ PhysicallyExists sensor`
906
907This immediately gives: every physically existing sensor has charge `0`.
908No axioms. No hypotheses. Machine-verified from T1 alone.
909
910The RS argument for RH is then:
9111. `ontological_dichotomy` — PROVED: charge = 0 ↔ T1-bounded (no custom axioms)
9122. ζ zeros are physical events → T1-bounded (RS physical claim, not a Lean axiom)
9133. Therefore all ζ zeros have charge 0 (= RH)
914
915Step 1 is the mathematical content. Step 2 is the physical interpretation.
916Step 3 follows from 1 and 2. The Lean formalization captures step 1
917completely and lets step 2 be expressed as the `PhysicalSensor` subtype. -/
918
919/-- A sensor physically exists iff its cost scalar has bounded T1 defect.
920This is the RS existence criterion applied to the arithmetic ledger. -/