chudnovsky_prefactor_12
plain-language theorem explainer
The declaration equates the prefactor 12 in the Chudnovsky series for 1/π to the edge count of the three-dimensional hypercube. Number theorists and Recognition Science researchers linking Ramanujan series to geometric topology would cite this result. The proof consists of a direct one-line application of the prior theorem edges_at_D3 that computes cube_edges D for D equal to 3.
Claim. The edge count of the three-dimensional hypercube, defined by $d · 2^{d-1}$, equals 12.
background
In Recognition Science the hypercube edge count is defined as cube_edges(d) := d * 2^{d-1}. For spatial dimension D=3 this evaluates to 12. The module places this integer in the context of the Chudnovsky series prefactor, where 12 multiplies the sum involving factorials and the constant 640320 derived from the Heegner number 163. Upstream the definition cube_edges and the theorem edges_at_D3 establish the numerical value for D=3 via native_decide.
proof idea
The proof is a one-line wrapper that applies the theorem edges_at_D3 from AlphaDerivation.
why it matters
This result supplies the geometric interpretation of the prefactor 12 in the Chudnovsky series as the edge count of Q_3, consistent with T8 forcing D=3 spatial dimensions. It bridges the Ramanujan π-series to the Recognition Composition Law and the eight-tick octave structure. No immediate parent theorems appear in the used_by graph, leaving open further integration into mass formulas or alpha derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.