Pith. sign in
module module high

IndisputableMonolith.Constants.AlphaGenesis.CurvatureJCostVerdict

show as:
view Lean formalization →

Module that defines the genuine quadratic recognition cost of the cube's eight vertex curvature deficits and proves it equals π². It then compares that cost to the Gauss–Bonnet total, the cubic-ledger seed 4π·11, and the measured α⁻¹ band. Anyone auditing the AlphaGenesis seed assembly cites it to separate forced J-cost geometry from the open infrared identification. Proofs are short algebraic reductions from the J-cost Hessian coefficient 1/2.

claimThe genuine quadratic recognition cost of the cube is $8 \cdot \tfrac12 \cdot (\pi/2)^2 = \pi^2$, using the J-cost quadratic coefficient $1/2$ on each of the eight vertex deficits $\delta = \pi/2$. This cost is strictly less than the Gauss–Bonnet total, far below the cubic seed $4\pi \cdot 11$, and far below the measured $\alpha^{-1}$ band.

background

Recognition Science forces the cost functional $J$ uniquely (T5). Near equilibrium the local expansion is exact: $J(1+\varepsilon)=\varepsilon^2/(2(1+\varepsilon))$, so the quadratic coefficient is $1/2$ (module JCostHessianC7). On the cube each of the eight vertices carries angular deficit $\delta=\pi/2$.

AlphaDerivation assembles the seed $4\pi\cdot 11$ from cubic-ledger combinatorics. Its own doc states that this is "NOT a first-principles derivation of the measured fine-structure constant" and that exact $\alpha^{-1}(0)$ remains an open boundary condition. The present module isolates the pure geometric J-cost piece of that story.

AlphaBounds supplies interval machinery for $\alpha^{-1}$ comparisons used in the far-below lemmas.

proof idea

Define cubeCurvatureJCost as the sum $8\cdot(1/2)\cdot(\pi/2)^2$. The equality to $\pi^2$ is pure arithmetic. The three comparison lemmas (genuine cost less than Gauss–Bonnet, seed far above genuine cost, genuine cost far below $\alpha^{-1}$) are short inequalities chaining that closed form to the known numerical seed and the AlphaBounds intervals. A small inductive type CurvatureCostVerdict packages the three inequalities; curvatureCostVerdict is the constructed witness.

why it matters in Recognition Science

Inside Constants.AlphaGenesis this module is the honest geometric ledger for cube curvature: it shows what the forced J-cost actually contributes ($\pi^2$) and that this contribution sits far below both the combinatorial seed $4\pi\cdot 11$ and the measured $\alpha^{-1}$ window. Downstream AlphaGenesis audit pages rely on that separation when they refuse to identify the seed with the infrared coupling. The module therefore closes a scaffolding gap between T5 J-uniqueness / the Hessian C7 expansion and the still-open exact $\alpha^{-1}(0)$ boundary condition flagged in AlphaDerivation. No parent theorems currently import it (used_by empty); it is a leaf verdict for human and machine audit.

scope and limits

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (7)