theorem proved term proof

`bridge_contradiction_core`

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

formal statement (Lean)

 680theorem bridge_contradiction_core (sensor : DefectSensor)
 681    [inst : PhysicallyRealizableLedger sensor]
 682    (hba : BoundaryApproaching sensor) :
 683    False :=

proof body

Term-mode proof.

 684  physicallyRealizableLedger_not_boundaryApproaching sensor hba
 685
 686/-- The structural asymmetry that makes the bridge nontrivial: the collapse
 687observable approaches `0` while the realizability proxy stays bounded away
 688from `0`.  Any proof of the bridge must reconcile these two distinct scalar
 689behaviors.  This theorem packages both sides as a conjunction. -/

depends on (15)

Lean names referenced from this declaration's body.

nontrivial in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
DefectSensor in IndisputableMonolith.NumberTheory.CostCoveringBridge decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
two in IndisputableMonolith.QFT.SpinStatistics decl_use
BoundaryApproaching in IndisputableMonolith.Unification.UnifiedRH decl_use
PhysicallyRealizableLedger in IndisputableMonolith.Unification.UnifiedRH decl_use
physicallyRealizableLedger_not_boundaryApproaching in IndisputableMonolith.Unification.UnifiedRH decl_use