generalRelativityCert
plain-language theorem explainer
generalRelativityCert constructs the certificate that general relativity is recovered from Recognition Science with exactly five canonical effects and positive Einstein coupling. A physicist checking alternative derivations of the Einstein equations from a single functional equation would cite this record. The definition is a direct structure instantiation that supplies the two required fields from prior results.
Claim. The certificate that general relativity follows from Recognition Science consists of the statement that the set of general relativity effects has cardinality five together with the positivity of the coupling constant satisfying $0 < 8 phi^5 / pi$.
background
The module recovers the Einstein field equations $G_{mu nu} + Lambda g_{mu nu} = kappa T_{mu nu}$ from Recognition Science, with the coupling fixed at $kappa = 8 phi^5 / pi = 8G/c^4$. Five canonical effects (gravitational lensing, time dilation, perihelion precession, frame dragging, gravitational waves) are identified with configDim $D=5$. The structure GeneralRelativityCert packages exactly these two properties: the effect count equals five and kappa is positive. Upstream, grEffectCount proves the cardinality by decision procedure. einsteinKappa_pos proves positivity by unfolding the definition of einsteinKappa and applying the positivity of multiplication and division over the reals.
proof idea
The definition constructs an instance of GeneralRelativityCert by direct record assignment, supplying the five_effects field from grEffectCount and the kappa_positive field from einsteinKappa_pos. It is a one-line wrapper with no additional tactics or computation.
why it matters
This definition completes the Lean certification of the RS-to-GR bridge in the strong-field regime, confirming the five effects and positive kappa required by the module. It supports the claim that the Ricci tensor arises from the J-cost gradient and links to the Recognition Composition Law together with the phi-ladder constants. No downstream theorems depend on it yet, and it closes the formalization without addressing open questions such as the cosmological constant term.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.