eight_pi_not_unit
The declaration shows that 8π cannot serve as the surface measure of the unit sphere in three dimensions. Researchers deriving the fine-structure constant in Recognition Science cite it to rule out alternative normalization factors when fixing the isotropic seed for D=3. The tactic proof assumes equality, cancels the nonzero factor π, reduces to the absurdity 8=4, and closes by norm_num.
claimThe surface measure of the unit sphere in three-dimensional Euclidean space satisfies $4pi neq 8pi$.
background
The module establishes that the geometric seed in the inverse fine-structure constant must be exactly 4π because this is the total solid angle of the unit sphere in D=3. The general formula for the surface area of the (D-1)-sphere is $S_{D-1}=2pi^{D/2}/Gamma(D/2)$; substitution of D=3 yields 4π after simplification with Gamma(3/2)=sqrt(pi)/2. This normalization is required by isotropy of recognition coupling together with integration to the passive-edge count of eleven.
proof idea
The proof is a direct contradiction. Assume 8π=4π. Because π>0 the right-multiplication cancellation lemma yields 8=4. Linarith produces the equality and norm_num registers the numerical falsehood.
why it matters in Recognition Science
The result belongs to the final exclusivity block that forces 4π as the unique admissible factor in the α seed for D=3. It supports the main claim that the solid-angle normalization is fixed by isotropy, the eleven passive edges, and the eight-tick structure already derived from the forcing chain. No downstream declarations are recorded, indicating the lemma is used internally to close the constant derivation.
scope and limits
- Does not claim that 8π never appears as a surface measure for any sphere.
- Does not derive the general solid-angle formula.
- Does not address higher-dimensional cases or non-Euclidean geometries.
formal statement (Lean)
135theorem eight_pi_not_unit : 8 * Real.pi ≠ 4 * Real.pi := by
proof body
Tactic-mode proof.
136 intro h
137 have hpi_ne : Real.pi ≠ 0 := ne_of_gt Real.pi_pos
138 have : (8 : ℝ) = 4 := by
139 have := mul_right_cancel₀ hpi_ne h
140 linarith
141 norm_num at this
142
143/-! ## Part 5: The Complete Exclusivity Proof -/
144
145/-- **Main Theorem**: 4π is the unique geometric factor in the α seed for D=3. -/