stationarityBridgeClosureStatus_flags
plain-language theorem explainer
Canonical status flags for the stationarity-to-bridge closure: the constitutive deficit-source bridge is marked closed, and derivation from the bare recognition ledger is marked false. Gravity auditors of the Seven Gaps campaign cite this to lock promotion language. The proof is pure reflexivity on the status record definition.
Claim. In the canonical stationarity-bridge closure status record, the flag "constitutive stationarity bridge closed" equals $\mathrm{true}$ and the flag "derivation from bare ledger" equals $\mathrm{false}$.
background
The Seven Gaps gravity stack builds a recognition-ratio bridge from hinge-wise stationarity of a sourced action. The constitutive model couples a deficit to a source inside sourcedAction; J-cost identification is the kernel equation equating that action to a sum of J-costs. Stationarity theorems supply a unique global minimizer whose total strain defines the bridge ratio $x^*$, with a cubic remainder bound of constant $1/6$ under mesh domination.
RecognitionRatioBridge left a derivation-from-stationarity flag open. This module inhabits the bridge by constructor: ratio data are defined from the minimizer, not hypothesized. Kernel kill records show the bare-ledger route is circular, so the bare-ledger derivation flag is locked false.
The upstream definition stationarityBridgeClosureStatus is the canonical record with those two Boolean fields preset; the present theorem only reifies them as equalities.
proof idea
One-line term proof: pair of rfl proofs. Each conjunct unfolds the corresponding field of the canonical status definition and matches by definitional equality. No lemmas, no tactics beyond the anonymous constructor.
why it matters
Locks campaign language for the stationarity bridge: closed under an explicit deficit-source constitutive action plus J-stationarity, never claimed from the bare RecognitionLedger. That distinction is the module's audit point; the bare-ledger kill path (closed-cycle coboundary vanishing and budget-implies-ratio without stationarity) stays documented by the false flag.
No downstream dependents are wired yet; the theorem is documentation infrastructure for the closure module itself. It does not advance T0–T8 forcing, RCL, or the mass ladder; it only certifies how the gravity ratio bridge may be cited after the constructor recognitionRatioBridge_ofStationarity is built.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.