Pith. sign in
module module high

IndisputableMonolith.Gravity.Analysis.RecognitionMeshDualEntryCoupling4D

show as:
view Lean formalization →

Packages the Wave B R4 mesh dual-entry coupling: a single-channel (Fin 1) dual-entry state whose sign tracks deformation (debit-leads when positive, credit-leads when negative) with magnitude equal to the absolute mesh geometric deficit. Gravity and QG auditors cite it as the inhabited constitutive link between deficit, hinge kappa, and signed-source enrichment. The module assembles upstream R1–R3 objects into the coupling and residual-closure receipts used by the recognition-ratio derivation.

claimOn a single mesh channel, the dual-entry state has magnitude $|\mathrm{meshGeometricDeficit}(h)|$, with debit-leading sign when the deformation is positive and credit-leading sign when negative. The mesh dual-entry coupling is the inhabited constitutive map tying this signed source to the geometric deficit and hinge-$\kappa$ data, discharging the deficit–source constitutive residual from the dual-entry enrichment.

background

Wave B of the QG residual DAG closes Gap-1 style bridge residuals without an external $x$-ratio. Upstream R1 identifies the mesh geometric deficit; R2 supplies hinge $\kappa$ under source-dominated admissibility; R3 builds the dual-entry signed-source enrichment schema. This module sits at R4: it puts those pieces on one mesh channel ($\mathrm{Fin},1$).

Dual-entry bookkeeping means the ledger records a debit-leading or credit-leading entry according to the sign of the deformation, while the size of the entry is fixed by the absolute geometric deficit. The coupling object is the constitutive link that says the signed source is not free data but is determined by that deficit (and the hinge admissibility already proved upstream).

Local setting is 4D recognition-mesh gravity analysis: residuals are typed, and enrichment is required to stay inside the dual-entry discipline rather than a magnitude-only decoy.

proof idea

Definition-first assembly, then residual discharge. The module defines the dual-entry state and its source projection, proves the source equals the signed absolute deficit, and packages meshDualEntryCoupling as the inhabited coupling. Typed residual theorems then show the deficit–source constitutive coupling follows from the R3 enrichment (with a closed variant). Adversarial decoy lemmas separate the genuine dual-entry object from magnitude-only impostors. Status markers record the Wave B R4 closure for audits.

why it matters in Recognition Science

R4 is the missing constitutive hinge between geometry and ledger source before the recognition ratio can be named. Downstream, RecognitionRatioDerived (Wave B R5) packages this inhabited meshDualEntryCoupling with the blocker's conditional derivation and the stationarity minimizer receipt under the exact ledger proposition gap1_bridge_derived. The dual-entry enrichment audit module imports it so headline theorems stay inside [propext, Classical.choice, Quot.sound]. In the broader RS gravity stack this is the mesh-side step that turns identified deficit and hinge $\kappa$ into a signed source fit for the recognition-ratio bridge, rather than an under-specified enrichment schema.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (13)