typedResidual_DeficitSourceConstitutiveCoupling_from_enrichment_closed
plain-language theorem explainer
R4 is closed: a deficit-source constitutive coupling on the reals exists whose hinge stiffness, geometric deficit, and dual-entry source match the banked mesh data, with source equal to kappa times deficit, positive mesh scale, source dominated by channels times scale, and at least one channel. Gravity analysts on the QG Wave B residual DAG cite this as the inhabited coupling residual. The proof is a short term construction packaging the pre-assembled mesh dual-entry coupling and reading off its field equalities and inequalities.
Claim. There exists a deficit-source constitutive coupling $C$ on $\mathbb{R}$ such that the hinge stiffness of $C$ equals the mesh hinge kappa, the geometric deficit of $C$ equals the mesh geometric deficit, the source strength of $C$ equals the mesh dual-entry source, source strength equals kappa times geometric deficit at every state, the mesh scale is positive, absolute source strength is bounded by (number of channels) times mesh scale, and the number of channels is at least one.
background
Wave B of the QG full-completion session attacks the residual that a deficit-source constitutive coupling can be assembled from enrichment data. The carrier is the reshaped real line $H = \mathbb{R}$ from the geometric-deficit and hinge-kappa banks (R1/R2), not an encoded Freudenthal triangulation. Convention: deficit means debit-leads ($0 < h$), mirroring the Regge-side geometric-deficit convention.
A deficit-source constitutive coupling packages channels, hinge stiffness $\kappa$, geometric deficit, source strength, and mesh scale, together with positivity and domination bounds. The dual-entry enrichment (R3) supplies the source extract; R1 and R2 supply geometric deficit, hinge kappa, channels, and mesh scale. The assembly is definitionally free of $x$-ratio and real logarithm; those appear only later in the derived-ratio theorem inherited from the blocker.
Upstream, the mesh dual-entry coupling is the concrete structure with channels and kappa from the hinge bank, geometric deficit from the mesh geometric-deficit bank, and source from the dual-entry extract, already carrying source_eq and source_dominated.
proof idea
Term-mode existence proof. Refine with the pre-assembled mesh dual-entry coupling as the witness $C$, then discharge the seven conjuncts of the residual Prop: three definitional equalities (kappa, geometric deficit, source strength) by rfl against the structure fields; source_eq by the coupling's source-equality lemma; mesh-scale positivity by the coupling's positivity field; source domination by the coupling's domination lemma; and channels at least one by the coupling's channels-positivity field. No new analysis is performed; the residual is exactly the inhabited packaging of banked R1–R3 data.
why it matters
Closes residual R4 in the Wave B attack on the typed residual for deficit-source constitutive coupling from enrichment (QG Wave B Gap1 residual DAG). Downstream, the capitalized status theorem is a one-line re-export of this result, marking the residual closed in the module's status block.
In the Recognition gravity stack this is the coupling that feeds the blocker's conditional recognition-ratio derivation: once the coupling is inhabited, recognition_ratio_derived_of_deficit_source_coupling yields the mesh recognition-ratio theorem. It does not itself flip gap1_bridge_derived, and it does not introduce a ledger-named standalone recognition-ratio Prop (that is R5). R0a/R0b validation name-bindings and the encoded Freudenthal lift remain open upstream. Framework-wise it sits in the gravity analysis layer that turns eight-tick / $D=3$ mesh geometry into constitutive source-deficit balance, without yet touching the alpha band or mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.