pi6_excess
plain-language theorem explainer
π^6 cannot equal π raised to the configuration space dimension because that dimension is fixed at five. Derivations of the fine structure constant correction cite this to fix the exponent in the curvature integral. The proof reduces the assumed equality to a numerical contradiction after taking logarithms and applying linear arithmetic.
Claim. $π^6 ≠ π^5$ in the reals, where the exponent 5 is the effective dimension of the ledger configuration space for curvature integration.
background
The Curvature Space Derivation module shows why the curvature correction δ_κ = -103/(102π^5) in the fine-structure constant formula uses π^5 rather than another power. The configuration space dimension is defined as 5 and arises from three spatial dimensions (forced by D=3), one temporal dimension from the eight-tick cycle, and one dual-balance dimension from the conservation constraint σ. This is the effective dimension over which the mismatch between spherical and cubic geometries integrates in the ledger phase space.
proof idea
The tactic proof unfolds configSpaceDim to obtain the concrete exponent 5. It assumes π^6 = π^5, applies the logarithm to both sides, simplifies the resulting equation with the power rule for logarithms, cancels the positive factor log π, and reaches the false equality 6 = 5, which linarith refutes.
why it matters
This result fixes the exponent in the curvature term of the alpha inverse derivation. It rests on the Recognition Science forcing chain (T8 for D=3 spatial dimensions, T7 for the eight-tick octave, and the balance constraint) that produces exactly five dimensions. No downstream uses are recorded, so the theorem functions as an internal consistency check within the constants module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.