two_pi_not_D3
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 in Recognition Science
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.
scope and limits
- Does not derive the general solid-angle formula for arbitrary D.
- Does not address non-Euclidean or curved manifolds.
- Does not connect to the phi-ladder or J-cost definitions.
- Does not treat the gap or passive-edge corrections in the alpha formula.
formal statement (Lean)
126theorem two_pi_not_D3 : 2 * Real.pi ≠ 4 * Real.pi := by
proof body
Tactic-mode proof.
127 intro h
128 have hpi_ne : Real.pi ≠ 0 := ne_of_gt Real.pi_pos
129 have : (2 : ℝ) = 4 := by
130 have := mul_right_cancel₀ hpi_ne h
131 linarith
132 norm_num at this
133
134/-- 8π is the surface of a sphere with radius √2, not the unit sphere. -/