couplingS
plain-language theorem explainer
Extracts the rational edge-pair coupling weight as the ratio of integer numerator to natural denominator. Gravity analysts cite it when assembling quartic Bloch-symbol coefficients and the exact midpoint m² TT identity in 4D Regge calculus. The body is a one-line cast of num/den into ℚ.
Claim. Given a unit-cell edge-pair coupling with integer numerator $n$ and natural denominator $d$, its coupling weight is the rational $s = n/d \in \mathbb{Q}$.
background
The ambient module closes the exact midpoint Bloch $m^2$ TT identity in 4D Regge calculus (script-backed kernel certs and numerical assembly). A Coupling is one unit-cell edge-pair entry for the exact midpoint Bloch symbol: integer num, natural den, and integer 4-vectors De, Dep (doubled midpoint offsets).
The field s on the data structure is noncomputable in the section, so this definition supplies the computable rational weight used in all subsequent coefficient sums. The same ratio appears in the zero-momentum Bloch-symbol module; here it is restated so the midpoint $m^2$ identity file is self-contained.
proof idea
Pure definition: cast coup.num and coup.den to $\mathbb{Q}$ and form the quotient. No lemmas, tactics, or proof obligations.
why it matters
Feeds every place that needs a rational coupling weight in the 4D midpoint pipeline: couplingS_eq_s (identifies it with the data field s), couplingMonomial and qCoeff (quartic zero-momentum symbol coefficients $Q_{abcd}$), couplingWeight_eq_quartic, and the midpoint-side m2Coeff / exactMidpointBlochM2_eq_biquad that close exact_midpoint_m2_tt_identity.
In the broader RS gravity stack this is bookkeeping, not a forcing-chain step: it makes the edge-pair table of the Regge Hessian symbol fully computable over $\mathbb{Q}$ so the TT-sector $m^2$ identity can be certified exactly rather than numerically.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.