pith. machine review for the scientific record. sign in
class definition def or abbrev

DivergenceWitnessesBoundary

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 504class DivergenceWitnessesBoundary (sensor : DefectSensor)
 505    [PhysicallyRealizableLedger sensor] where
 506  toBoundary :
 507    EulerTraceAdmissible sensor → CostDivergent sensor → BoundaryApproaching sensor
 508
 509/-- If the concrete collapse scalar coming from the realized defect family
 510approaches `0`, then the Euler ledger scalar approaches the T1 boundary as
 511well.  After redefining the ledger scalar to be the realized collapse
 512observable in the nonzero-charge sector, this becomes a theorem. -/

used by (6)

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

depends on (8)

Lean names referenced from this declaration's body.