TypedResidual_DeficitSourceConstitutiveCoupling_from_enrichment_closed
plain-language theorem explainer
Existence of a deficit–source constitutive coupling on the real hinge carrier is settled by assembling mesh geometric deficit, hinge stiffness, and dual-entry source into one inhabited structure. Gravity analysts closing Wave B residual R4 cite this. The proof is a one-line term that applies the constructive witness packaging that dual-entry mesh coupling.
Claim. There exists a deficit–source constitutive coupling $C$ over $\mathbb{R}$ such that $C$'s stiffness equals the mesh hinge kappa, $C$'s geometric deficit equals the mesh geometric deficit, $C$'s source strength equals the dual-entry mesh source, source equals stiffness times geometric deficit pointwise, the mesh scale is positive, $|\mathrm{source}|$ is dominated by channels times mesh scale, and the channel count is at least one.
background
Wave B residual R4 in the quantum-gravity completion stack targets an inhabited deficit–source constitutive coupling on the reshaped real hinge carrier $H=\mathbb{R}$. The coupling packages three banked pieces: the mesh geometric deficit (R1, Regge-style hinge deficit $2\pi-\sum\theta$ in the debit-leads convention), mesh hinge kappa with source-domination (R2), and the dual-entry strain state (R3).
The residual Prop asserts existence of such a $C$ with fixed field equalities (kappa, geometric deficit, source), the constitutive law $\mathrm{source}=\kappa\cdot\mathrm{deficit}$ pointwise, positive mesh scale, channel-wise source bound, and at least one channel. Premise fields stay free of ratio logarithms; the log appears only later in the derived-ratio theorem inherited from the blocker.
Upstream geometry supplies hinge deficit as $2\pi-\sum\theta$ (dihedral and Schläfli forms). The constructive sibling builds the concrete dual-entry mesh coupling and discharges the equalities and bounds by reflexivity and the coupling's own source-equality and source-domination lemmas.
proof idea
One-line term-mode wrapper: the claim is definitionally the residual Prop, and the proof is exactly the already-proved constructive theorem that inhabits it.
That constructive theorem refines an existential with the dual-entry mesh coupling as witness, closes the three field equalities by rfl, inserts the coupling's pointwise source-equality lemma, the positive mesh-scale fact, the source-domination bound, and the positive channel count. No new algebra is done at this declaration.
why it matters
Closes Wave B residual R4 on the QG gap-1 residual DAG: the enrichment-plus-R1/R2 assembly is no longer a bare Prop, but a proved inhabited coupling. Downstream the module applies the blocker's conditional recognition-ratio derivation to this coupling, yielding the mesh recognition-ratio theorem (still conditional on the assembled coupling, not a ledger-named standalone ratio Prop).
Per the module honesty note, this does not flip the gap-1 bridge flag, does not bind a standalone recognition-ratio Prop (that is R5), and keeps the carrier as reshaped $\mathbb{R}$ rather than an encoded Freudenthal triangulation. R0a/R0b validation name-bindings remain open. No used-by edges are recorded yet; the immediate consumer is the in-module derived-ratio application that needs an inhabited coupling of this shape.
Framework-wise this is constitutive bookkeeping for recognition gravity on a 4D mesh, not a forcing-chain (T0–T8) step; it supplies the deficit–source link that later ratio and ledger bridges expect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.