WeakFieldBridge

formal source

 104    ∇²Φ = (κ/2) ρ, where Φ = -h_{00}/2 and ρ is mass density.
 105
 106    This is the bridge from curvature to Newtonian gravity. -/
 107structure WeakFieldBridge where
 108  potential : (Fin 4 → ℝ) → ℝ
 109  density : (Fin 4 → ℝ) → ℝ
 110  poisson : ∀ x, laplacian potential x = (1/2 : ℝ) * 8 * phi ^ 5 * density x
 111
 112/-! ## §4 Coupling Constant Chain -/
 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