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

DiscreteContinuumBridge

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)

 153structure DiscreteContinuumBridge : Prop where
 154  -- Tier 1: PROVED (from ContinuumManifoldEmergence and this module)
 155  flat_chain : FlatChain
 156  coupling_positive : (8 : ℝ) * phi ^ (5 : ℝ) > 0
 157  dimension : (1 : ℕ) + 3 = 4
 158
 159  -- Tier 2: PROVED (from Curvature.lean, LeviCivitaTheorem.lean)
 160  christoffel_torsion_free : IsTorsionFree (christoffel minkowski_tensor)
 161  levi_civita_exists : FundamentalTheoremExistence minkowski_tensor
 162  levi_civita_unique : FundamentalTheoremUniqueness minkowski_tensor
 163
 164  -- Tier 3: HYPOTHESIS (external mathematics)
 165  regge_convergence : ReggeConvergenceHypothesis
 166
 167/-- The bridge certificate is inhabited (modulo the Regge hypothesis). -/

used by (2)

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

depends on (16)

Lean names referenced from this declaration's body.