continuumPromotionEarned
plain-language theorem explainer
Boolean status flag fixed at false: continuum promotion of the order-sensitive residual is not earned. Gravity analysts cite it as the honesty gate before any continuum novelty or coefficient forcing. The body is the literal constant false; companion theorems prove the finite outside-image result cannot flip it.
Claim. The continuum-promotion status flag is the Boolean constant $\mathsf{false}$: promotion of the order-sensitive residual from the finite metric-edge-image exclusion to a continuum terminal (survival, metric collapse, or lattice washout) has not been earned.
background
Campaign G4/G5 studies continuum promotion of the order-sensitive residual in 4D gravity analysis. The finite stage already shows the response difference of a certificate pair lies outside the metric edge image. Continuum work replaces that Boolean non-membership by a normalized-separation trichotomy along a shape-regular refinement family: survive (positive liminf of normalized distance to the metric image), metric collapse (normalized distance tends to 0 while the response norm does not), or lattice washout (response norm tends to 0).
Those three continuum terminals are recorded in the module as open residual propositions. The geometric mesh Tendsto baseline is required before any terminal may be claimed. The module forbids promoting the finite Boolean exclusion to continuum novelty. This definition is the explicit honesty flag encoding that prohibition.
proof idea
Definitional constant: the flag is bound to the Boolean value false. No lemmas, tactics, or computation. Equality to false is immediate by reflexivity in the companion theorem; the methodological wall then ignores any finite outside-image hypothesis and returns that same equality.
why it matters
The flag is the licensing gate for coefficient forcing. Downstream, coefficient forcing is licensed only when this flag is true, and a wall theorem states that while it remains false no forced coefficient may be constructed. Companion results in the same module prove the finite outside-image theorem does not flip the flag, so finite residual novelty cannot be smuggled into continuum claims.
In the Recognition gravity stack this keeps Campaign G4/G5 honest: continuum survival, collapse, and washout stay open until the mesh Tendsto baseline and an inhabited terminal exist. The declaration therefore blocks premature coefficient forcing and premature continuum novelty rather than asserting new physics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.