meshDualEntrySource_eq
plain-language theorem explainer
The dual-entry source extracted from the mesh strain state equals the constitutive product κ(h)·δ(h) for every real hinge parameter h. Gravity analysts assembling the R4 DeficitSourceConstitutiveCoupling cite this identity to wire the dual-entry ledger extract into the banked R2 product. The proof unfolds the extract, reduces κ to 1, and closes by trichotomy on the sign of h using the geometric-deficit sign lemmas.
Claim. For every real $h$, the dual-entry source extracted from the mesh dual-entry strain state at $h$ equals the product of the mesh hinge coupling $\kappa(h)$ and the mesh geometric deficit $\delta(h)$: $\mathrm{source}(h)=\kappa(h)\,\delta(h)$.
background
This module closes Wave B residual R4 for quantum-gravity completion work: assemble banked R1 (mesh geometric deficit $\delta$), R2 (mesh hinge $\kappa$ with source-dominated regime), and R3 (dual-entry strain state) into an inhabited DeficitSourceConstitutiveCoupling on the carrier $H=\mathbb{R}$.
The dual-entry strain state packages debit/credit channels, a sign field $\phi\in{\pm 1}$, and a strain magnitude built from $|\delta|$. The source map is the extract of that strain; the constitutive claim is that this extract coincides with the R2 product $\kappa\cdot\delta$. Convention: deficit means debit-leads ($0<h$), mirroring the Regge-side geometric-deficit convention pinned upstream.
Definitions stay free of $x$-ratio and $\log$; those appear only later in the derived-ratio theorem inherited from the blocker. The hinge coupling is definitionally one on this mesh (meshHingeKappa_eq_one), so the identity is really source $=\delta$ after the unit factor.
proof idea
Unfold the source extract through the dual-entry strain fields (strain, $\phi$, and the mesh dual-entry constructor). Rewrite $\kappa(h)=1$ and cancel the unit factor via one_mul, leaving an equality between the extracted strain and $\delta(h)$.
Case-split on the trichotomy of $h$ relative to $0$. For $h<0$: debit off, credit on, $\phi=-1$, so strain $=-|\delta|$; the geometric-deficit sign lemma gives $\delta<0$, hence $|\delta|=-\delta$ and strain $=\delta$. For $h=0$: flat deficit vanishes and absolute value is zero. For $h>0$: debit on, credit off, $\phi=+1$, strain $=|\delta|$; positivity of $\delta$ yields $|\delta|=\delta$. Each branch finishes by simplification under the sign hypotheses.
why it matters
This identity is the algebraic hinge of R4 assembly. Downstream, meshDualEntryCoupling builds a full DeficitSourceConstitutiveCoupling on $\mathbb{R}$ by taking channels and $\kappa$ from the hinge bank, geometric deficit from R1, and source from the dual-entry extract; the field equations of that structure need source $=\kappa\cdot\delta$, which is exactly this theorem.
With the coupling inhabited, the module can apply the blocker's conditional recognition_ratio_derived_of_deficit_source_coupling to obtain mesh_recognition_ratio_derived without smuggling $x$-ratio or $\log$ into the definitions. That is the Wave B attack path on the typed residual TypedResidual_DeficitSourceConstitutiveCoupling_from_enrichment.
It does not close the larger gap-1 bridge, does not bind a ledger-named standalone recognition-ratio proposition (that is R5), and leaves R0a/R0b name-bindings and the encoded Freudenthal lift open. Within those limits it is the proved constitutive match that lets the dual-entry ledger talk to the mesh deficit product.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.