meshDualEntrySource
plain-language theorem explainer
Signed source strength on a single mesh hinge, obtained by extracting channel 0 from the dual-entry strain state. Gravity analysts cite it when wiring R3 dual-entry data into the R4 DeficitSourceConstitutiveCoupling assembly. The body is a one-line projection: apply extract at the unique Fin 1 index of the dual-entry record built from geometric deficit magnitude and debit/credit leads.
Claim. For a real hinge deformation $h$, the mesh dual-entry source is the signed scalar obtained by extracting channel $0$ from the dual-entry strain state on $\mathrm{Fin}\,1$ whose debit leads when $0<h$, credit leads when $h<0$, and magnitude equals $|\delta(h)|$ (the mesh geometric deficit).
background
Module setting is Wave B residual R4: assemble banked R1 geometric deficit, R2 hinge kappa with source-dominated regime, and R3 dual-entry strain into an inhabited DeficitSourceConstitutiveCoupling on carrier $\mathbb{R}$, then apply the blocker's conditional recognition-ratio derivation. Carrier is reshaped $H=\mathbb{R}$, not an encoded Freudenthal triangulation.
The dual-entry state on one mesh channel records debit-leads for positive deformation, credit-leads for negative, and magnitude equal to the absolute mesh geometric deficit. Convention pins deficit iff debit-leads ($0<h$), mirroring the Regge geometric-deficit convention. Extract pulls the signed source strength off that state at the unique channel index.
Upstream integer-order trichotomy on signed orbits underwrites the case split used later when equating the extract to the constitutive product $\kappa\cdot\delta$. Definitions stay free of $x$-ratio and real log; the log appears only in the final derived-ratio theorem inherited from the blocker.
proof idea
Definitional one-liner. Build the dual-entry strain state at hinge parameter $h$, then project with extract at channel index $0$ (the sole inhabitant of $\mathrm{Fin},1$). No tactics, no lemmas in the body; the mathematical content lives in how the dual-entry record is filled (debit/credit indicators and absolute geometric deficit as magnitude) and in the extract convention of the dual-entry strain API.
why it matters
Supplies the source-strength field for the R4 coupling assembly. Downstream, the coupling definition plugs this extract in as sourceStrength, and the equality theorem proves the extract equals the R2 constitutive product $\kappa\cdot\delta$ by unfolding extract/strain/phi and reducing via $\kappa\equiv 1$. The typed residual then packages existence of a coupling whose kappa, geometric deficit, and source strength match the mesh bank, free of $x$-ratio in the premise fields.
This is the R3-to-R4 handoff in the QG Wave B attack on the DeficitSourceConstitutiveCoupling residual: without a signed source tied to dual-entry leads, the coupling cannot be inhabited and the conditional recognition-ratio derivation cannot fire. It does not flip gap1_bridge_derived and does not introduce a ledger-named standalone recognition-ratio Prop (that is R5); the derived-ratio theorem here remains the conditional application on the assembled coupling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.