recognitionMeshDualEntryCoupling4DStatus
plain-language theorem explainer
Status record for Wave B residual R4 (mesh dual-entry constitutive coupling): R4 is marked closed, the ledger-named recognition-ratio binding is flagged open (owned by R5), and gap1_bridge_derived stays false. Downstream flag-check theorems cite it. The body is a three-field structure literal with boolean constants.
Claim. The R4 dual-entry coupling status package is the triple $(r4\_closed,\ recognition\_ratio\_ledger\_binding\_open,\ gap1\_bridge\_derived) = (\mathrm{true},\ \mathrm{true},\ \mathrm{false})$.
background
Wave B residual R4 assembles banked pieces R1 (mesh geometric deficit), R2 (hinge kappa with source domination), and R3 (dual-entry strain state) into an inhabited DeficitSourceConstitutiveCoupling on the carrier $H = \mathbb{R}$. From that coupling it applies the blocker's conditional recognition-ratio derivation, yielding a mesh-local derived-ratio theorem rather than a ledger-named standalone Prop.
The status structure packages three honesty flags for this module: whether R4 itself is closed, whether the ledger-named binding RecognitionRatioDerived remains open (R5 owns that landing), and whether the gap1 bridge has been derived. Module scope explicitly refuses to flip the bridge flag, refuses a ledger-named standalone binding, and keeps the carrier as reshaped reals rather than an encoded Freudenthal triangulation.
Convention pin: deficit iff debit-leads ($0 < h$), mirroring the Regge-side geometric-deficit convention.
proof idea
Definitional structure literal. Instantiates the three Bool fields of the status package by constants: R4 closed true, ledger-named recognition-ratio binding open true, gap1 bridge derived false. No lemmas, no tactics.
why it matters
Documents the honesty boundary of the R4 dual-entry coupling work inside the QG Wave B residual DAG. Downstream, the flags theorem reads these three fields and decides they equal (true, true, false), so auditors and completion scripts can machine-check that R4 did not overclaim.
Per the module doc and field comment, R5 is the intended owner of the ledger-named binding in SevenGaps.RecognitionRatioDerived; this status field records that R4 does not own it. The false gap1_bridge_derived flag keeps the larger Gap1 residual open even though the mesh-local conditional ratio theorem is available. No direct T0–T8 forcing-chain step; this is gravity-analysis scaffolding around constitutive coupling and recognition ratio, not a foundation uniqueness result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.