def definition def or abbrev

`BoundaryApproaching`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 255def BoundaryApproaching (sensor : DefectSensor)
 256    [PhysicallyRealizableLedger sensor] : Prop :=

proof body

Definition body.

 257  ∀ ε > 0, ∃ N : ℕ,
 258    PhysicallyRealizableLedger.scalarState (sensor := sensor) N < ε
 259
 260/-- T1 forbids a physically realizable ledger from approaching the boundary
 261`x = 0`: a uniform T1 defect bound contradicts `nothing_cannot_exist`. -/

used by (11)

From the project-wide theorem graph. These declarations reference this one in their body.

realizable_not_boundary_approaching in IndisputableMonolith.NumberTheory.T1BoundaryExclusion decl_use
T1BoundaryExclusionCert in IndisputableMonolith.NumberTheory.T1BoundaryExclusion decl_use
bridge_contradiction_core in IndisputableMonolith.Unification.UnifiedRH decl_use
CollapseBoundaryTransport in IndisputableMonolith.Unification.UnifiedRH decl_use
DivergenceWitnessesBoundary in IndisputableMonolith.Unification.UnifiedRH decl_use
eulerScalarProxy_not_boundaryApproaching in IndisputableMonolith.Unification.UnifiedRH decl_use
obstruction_structural_asymmetry in IndisputableMonolith.Unification.UnifiedRH decl_use
ontological_exclusion_of_realizable in IndisputableMonolith.Unification.UnifiedRH decl_use
physicallyRealizableLedger_not_boundaryApproaching in IndisputableMonolith.Unification.UnifiedRH decl_use
UnifiedRHCert in IndisputableMonolith.Unification.UnifiedRH decl_use
unified_rh_cert_of_bridge in IndisputableMonolith.Unification.UnifiedRH decl_use

depends on (6)

Lean names referenced from this declaration's body.

defect in IndisputableMonolith.Foundation.LawOfExistence decl_use
nothing_cannot_exist in IndisputableMonolith.Foundation.LawOfExistence decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
uniform in IndisputableMonolith.Information.ShannonEntropy decl_use
DefectSensor in IndisputableMonolith.NumberTheory.CostCoveringBridge decl_use
PhysicallyRealizableLedger in IndisputableMonolith.Unification.UnifiedRH decl_use