coupling_from_phi
In Recognition Science native units the Einstein coupling constant equals 8φ^5 and is strictly positive. Researchers assembling the discrete-to-continuum bridge from J-cost lattices to continuum curvature cite this result as one of the proved Tier 1 components. The proof is a direct term-mode application of multiplication positivity together with the fact that a positive base raised to a real power remains positive.
claimIn Recognition Science units with $c=1$, the Einstein coupling constant satisfies $κ=8φ^5>0$.
background
The Discrete-to-Continuum Bridge module connects the discrete J-cost lattice theory to continuum general relativity by the chain J-cost lattice to quadratic defect to lattice Laplacian to Ricci scalar to Einstein tensor. This theorem belongs to the proved Tier 1 results that also include the Minkowski flat limit and the spatial metric derived from J-cost. The local setting is given by the three-tier architecture in which Tier 1 supplies the coupling $κ=8φ^5$ while Tier 3 packages the external Regge convergence hypothesis.
proof idea
The term proof applies the lemma that the product of two positive reals is positive, with the constant factor 8 shown positive by normalization and the factor $φ^5$ shown positive by the real-power positivity lemma applied to the established positivity of $φ$.
why it matters in Recognition Science
The result supplies the coupling_positive field required by the bridge_certificate theorem that inhabits the DiscreteContinuumBridge structure. It completes the proved coupling step of the discrete-to-continuum bridge, consistent with the forcing-chain constants that yield $G=φ^5/π$ and therefore $κ=8φ^5$. The declaration remains independent of the Regge Convergence Hypothesis that appears only in Tier 3.
scope and limits
- Does not derive the explicit numerical value of G or c.
- Does not prove convergence of Regge calculus to the Einstein-Hilbert action.
- Does not establish the spatial dimension D=3.
- Does not address higher-order curvature terms beyond the leading coupling factor.
formal statement (Lean)
116theorem coupling_from_phi : (8 : ℝ) * phi ^ (5 : ℝ) > 0 := by
proof body
Term-mode proof.
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. -/