GeneralRelativityCert
plain-language theorem explainer
GeneralRelativityCert packages the two conditions needed to certify that general relativity follows from Recognition Science: exactly five canonical effects and a positive Einstein coupling. A physicist comparing RS predictions to GR observations would reference this certificate to confirm the count of testable effects matches the observed phenomena. The structure is assembled directly from the enumeration of GREffect and the positivity proof for einsteinKappa.
Claim. A structure certifying emergence of general relativity from Recognition Science, consisting of the assertion that the finite type of canonical effects has cardinality five together with the inequality $0 < 8 phi^5 / pi$.
background
The module derives Einstein field equations from RS in the strong-field regime, with coupling constant kappa equal to 8 phi^5 over pi. The inductive type GREffect enumerates five effects (gravitational lensing, time dilation, perihelion precession, frame dragging, gravitational waves) whose cardinality is required to equal five. The sibling definition einsteinKappa supplies the explicit real value 8 * phi ^ 5 / Real.pi, whose positivity is asserted separately.
proof idea
GeneralRelativityCert is a structure definition with no proof body. The downstream generalRelativityCert populates its fields by direct reference to grEffectCount for the cardinality and einsteinKappa_pos for the inequality.
why it matters
This definition supplies the interface for the general relativity certificate in the RS framework and is instantiated by generalRelativityCert. It ties the five effects directly to configDim D = 5 and the RS-native kappa = 8 phi^5 / pi, closing the A4 strong-field confirmation with zero axioms or sorrys.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.