RecognitionMeshDualEntryCoupling4DStatus
plain-language theorem explainer
Status record for Wave B residual R4: the mesh dual-entry deficit-source constitutive coupling in four dimensions. Three boolean flags track whether R4 closed, whether the ledger-named recognition-ratio binding stays open (owned by R5), and whether the gap-1 bridge is derived. Auditors cite the inhabited instance to read completion without claiming gap1_bridge_derived. Pure structure definition; no proof content.
Claim. A status package with three boolean fields: (i) whether the R4 mesh dual-entry coupling assembly is closed; (ii) whether the ledger-named recognition-ratio derived binding remains open (deferred to residual R5); (iii) whether the gap-1 bridge has been derived.
background
This module is Wave B residual R4 in the quantum-gravity completion attack on the typed residual DeficitSourceConstitutiveCoupling from enrichment. It assembles banked pieces: R1 mesh geometric deficit, R2 mesh hinge kappa with source-domination, and R3 dual-entry strain state, into an inhabited deficit-source constitutive coupling on the carrier $H = \mathbb{R}$, then applies the blocker's conditional recognition-ratio derivation.
The module is deliberately narrow. It does not own a ledger-named standalone recognition-ratio Prop (that binding is residual R5). It does not flip the gap-1 bridge flag. The carrier is the reshaped real line from R1/R2, not an encoded Freudenthal triangulation; upstream encodedFreudenthalLiftOpen stays true. R0a/R0b validation name-bindings remain open. Convention: deficit iff debit-leads ($0 < h$), mirroring the Regge convention for the mesh geometric deficit.
Upstream status objects in discrete Lichnerowicz and four-tet signed deficit similarly package proved-vs-open flags (flat TT convergence proved, curved background open; N=5 torus extension closed). This structure follows that audit pattern for the dual-entry coupling residual.
proof idea
No proof. The declaration is a structure type with three Bool fields. The inhabited value in the same module sets R4 closed to true, ledger-binding open to true, and gap-1 bridge derived to false, matching the honesty scope of the residual.
why it matters
Gives a machine-readable completion snapshot for residual R4 so downstream audits can distinguish what this module closed from what it deliberately left open. The sole direct consumer is the inhabited status value recognitionMeshDualEntryCoupling4DStatus, whose doc-comment states that R5 lands the ledger-named binding in SevenGaps.RecognitionRatioDerived and that R4 itself does not own that binding.
In the Recognition gravity stack this residual sits on the path from mesh geometric deficit and hinge kappa through dual-entry strain to a constitutive coupling that feeds the conditional recognition-ratio theorem. Framework landmarks nearby include the forcing chain's $D=3$ and eight-tick octave (period $2^3$), and the discrete-to-continuum Lichnerowicz work on the flat 3-torus TT sector; none of those are discharged here. The open items recorded by the flags (ledger binding, gap-1 bridge, Freudenthal lift, R0a/R0b) are the residual DAG's next targets, not claims of this structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.