coupling_from_phi

formal source

 113
 114/-- The Einstein coupling κ = 8πG/c⁴ = 8φ⁵ in RS-native units.
 115    This is derived in `Constants.lean` and `ZeroParameterGravity.lean`. -/
 116theorem coupling_from_phi : (8 : ℝ) * phi ^ (5 : ℝ) > 0 := by
 117  apply mul_pos (by norm_num : (8 : ℝ) > 0)
 118  exact Real.rpow_pos_of_pos phi_pos 5
 119
 120/-! ## §5 Regge Convergence Hypothesis -/
 121
 122/-- Non-degeneracy of the metric matrix at a point.
 123    This mirrors the variational layer's invertibility hypothesis without
 124    importing the full `Variation.Functional` stack. -/
 125def metric_matrix_invertible_at (g : MetricTensor) (x : Fin 4 → ℝ) : Prop :=
 126  Nonempty (Invertible (metric_to_matrix g x))
 127
 128/-- **HYPOTHESIS (External Mathematics)**: Nonlinear Regge calculus convergence.
 129
 130    On a sequence of simplicial manifolds T_N with mesh → 0, the Regge action
 131    S_Regge[T_N] converges to the Einstein-Hilbert action S_EH[g] for smooth g.
 132
 133    Reference: Cheeger, Muller, Schrader (1984), "On the curvature of piecewise
 134    flat spaces", Comm. Math. Phys. 92, 405-454.
 135
 136    This is standard external mathematics, analogous to the Aczel smoothness
 137    package for d'Alembert solutions. It is NOT an RS assumption. If/when
 138    physlib or Mathlib formalizes Regge calculus convergence, this hypothesis
 139    can be discharged by import. -/
 140def ReggeConvergenceHypothesis : Prop :=
 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 -/