empiricalGateOpen
plain-language theorem explainer
The empirical design gate for order-sensitive 4D gravity is hard-coded closed. Anyone citing Campaign G6 coefficient-forcing status uses this flag to show that no fitted scalar may be designed until a forced coefficient exists. The body is the constant Boolean false.
Claim. The empirical gate is closed: the Boolean status flag equals $\mathrm{false}$. Design of any empirical gate remains frozen until a forced dimensionless coefficient exists.
background
Campaign G6 treats coefficient forcing for order-sensitive gravity under an explicit license gate. A dimensionless, normalization-invariant coefficient may be derived only after a nonzero continuum residual has been earned. The module records that continuum promotion is not earned, so coefficient forcing is not licensed.
The empirical gate is a separate freeze: even the design of how one would confront data stays closed until that forced coefficient exists. No fitted scalar is admitted as a stand-in. External experiments, publication, and spending remain separately gated after a coefficient appears.
This definition is the Boolean status of that empirical freeze. Sibling flags in the same module track licensing of coefficient forcing and the prohibition on forcing while the continuum residual is unearned.
proof idea
Definitional constant: the flag is set to false with no computation. The companion equality theorem is reflexivity on that definition.
why it matters
Pins the honesty claim of Campaign G6: empirical-gate design stays frozen closed until a forced coefficient exists. Downstream, the equality theorem records that the flag equals false and carries the gloss that no fitted scalar may stand in for a forced coefficient. Together with the unlicensed coefficient-forcing flag, this blocks premature data-facing design while continuum promotion remains unearned. It does not produce the open coefficient itself; it only freezes the empirical side until that object appears.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.