no_forced_coefficient_while_unearned
plain-language theorem explainer
While continuum promotion remains unearned, no forced dimensionless gravity coefficient can be constructed. Gravity analysts cite this as the Campaign G6 methodological wall: coefficient forcing stays closed until a nonzero continuum residual is earned. The proof is a short term argument: the earned flag is definitionally false, so the existential is impossible regardless of the license hypothesis.
Claim. If coefficient forcing is unlicensed, then there is no forced coefficient $c$ (a rescaling-, seating-, and refinement-invariant real ratio derived from $J$-cost or genesis, not fitted) for which continuum promotion is earned. Equivalently: unlicensed forcing precludes any witness that continuum promotion has been earned.
background
Campaign G6 gates coefficient forcing for order-sensitive gravity. A dimensionless, normalization-invariant coefficient may be derived only after a nonzero continuum residual is earned. Until then the empirical gate stays frozen closed; no fitted scalar is admitted as a stand-in.
Continuum promotion is an honest status flag fixed at false in the residual module; the companion equality theorem records that fact by reflexivity. Coefficient forcing is licensed exactly when that flag is true, so the license is presently false as well.
A forced coefficient is a structure carrying a real ratio, a genesis-or-$J$-cost provenance bit, and invariance propositions under rescaling, seating, and refinement, plus an explicit not-fitted clause. The module's honesty note: the gate status is theorem-level; the coefficient itself remains open.
proof idea
Term-mode proof. Assume the license flag is false and, for contradiction, a pair consisting of some forced-coefficient witness together with the assertion that continuum promotion is earned. Rewrite the earned assertion by the upstream equality theorem, which identifies the earned flag with false. The rewritten goal is then false = true, discharged by Bool.false_ne_true. The license hypothesis is unused; the contradiction is carried entirely by the fixed falsehood of continuum promotion.
why it matters
This is the Campaign G6 wall theorem: no forced coefficient is constructed while continuum promotion is unearned. It records, at theorem level, that coefficient forcing stays closed and that the empirical-gate design remains frozen until a genuine coefficient exists. Downstream use is presently empty; the declaration is a standing prohibition rather than a lemma in a longer derivation chain.
In the broader Recognition gravity program it separates honest residual status from premature scalar fitting. The coefficient itself is explicitly open: no fitted number is admitted, and external experiments, publication, and spending remain separately gated even after a coefficient appears. The result does not touch the forcing chain T0–T8, RCL, or the mass ladder; it is a methodological lock on 4D order-sensitive continuum promotion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.