theorem
proved
physicallyRealizableLedger_not_boundaryApproaching
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Unification.UnifiedRH on GitHub at line 262.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
K -
K -
canonical -
extracted -
defect -
cost -
cost -
is -
from -
as -
is -
for -
is -
canonical -
is -
divergence -
total -
canonical -
and -
DefectSensor -
total -
BoundaryApproaching -
eulerScalarProxy -
PhysicallyRealizableLedger -
t1_cost_barrier
used by
formal source
259
260/-- T1 forbids a physically realizable ledger from approaching the boundary
261`x = 0`: a uniform T1 defect bound contradicts `nothing_cannot_exist`. -/
262theorem physicallyRealizableLedger_not_boundaryApproaching
263 (sensor : DefectSensor) [PhysicallyRealizableLedger sensor] :
264 ¬ BoundaryApproaching sensor := by
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. -/