meshDualEntryCoupling
plain-language theorem explainer
Assembles the mesh dual-entry constitutive coupling on the real carrier: hinge channels, hinge kappa, geometric deficit, dual-entry source strength, and mesh scale, plus the source-dominated inequality. Gravity analysts cite it as the R4 package that feeds the conditional recognition-ratio bound and closes the typed residual for deficit-source coupling from enrichment. The body is a structure instance wiring banked R1–R3 components, with one short rewrite for source domination.
Claim. The mesh dual-entry constitutive coupling is the inhabited structure on $\mathbb{R}$ with hinge channel count $N$, positivity of $N$, hinge constitutive factor $\kappa$, mesh geometric deficit $\delta$, dual-entry source strength $S$, the identity $S(h)=\kappa(h)\,\delta(h)$ for all $h$, positive mesh scale, and the source-dominated bound at every carrier point. The assembly uses only banked mesh geometry and dual-entry extract data; it does not mention $x$-ratio or $\log$.
background
Wave B residual R4 packages a full DeficitSourceConstitutiveCoupling on the reshaped carrier $H=\mathbb{R}$. The module goal is to inhabit that structure from already-banked pieces, then hand it to the blocker's conditional recognition-ratio lemma. Carrier is not an encoded Freudenthal triangulation; that lift remains open upstream.
Geometric deficit is the signed Regge-convention star deficit as a function of the deformation parameter, built from squared-edge and dihedral geometry, with no $x$-ratio or log in the definition. Hinge channels and hinge kappa (with source domination) are the R2 bank. Dual-entry source strength is the extract of the dual-entry strain state at index 0; the companion equality proves that extract equals the constitutive product $\kappa,\delta$ by trichotomy on the deformation parameter (and $\kappa\equiv 1$ on this mesh).
Convention: deficit iff debit-leads ($0<h$), mirroring the Regge convention pin for the geometric deficit. Definitions stay free of ratio fields; log appears only later in derived-ratio statements inherited from the blocker.
proof idea
Structure instance, not a deep proof. Fields are filled by name: channels and positivity from hinge channels; kappa from hinge kappa; geometric deficit from the banked mesh deficit; source strength and its equality from the dual-entry extract and the extract-equals-$\kappa\delta$ theorem; mesh scale and positivity from the hinge mesh-scale bank.
The only tactic block is source_dominated: introduce the carrier point, rewrite the source via the extract equality, then apply the banked hinge-kappa source-domination lemma. No new analysis is performed here.
why it matters
This is the R4 assembly step in the QG Wave B attack on the typed residual for deficit-source constitutive coupling from enrichment. Downstream, the conditional recognition-ratio theorem applies the blocker lemma to this coupling and obtains the log-ratio bound by channels over six. The residual-closed theorem exhibits this coupling as the witness that discharges R4.
Further downstream, the ledger-named recognition-ratio Prop (derivation half of the gap-1 bridge) exists over a dual-entry enrichment equal to the mesh dual entry and a coupling equal to this assembly; the holds theorem inhabits that Prop with this coupling plus the blocker inequality and the minimizer-strain identification. Honesty scope is explicit: this does not flip gap1_bridge_derived (R6 still needs R0a, R0b, and R5), and it is not itself the ledger-named standalone ratio binding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.