ilg_parameter_count
plain-language theorem explainer
ILG's free phenomenological parameter count is defined as 0 when a named conjecture holds and 1 otherwise (the galactic timescale rung). Gravity and phenomenology workers cite it when stating the zero-parameter claim for emergent ILG. The body is a pure Boolean case split on that flag.
Claim. The number of free phenomenological parameters of ILG is $0$ if the conjecture holds and $1$ otherwise (the single remaining parameter being the galactic timescale rung).
background
Module G-004 formalizes the RS stance that gravity is emergent ledger curvature, not a spin-2 force. Three concrete claims sit nearby: $\kappa = 8\varphi^5$ is algebraic in $\varphi$ alone (no gauge generator), GW polarizations equal 2 in $D=3$, and a BMV entanglement rate $\kappa_{\mathrm{rs}}\approx 88.7$.
ILG is the RS gravity phenomenology. The Boolean flag here is whether a named conjecture closes the last free scale (the galactic timescale rung). If that conjecture is true, ILG inherits the zero-parameter character already claimed for the coupling via $\varphi$; if false, exactly one phenomenological parameter remains.
proof idea
Definition by cases on a Boolean: return $0$ when the conjecture flag is true and $1$ when false. No lemmas; the two downstream equalities are rfl unfoldings of this definition.
why it matters
Pins the bookkeeping for ILG's parameter count inside the NoGraviton / zero-parameter gravity story. Downstream, ilg_zero_params_if_conjecture and ilg_one_param_if_not are the two rfl corollaries that make the cases citeable as theorems. It sits next to $\kappa$ from $\varphi$ alone and the emergent-not-mediated claims: if the conjecture holds, gravity phenomenology has no free knobs beyond the RS constants forced by the T5–T8 chain ($J$-uniqueness, $\varphi$, eight-tick, $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.