realizedDefectCollapseScalar_defect_unbounded
The T1 defect of the realized collapse scalar grows without bound above for any nonzero-charge sensor. Researchers on the Recognition Science route to RH cite it to block a uniformly bounded T1 Euler ledger proxy. A short tactic proof obtains ε from the T1 cost barrier, N from the boundary-approaching lemma for nonzero charge, then applies the barrier inequality to the positive scalar and the closeness witness.
claimLet $J$ be the defect functional. For any sensor with nonzero charge, $J$ applied to the realized collapse scalar is unbounded above: for every real $C$ there exists a natural number $N$ such that $C < J$ of the scalar at step $N$.
background
The Unified RH module replaces earlier bounded-total-cost attempts with a three-component T1-bounded realizability architecture. CostDivergent holds for nonzero charge by annular coercivity; EulerTraceAdmissible holds for the Euler carrier; PhysicallyRealizableLedger requires the scalar proxy to keep T1 defect uniformly bounded. The defect functional equals $J(x)$ for $x>0$, where $J(x)=(x+x^{-1})/2-1$ diverges as $x$ approaches the T1 boundary at 0. The realized collapse scalar is the sensor-indexed proxy state whose approach to 0 is forced by divergence.
proof idea
The term-mode proof (written with tactics) introduces arbitrary $C$. It obtains positive ε and the implication $hε$ from the t1_cost_barrier lemma. It obtains $N$ from realizedDefectCollapseBoundaryApproaching_of_nonzero_charge using the sensor, nonzero-charge hypothesis, and ε. It then refines to that $N$ and applies $hε$ to the realized scalar, its positivity, and the boundary-closeness witness $hN$ to conclude the inequality.
why it matters in Recognition Science
This result directly supplies the unboundedness needed for not_realizedDefectCollapseScalar_t1_bounded, which negates any uniform bound $K$ on the defect. That negation supports EBBA_iff_rh, equating the EulerBoundaryBridgeAssumption to the Riemann Hypothesis. It closes the obstruction step in the module chain: divergence forces the scalar toward the T1 boundary, which T1-bounded realizability forbids. It touches the remaining external bridge hypothesis that would otherwise discharge the architecture without assuming RH.
scope and limits
- Does not give an explicit rate of defect growth.
- Does not apply to zero-charge sensors.
- Does not construct $N$ explicitly from $C$.
- Does not address other convergence properties of the scalar.
- Does not claim bounded defect for any non-collapse observable.
formal statement (Lean)
415theorem realizedDefectCollapseScalar_defect_unbounded
416 (sensor : DefectSensor) (hm : sensor.charge ≠ 0) :
417 ∀ C : ℝ, ∃ N : ℕ,
418 C <
419 IndisputableMonolith.Foundation.LawOfExistence.defect
420 (realizedDefectCollapseScalar sensor hm N) := by
proof body
Term-mode proof.
421 intro C
422 obtain ⟨ε, hεpos, hε⟩ := t1_cost_barrier C
423 obtain ⟨N, hN⟩ :=
424 realizedDefectCollapseBoundaryApproaching_of_nonzero_charge sensor hm ε hεpos
425 refine ⟨N, ?_⟩
426 exact hε
427 (realizedDefectCollapseScalar sensor hm N)
428 (realizedDefectCollapseScalar_pos sensor hm N)
429 hN
430
431/-- The current one-scalar closure target is impossible: the realized collapse
432observable cannot have uniformly bounded T1 defect, because its defect is
433already proved to be unbounded. -/