meshHingeKappa
plain-language theorem explainer
The mesh hinge coupling is the constant unit map on the reals: every hinge is scaled by 1. Gravity analysts cite it when assembling the deficit-source constitutive coupling and when excluding decoy kappas that vanish or smuggle recognition ratios. It is the banked unit-coupling pattern from stationarity-bridge closure, definitionally free of log and ratio dependence.
Claim. The mesh hinge coupling is the constant function $\kappa:\mathbb{R}\to\mathbb{R}$ defined by $\kappa(h)=1$ for every real hinge parameter $h$.
background
Wave B residual R2 in the QG completion session targets hinge kappa with a source-dominated admissibility bound and no recognition ratio in the coupling. The DAG draft asked for a kappa on a hinge carrier built from RS/mesh constitutive data; Lean has no separate hinge carrier type, so R1 already reshaped the carrier to $\mathbb{R}$ via the geometric deficit identified with the star deficit.
The honest binding used here packages the banked unit coupling of the concrete stationarity-bridge pattern (stationarity-bridge closure forces kappa equal to 1 everywhere). Named constitutive data, not a free field: definitionally free of ratio and real logarithm. Geometric side comes from R1; mesh context conjoins the exact-J/true-Regge-Hessian identification and flat star angle sum $2\pi$.
Admissibility content lives in sibling theorems: $|\kappa,\delta|$ bounded by channels times mesh scale, with four bridge channels and mesh scale $\pi/2>0$, using $|\arcsin|\le\pi/2$ so the star deficit is at most $2\pi$ in absolute value.
proof idea
Definitional packaging only: the constant function sending every real argument to $1$. No lemmas, no tactics; the body is the unit map that stationarity-bridge closure already names as the constitutive hinge coupling.
why it matters
Supplies the kappa field for the R4 dual-entry constitutive coupling assembly (meshDualEntryCoupling), where channels, geometric deficit, and mesh scale come from banked R1/R2 and source from dual-entry extract. Downstream, the dual-entry source is proved equal to the product $\kappa,\delta$ by reducing through the unit identity. The typed residual for deficit-source constitutive coupling from enrichment requires this same named kappa.
Sibling decoys use it as the target that zero kappa fails (nontriviality) and that log-ratio-over-deficit cannot match on a punctured interval (oddness of the geometric deficit versus constant 1). The theorem content around this definition is the source-dominated inequality, nontriviality, and decoy package; continuum Einstein-scale join of hinge-local unit coupling versus Einstein-scale kappa remains open. Does not flip the gap-1 bridge-derived flag and does not yet inhabit the full signed-source constitutive structure (needs R3 enrichment).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.