recognitionDualEntryEnrichment4DStatus
plain-language theorem explainer
Status triple for Wave B residual R3: dual-entry signed-source enrichment is marked closed, posting-run realization is dropped as garnish, and the gap-1 bridge flag stays false. Gravity auditors cite it as the machine-checkable dashboard for this residual. The body is a pure structure literal with three Boolean fields.
Claim. The R3 enrichment status record is the triple $(\mathsf{r3Closed},\mathsf{postingRunDropped},\mathsf{gap1BridgeDerived}) = (\mathrm{true},\mathrm{true},\mathrm{false})$: dual-entry signed-source enrichment is closed, posting-run realization is omitted, and the gap-1 ledger bridge is not claimed derived.
background
Wave B residual R3 attacks the typed residual for signed-source enrichment in the quantum-gravity completion plan. The bare cost ledger is treated as a derived shadow of the foundational recognition ledger, which carries two signed integer columns (debit and credit) with strain $\phi = \mathrm{debit}-\mathrm{credit}$. The J-cost quotient is even and forgets exactly $\mathrm{sign}(\phi)$; the enrichment restores dual-entry column orientation with nonnegative magnitude and a unit-flux cap.
A global $\mathbb{Z}/2$ convention pins "deficit iff debit-leads," mirroring the Regge sign convention for mesh geometric deficit. Flipping the convention swaps columns and negates strain while leaving the bare J-ledger unchanged. The status structure packages three honesty flags for this residual: whether R3 is closed, whether posting-run realization was dropped, and whether the gap-1 bridge is claimed derived.
proof idea
Definitional structure literal, not a proof. The three Boolean fields of the status record are set by hand: R3 closed to true, posting-run realization dropped to true, gap-1 bridge derived to false. No lemmas are applied; downstream consumers read the fields directly (the companion flags theorem discharges equality by decide).
why it matters
Gives a single named status object for the R3 dual-entry enrichment residual so downstream checks can assert the intended honesty profile without re-reading the module narrative. The immediate consumer is the flags theorem, which proves the three field equalities by decision procedure.
In the Recognition gravity stack this records that the dual-entry enrichment (F2 plus separation of extract-zero, bare projection, swap invariance, and non-factorability) is treated as closed, while posting-run adjacency remains garnish and the gap-1 bridge flag is deliberately left false. It does not touch the forcing chain T0–T8, the Recognition Composition Law, or the $\phi$-ladder mass formula; it is local bookkeeping for the signed-source residual in the QG Wave B attack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.