coupling_from_phi
plain-language theorem explainer
The theorem asserts positivity of the Einstein coupling expressed as eight times phi to the fifth power in RS-native units. Workers assembling the discrete-to-continuum bridge certificate cite it to confirm the coupling term remains positive. The proof is a direct term-mode application of multiplication positivity together with the fact that phi raised to the fifth power stays positive.
Claim. $8 phi^5 > 0$, where $phi$ is the self-similar fixed point of the Recognition Science forcing chain and the expression equals the Einstein coupling constant $kappa$ in RS-native units.
background
The module builds the discrete-to-continuum bridge that maps J-cost lattice data through quadratic defect, lattice Laplacian, Ricci scalar, Einstein tensor, and the Einstein field equations. Tier 1 of the architecture lists the coupling $kappa = 8 phi^5$ among the proved statements, alongside the flat limit and $D=3$. Upstream structures supply the J-cost definition from PhiForcingDerived.of, the ledger factorization from DAlembert.LedgerFactorization.of, and the spectral emergence of gauge content from SpectralEmergence.of.
proof idea
The term proof applies mul_pos to the norm_num fact that 8 is positive and to Real.rpow_pos_of_pos instantiated at phi_pos and exponent 5.
why it matters
bridge_certificate invokes this result as coupling_positive to inhabit DiscreteContinuumBridge. The declaration completes the proved tier-1 list in the module architecture and records the Einstein coupling derived in Constants.lean. It anchors the positivity step required before the Regge convergence hypothesis is introduced in tier 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.