GREffect
plain-language theorem explainer
Recognition Science enumerates five canonical general relativity effects via an inductive type. Researchers confirming the RS derivation of Einstein gravity cite this list to verify that all standard strong-field phenomena are recovered. The definition supplies the finite type structure whose cardinality is computed directly as five by the decide tactic in a downstream theorem.
Claim. The inductive type of canonical general relativity effects is generated by the five constructors gravitational lensing, time dilation, perihelion precession, frame dragging, and gravitational waves.
background
The module recovers the Einstein field equations $G_μν + Λ g_μν = κ T_μν$ from Recognition Science, with coupling $κ = 8 φ^5 / π$ obtained from the J-cost gradient. The Ricci tensor is identified with that gradient, and the five listed effects are asserted to equal the configuration dimension $D=5$ in the strong-field regime. The local setting assumes the forcing chain has already fixed φ as the self-similar point and established $D=3$ spatial dimensions, while treating the effect count separately as $D=5$.
proof idea
The declaration is the inductive definition that introduces the five constructors and derives DecidableEq, Repr, BEq, and Fintype instances. No lemmas are applied; the Fintype structure is generated automatically by the inductive declaration. The cardinality computation is deferred to the downstream theorem that applies the decide tactic.
why it matters
This enumeration is the basis for the GeneralRelativityCert structure, which requires Fintype.card of the type to equal 5 together with positivity of einsteinKappa, and for the theorem all_gr_effects_tested. It fills the explicit listing step in the module's claim that all five GR effects are tested and consistent with RS predictions. The framework landmark is the recovery of the Einstein equations with $κ = 8 φ^5 / π > 0$ from the J-cost gradient after T5 J-uniqueness and T6 phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.