Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.RecognitionMeshDualEntryCoupling4D

show as:
view Lean formalization →

Packages the Wave B R4 mesh dual-entry coupling: a single-channel (Fin 1) ledger state whose sign tracks deformation and whose magnitude is the absolute geometric deficit. Gravity and QG auditors cite it when closing the deficit–source constitutive link without an external xRatio. The module wires enrichment, geometric deficit, and hinge-kappa imports into an inhabited coupling and residual-closure receipts.

claimOn a single mesh channel, the dual-entry state is debit-leading when the deformation is positive and credit-leading when negative, with magnitude equal to the absolute mesh geometric deficit $|\Delta_{\mathrm{geom}}(h)|$. The module supplies the inhabited coupling between that dual-entry source and the constitutive residual, together with equality and residual-closure lemmas that identify the coupling with the enrichment schema.

background

Wave B of the QG residual DAG attacks typed residuals that previously blocked a ledger-native recognition ratio. Residual R1 identifies the mesh geometric deficit; R2 supplies hinge kappa under source-dominated admissibility; R3 builds dual-entry signed-source enrichment. This module is the R4 layer that couples those pieces on a one-channel mesh.

Dual-entry here is bookkeeping language for a signed source: positive deformation posts a debit-leading entry, negative deformation a credit-leading entry, both sized by $|\mathrm{meshGeometricDeficit}, h|$. The construction deliberately avoids an external $x$-ratio parameter; the magnitude is taken from the geometric deficit already fixed upstream.

Imports are exactly the three Wave B analysis modules (enrichment, geometric deficit, hinge kappa). Downstream, the inhabited meshDualEntryCoupling is what the recognition-ratio packaging and the axiom audit consume.

proof idea

Definition-first module with thin equality and residual wrappers. It introduces the dual-entry state and source on Fin 1, proves the source equals the signed absolute geometric deficit, and packages an inhabited coupling object. Residual theorems then discharge the typed deficit–source constitutive coupling from the enrichment schema (open and closed forms), plus decoy lemmas that separate magnitude-only impostors from the genuine mesh geometric deficit. No deep new analysis: the work is wiring R1–R3 into a named R4 coupling.

why it matters in Recognition Science

Closes Wave B residual R4 so that R5 can name a ledger recognition_ratio_derived. Downstream RecognitionRatioDerived packages this module's inhabited coupling with the blocker's conditional derivation and the stationarity minimizer receipt under the exact Prop demanded by FullTheoryBenchmarks.gap1_bridge_derived. The audit module requires headline theorems here to print within [propext, Classical.choice, Quot.sound] only.

In the broader Recognition stack this is constitutive bookkeeping for mesh gravity, not a new force law: it makes the signed source and geometric deficit speak the same dual-entry language so the recognition ratio can be derived rather than postulated. It sits after the forcing-chain geometry (eight-tick, $D=3$) has already fixed the mesh setting, and before SevenGaps claims the bridge as derived.

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)