two_pi_not_D3
plain-language theorem explainer
2π equals the circumference of the unit circle in two dimensions but cannot serve as the surface measure of the unit sphere in three dimensions. Researchers deriving the fine structure constant from Recognition Science would cite this to exclude 2π as the isotropic prefactor. The tactic proof assumes equality, cancels the nonzero factor π, and reaches the absurdity 2=4 via linear arithmetic.
Claim. $2π ≠ 4π$ in the reals, where $2π$ is the circumference of the unit circle in D=2 while $4π$ is the solid angle of the unit sphere in D=3.
background
The module proves that the geometric seed factor 4π in the α derivation is uniquely fixed by isotropic coupling in D=3. The surface area of the unit (D-1)-sphere is given by $S_{D-1} = 2π^{D/2}/Γ(D/2)$, which evaluates to exactly 4π when D=3. This follows from the forcing chain that sets spatial dimensionality to three and requires rotationally invariant ledger coupling.
proof idea
The tactic proof introduces the equality assumption, records that π is nonzero from its positivity, cancels the common nonzero multiplier to obtain 2=4, and refutes the result with norm_num.
why it matters
This lemma secures the exclusivity of 4π as the D=3 solid angle in the α derivation α^{-1} = 4π·11 - f_gap - δ_κ. It directly implements the module's claim that 4π is forced by isotropy and T8 dimensionality rather than the D=2 circumference 2π. No downstream theorems depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.