direct_t1_exclusion
Nonzero charge on a DefectSensor forces the T1 defect of its realized collapse scalar to diverge over all natural numbers N. Workers on the Recognition Science ontological argument cite this to separate the realizable charge-zero sector from all others. The proof is a direct one-line application of the already-established unboundedness theorem for that scalar.
claimLet $s$ be a DefectSensor whose charge is nonzero. Then no real $K$ exists such that the defect $J$ of the realized collapse scalar for $s$ satisfies $J(s,N) ≤ K$ for every natural number $N$.
background
DefectSensor is the structure carrying an integer charge (multiplicity of a zeta zero) and real part location inside the critical strip. The defect functional equals the J-cost, which vanishes at unity. realizedDefectCollapseScalar produces the scalar proxy state attached to a given sensor and iteration N. The module replaces an earlier total-cost ledger with a three-part architecture: CostDivergent for nonzero charge, EulerTraceAdmissible for the carrier, and PhysicallyRealizableLedger for the bounded-T1 case. The immediate upstream result not_realizedDefectCollapseScalar_t1_bounded already records that the realized scalar cannot stay bounded when charge is nonzero.
proof idea
One-line wrapper that applies not_realizedDefectCollapseScalar_t1_bounded to the supplied sensor and charge hypothesis.
why it matters in Recognition Science
The theorem supplies the nonzero-charge direction of ontological_dichotomy, which asserts that T1-bounded defect holds if and only if charge equals zero. This is the one-scalar core of the RS ontological argument: nonzero charge implies unbounded defect, hence non-realizability. The parent ontological_dichotomy invokes it directly to finish the equivalence. The result sits inside the T1-Bounded Realizability Architecture and closes the divergence half of the chain that begins from CostDivergent.
scope and limits
- Does not prove existence of any physical sensor.
- Does not bound the defect when charge equals zero.
- Does not treat annular cost divergence directly.
- Does not establish the Riemann hypothesis.
formal statement (Lean)
851theorem direct_t1_exclusion (sensor : DefectSensor) (hm : sensor.charge ≠ 0) :
852 ¬ ∃ K : ℝ, ∀ N : ℕ,
853 IndisputableMonolith.Foundation.LawOfExistence.defect
854 (realizedDefectCollapseScalar sensor hm N) ≤ K :=
proof body
Term-mode proof.
855 not_realizedDefectCollapseScalar_t1_bounded sensor hm
856
857/-- For charge `0`, the Euler ledger scalar `1` has T1 defect `0` — perfectly
858bounded. The charge-`0` sector IS physically realizable. -/