ForcedCoefficient
plain-language theorem explainer
A forced gravity coefficient is a real ratio that must come from J-cost or genesis, stay invariant under rescaling, seating, and refinement, and never be a fitted nonzero scalar. Gravity analysts cite it when stating what a legitimate continuum coefficient would have to satisfy. It is a pure structure definition, not a construction.
Claim. A forced coefficient is a real number $r$ together with a Boolean flag that it arises from the $J$-cost or genesis, three propositions asserting invariance under rescaling, seating, and refinement, and the discipline that a nonzero $r$ is never admitted as a fitted scalar.
background
Campaign G6 gates coefficient forcing for order-sensitive 4D gravity. A dimensionless, normalization-invariant coefficient may be derived only after a nonzero continuum residual is earned. The module records that continuum promotion is presently unearned, so coefficient forcing is not licensed, and the empirical gate stays frozen closed.
Upstream, the CPT ratio coordinate is the real $R.\iota_S(s)/R.\iota_O(o)$ entering the canonical reciprocal cost used in factorization arguments. The golden cost-projector package supplies the notion of a quantity forced by being a projector. Those supply the intended provenance for any future coefficient: it must come from $J$-cost structure or genesis, not from a free fit.
Local honesty is explicit: the gate status is theorem-shaped; the coefficient itself remains open. No fitted scalar is admitted in its place.
proof idea
There is no proof body. The declaration is a structure bundling the mathematical obligations a forced coefficient must meet: a real ratio, a Boolean provenance flag (from $J$-cost or genesis), three invariance propositions (rescaling, seating, refinement), and the not-fitted discipline on nonzero ratios. Downstream theorems quantify over inhabitants of this type.
why it matters
This type is the formal stand-in for the still-open continuum coefficient in order-sensitive gravity. The parent wall theorem no_forced_coefficient_while_unearned uses it to prove that if coefficient forcing is unlicensed, no such coefficient can coexist with earned continuum promotion (which is false by the continuum residual gate).
In the Recognition framework this protects the forcing chain discipline: dimensionless constants (compare $\alpha^{-1}$ in the RS band, or $G=\varphi^5/\pi$ in RS-native units) are admissible only when forced from $J$ and the composition law, not fitted. The module keeps external experiments and spending Jon-gated even after a coefficient exists. The open question remains construction of an actual inhabitant once continuum promotion is earned.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.