physicallyRealizableLedger_not_boundaryApproaching
A physically realizable ledger, carrying a scalar proxy whose T1 defect remains uniformly bounded, cannot have that proxy driven arbitrarily close to zero. Researchers working on the unified RH architecture cite this result to close the T1 boundary exclusion step. The proof assumes boundary approach, extracts the uniform defect bound K from the ledger interface, invokes the T1 cost barrier to produce an N where defect exceeds K, and obtains the contradiction via not_lt_of_ge.
claimLet $s$ be a defect sensor equipped with a physically realizable ledger, so that its scalar proxy state $x_N > 0$ satisfies a uniform bound on the defect functional: there exists $K$ such that defect$(x_N) ≤ K$ for all $N$. Then $x_N$ cannot approach the T1 boundary: it is not the case that for every $ε > 0$ there exists $N$ with $x_N < ε$.
background
In the Unified RH module the architecture separates cost divergence, Euler trace admissibility, and the PhysicallyRealizableLedger interface. The latter attaches to a DefectSensor a scalar proxy state $x_N$ together with the guarantee that defect$(x_N)$ stays bounded by some fixed $K$; defect is the J-cost functional from LawOfExistence. BoundaryApproaching is the predicate that this proxy can be driven below any positive $ε$. The module imports K from Constants (defined as $ϕ^{1/2}$) and the canonical/extracted arithmetic objects, but the local argument relies only on the ledger interface and the sibling t1_cost_barrier lemma.
proof idea
Proof by contradiction. Assume BoundaryApproaching sensor. Obtain the uniform bound $K$ from PhysicallyRealizableLedger.scalarDefectBounded. Apply t1_cost_barrier K to produce $ε > 0$ such that any positive scalar state below $ε$ has defect strictly larger than $K$. The boundary assumption supplies an $N$ with scalarState $N < ε$; the barrier then yields $K <$ defect(scalarState $N$), contradicting the uniform bound via not_lt_of_ge.
why it matters in Recognition Science
This supplies the proved half of the T1 boundary exclusion used directly by realizable_not_boundary_approaching and by bridge_contradiction_core to reach absurdity. It is invoked inside ontological_exclusion_of_realizable and obstruction_structural_asymmetry to separate the bounded realizability proxy from the collapse observable that approaches zero. The result closes the T1 step in the forcing chain for the Euler carrier while leaving the external DivergenceWitnessesBoundary bridge as the remaining hypothesis.
scope and limits
- Does not prove existence of any PhysicallyRealizableLedger instance.
- Does not derive the T1 cost barrier or the defect functional.
- Does not address zero-charge sensors or the bridge hypothesis itself.
- Does not establish convergence of the Euler trace.
Lean usage
theorem use_in_bridge (sensor : DefectSensor) [PhysicallyRealizableLedger sensor] (hba : BoundaryApproaching sensor) : False := physicallyRealizableLedger_not_boundaryApproaching sensor hbaformal statement (Lean)
262theorem physicallyRealizableLedger_not_boundaryApproaching
263 (sensor : DefectSensor) [PhysicallyRealizableLedger sensor] :
264 ¬ BoundaryApproaching sensor := by
proof body
Tactic-mode proof.
265 intro hboundary
266 obtain ⟨K, hK⟩ := PhysicallyRealizableLedger.scalarDefectBounded (sensor := sensor)
267 obtain ⟨ε, hεpos, hε⟩ := t1_cost_barrier K
268 obtain ⟨N, hN⟩ := hboundary ε hεpos
269 have hlt :
270 K <
271 IndisputableMonolith.Foundation.LawOfExistence.defect
272 (PhysicallyRealizableLedger.scalarState (sensor := sensor) N) := by
273 exact hε
274 (PhysicallyRealizableLedger.scalarState (sensor := sensor) N)
275 (PhysicallyRealizableLedger.scalarStatePos (sensor := sensor) N)
276 hN
277 exact not_lt_of_ge (hK N) hlt
278
279/-
280The auxiliary Euler stiffness proxy `eulerScalarProxy` is the actual
281T1-bounded realizability scalar for the Euler ledger. It stays away from the
282boundary and therefore supports the `PhysicallyRealizableLedger` interface.
283
284The realized collapse observable extracted from the canonical defect family is
285defined separately below. It captures the divergence-to-boundary mechanism, but
286the theorems proved in this file show it cannot itself serve as the uniformly
287T1-bounded realizability scalar.
288-/
289
290/-! ## §5. Concrete collapse mechanism from the realized defect family -/
291
292/-- The total annular cost is nonnegative. -/