meshHingeMeshScale
plain-language theorem explainer
The positive mesh scale is fixed at π/2 so four bridge channels times this scale recover the uniform angular deficit bound 2π. Gravity analysts cite it when discharging source-dominated admissibility for the unit hinge coupling against star geometry. The body is a one-line real constant assignment, not a derived identity.
Claim. Define the positive mesh scale by $S := \pi/2$. With channel count $4$, one has $4S = 2\pi$, matching the uniform bound on absolute star angular deficit.
background
This module closes Wave B residual R2 for hinge-level constitutive data in the 4D recognition mesh. The geometric side is already reshaped to a real carrier: the mesh geometric deficit equals the star deficit built from arcsin data. Absolute arcsin is at most $\pi/2$, so the absolute star deficit is at most $2\pi$ once the flat angle sum is $2\pi$.
Source-dominated admissibility asks for a positive mesh scale $S$ and a positive channel count $N$ such that $|\kappa(h),\delta(h)| \le N,S$ at every carrier point. Here the hinge coupling is the banked unit map $\kappa\equiv 1$ (definitionally free of $x$-ratio and log), and $N=4$ is the bridge channel count. Choosing $S=\pi/2$ makes $N S=2\pi$ sit exactly on the geometric ceiling.
The same package is later assembled into the dual-entry constitutive coupling and into the typed residual that records R2 closed, still without claiming continuum Einstein-scale join.
proof idea
Definitional one-liner: assign the real constant $\pi/2$. No lemmas fire at the definition site. Positivity is proved downstream by unfolding and a positivity tactic; the source-dominated inequality rewrites the unit coupling to $1$, multiplies, and compares absolute deficit to $4\cdot(\pi/2)=2\pi$.
why it matters
R2 needs a concrete positive mesh scale so the unit hinge coupling meets the source-dominated bound shape against R1 star geometry. This constant is that scale: $4\cdot(\pi/2)=2\pi$ matches the uniform deficit bound from $|\arcsin|\le\pi/2$.
Downstream, positivity of the scale, the source-dominated theorem for unit $\kappa$, and the closed typed residual for hinge-kappa identification all consume it. The dual-entry coupling assembly (R4) also wires this scale into the full DeficitSourceConstitutiveCoupling record, still free of $x$-ratio and log.
Framework role is local constitutive packaging for the recognition mesh, not a new forcing-chain step. Continuum Einstein-scale join of hinge-local unit coupling to Einstein $\kappa$ remains open, as the module records.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.