pith. machine review for the scientific record. sign in
def hypothesis interface def or abbrev

ReggeConvergenceHypothesis

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)

 140def ReggeConvergenceHypothesis : Prop :=

proof body

Definition body.

 141  ∀ (g : MetricTensor),
 142    (∀ x, metric_matrix_invertible_at g x) →
 143    ∃ (rate : ℝ), rate > 0 ∧
 144      True  -- Placeholder for: |S_Regge[T_N] - S_EH[g]| ≤ C · a^rate
 145
 146/-! ## §6 The Complete Bridge Certificate -/
 147
 148/-- The complete discrete-to-continuum bridge certificate.
 149
 150    This packages everything needed to conclude that N → ∞ J-cost lattice sites
 151    with defect-sourced metric perturbation produce the Einstein field equations
 152    in the coarse-graining limit. -/

used by (3)

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

depends on (14)

Lean names referenced from this declaration's body.