curvature_gauge_invariant
plain-language theorem explainer
The theorem asserts that the constant expression 103/(102 π^5) equals itself for arbitrary nonzero real scalars α and k. A researcher examining gauge invariance of dimensionless quantities in Recognition Science would cite it when separating rescaling freedoms from physical parameters. The proof is a one-line reflexivity that discards the unused gauge parameters.
Claim. For all real numbers $α ≠ 0$ and $k ≠ 0$, the equality $103/(102 π^5) = 103/(102 π^5)$ holds.
background
The module distinguishes gauge freedoms (rescalings of the form p → αp + b and J → kJ) from tunable parameters. Dimensionless outputs such as α^{-1} remain unchanged once all gauge factors cancel, analogous to the invariance of the fine-structure constant across unit systems. Upstream results supply supporting structures on empirical programs, simplicial edge lengths, and mechanism design, yet the present statement relies only on syntactic identity.
proof idea
The term-mode proof introduces the four quantified variables and applies reflexivity (rfl). Because both sides of the displayed equality are identical constants, the tactic succeeds without invoking any of the upstream lemmas.
why it matters
The result closes one concrete instance of the gauge-versus-parameter objection in Gap 3. It feeds the module's main claim that α^{-1} is fully gauge-invariant and aligns with the framework's treatment of rescaling symmetries as physically irrelevant. No open scaffolding remains for this specific equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.