recognitionDualEntryEnrichment4DStatus_flags
plain-language theorem explainer
Status flags for the R3 dual-entry signed-source enrichment: R3 is marked closed, posting-run realization is dropped, and the gap-1 bridge remains underived. Gravity analysts tracking Wave B residual closure cite this snapshot. The proof is a one-line decidability check against the hardcoded status record.
Claim. The dual-entry enrichment status record asserts that residual R3 is closed, that posting-run realization has been dropped, and that the gap-1 bridge is not derived: $r_3\mathrm{Closed}=\mathrm{true}$, $\mathrm{postingRunRealizationDropped}=\mathrm{true}$, and $\mathrm{gap1BridgeDerived}=\mathrm{false}$.
background
Wave B residual R3 enriches the bare cost ledger by restoring dual-entry orientation. The foundational recognition ledger carries signed columns debit and credit with $\phi=\mathrm{debit}-\mathrm{credit}$; the J-cost quotient is even and forgets $\mathrm{sign}(\phi)$. The enrichment is a dual-entry strain state with integer debit/credit, nonnegative magnitude, and a unit-flux cap.
A single global $\mathbb{Z}/2$ convention pins deficit to debit-leads (the ledger mirror of the Regge sign convention). Flipping it swaps columns and negates $\phi$ and strain while leaving the bare J-ledger unchanged.
The status record is a three-boolean snapshot of what this module claims to have closed versus left open. Upstream, that record is defined with the three literals checked here.
proof idea
One-line wrapper: decide evaluates the three boolean equalities against the definition of the status record, whose fields are the literals true, true, and false. No algebraic lemmas are needed.
why it matters
Pins an honest progress flag for Wave B residual R3 in the gravity analysis stack. The module doc states explicitly that R3 enrichment does not flip the gap-1 bridge flag and drops posting-run realization (F3 / ledger posting adjacency) as garnish; load-bearing content is F2 plus separation (a)(b)(c). Downstream consumers of residual-DAG status can read these three bits without re-auditing the enrichment constructions. No parent theorems currently depend on this flag theorem; it is a closure marker for the QG full-completion session rather than a step in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.