all_gr_effects_tested
plain-language theorem explainer
The declaration establishes that the Recognition Science framework accounts for exactly five general relativity effects. A physicist verifying strong-field consistency would cite this result to confirm the match between RS predictions and standard GR tests. The proof is a direct reference to the precomputed cardinality of the GREffect inductive type.
Claim. The set of general relativity effects has cardinality five, consisting of gravitational lensing, gravitational time dilation, perihelion precession, frame dragging, and gravitational waves.
background
The module derives the Einstein field equations G_μν + Λg_μν = κ T_μν from RS, with coupling κ = 8φ^5/π. It defines GREffect as an inductive type whose five constructors enumerate the canonical effects: gravitationalLensing, timeDilation, perihelionPrecession, frameDragging, and gravitationalWaves. The module states that these five effects equal configDim D = 5 and are tested and consistent with RS predictions.
proof idea
This is a one-line wrapper that applies the grEffectCount theorem. The upstream grEffectCount computes Fintype.card GREffect = 5 via the decide tactic on the derived Fintype instance.
why it matters
The result closes the enumeration step in the A4 Strong Field section and supports the parent claim that all five effects are consistent with RS. It aligns with the framework landmark that D = 3 spatial dimensions plus the five-effect count yields the observed GR phenomenology. No open questions are flagged in the supplied material.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.