direct_t1_exclusion
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.