meshDualEntry
plain-language theorem explainer
Builds the dual-entry strain state on one mesh channel from a real deformation h: debit-leads when h>0, credit-leads when h<0, magnitude equal to the absolute mesh geometric deficit. Gravity analysts cite it as the R3/R4 carrier that feeds the constitutive coupling and the recognition-ratio derivation. Field proofs are abs-nonneg plus trichotomy on the sign of h.
Claim. For each real deformation parameter $h$, the dual-entry strain state on a single channel ($\mathrm{Fin}\,1$) has debit $1$ if $h>0$ and $0$ otherwise, credit $1$ if $h<0$ and $0$ otherwise, and nonnegative magnitude equal to the absolute mesh geometric deficit $|\delta_{\mathrm{mesh}}(h)|$, with unit flux on that channel.
background
Wave B residual R4 assembles three banked pieces into an inhabited deficit-source constitutive coupling on the real carrier $H=\mathbb{R}$: the mesh geometric deficit $\delta_{\mathrm{mesh}}$ (R1), hinge stiffness $\kappa$ with source-domination (R2), and a dual-entry strain state (R3). Dual-entry bookkeeping records debit-lead versus credit-lead on each channel together with a magnitude; the convention is deficit iff debit-leads ($0<h$), mirroring the Regge star-deficit sign convention.
Upstream, meshGeometricDeficit is the signed Regge-convention star deficit built from squared-edge and dihedral geometry, with no log or ratio field in its definition. The present definition packages that deficit's absolute value as the dual-entry magnitude on the unique channel indexed by $\mathrm{Fin},1$.
The module does not flip the gap-1 bridge flag and does not bind a ledger-named standalone recognition-ratio Prop (that is R5). The carrier remains the reshaped real line from R1/R2, not an encoded Freudenthal triangulation.
proof idea
Structure definition, not a derived theorem. Debit and credit are indicator functions of $h>0$ and $h<0$ respectively (integer-valued). Magnitude is $|\mathrm{meshGeometricDeficit},h|$; nonnegativity is abs_nonneg.
The only nontrivial field is unit flux: case-split on $0<h$, then on $h<0$. In the positive branch, $h\not<0$ follows from le_of_lt, and simp closes debit/credit exclusivity. Negative and zero branches are symmetric simp discharges. No external mesh lemmas beyond the deficit symbol itself.
why it matters
This is the dual-entry enrichment that R4 and R5 inhabit. Downstream, the extracted source meshDualEntrySource is defined as the dual-entry extract on channel 0, and meshDualEntrySource_eq proves it equals the R2 constitutive product $\kappa(h)\cdot\delta_{\mathrm{mesh}}(h)$ by unfolding and $\kappa\equiv 1$.
Further downstream, the ledger Prop recognition_ratio_derived existentially quantifies over an enrichment equal pointwise to this dual-entry map and a coupling equal to the mesh dual-entry coupling; recognition_ratio_derived_holds closes R5 by supplying exactly meshDualEntry and meshDualEntryCoupling as witnesses, then applying the blocker's conditional recognition-ratio inequality and the minimizer-strain identification.
In the Recognition gravity stack this is the concrete dual-entry state that turns banked geometric deficit into a constitutive source without introducing $x$-ratio or $\log$ at definition time (logs appear only in the inherited derived-ratio theorem).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.