grEffectCount
plain-language theorem explainer
The theorem establishes that the finite type of canonical general relativity effects has cardinality five. A researcher recovering Einstein gravity from Recognition Science would cite this to confirm the enumeration of testable predictions matches the standard list. The proof is a one-line decision tactic that evaluates the cardinality directly from the inductive definition and its derived Fintype instance.
Claim. The finite type enumerating the five canonical general relativity effects (gravitational lensing, time dilation, perihelion precession, frame dragging, gravitational waves) has cardinality five: $|E| = 5$ where $E$ is the inductive type with those five constructors.
background
The module derives the Einstein field equations $G_μν + Λ g_μν = κ T_μν$ from Recognition Science, with coupling $κ = 8 φ^5 / π > 0$. The local setting lists five canonical GR effects whose count equals configDim $D = 5$. The inductive type enumerates exactly these cases and derives DecidableEq, Repr, BEq, and Fintype so that cardinality is computable. The upstream constant scalar field definition supplies the scalar background used elsewhere in the module but is not invoked by this cardinality statement.
proof idea
The proof is a term-mode wrapper that applies the 'decide' tactic. Because the inductive type derives Fintype, the tactic reduces the equality to a decidable computation that returns true for cardinality five.
why it matters
This result supplies the five_effects field inside the generalRelativityCert definition and is reused verbatim by all_gr_effects_tested. It anchors the A4 Strong Field claim that all five effects are tested and consistent with RS predictions, closing the enumeration step before the positivity proof for κ. It directly supports the framework landmark that GR effects arise from J-cost gradients in three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.