eight_pi_not_unit
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.