RamanujanPiCert
plain-language theorem explainer
RamanujanPiCert packages the D=3 topological integers into the factors of Ramanujan's 1914 π-series. Researchers connecting Recognition Science geometry to classical series would cite it to confirm that passive edges equal 11, total edges equal 12, and vertices equal 8 appear in 396 and 9801. The declaration is a structure that directly records upstream theorems from AlphaDerivation together with the factorization lemmas eleven_divides_396 and eleven_sq_divides_9801.
Claim. A structure $R$ such that $R$ asserts passive field edges in dimension 3 equal 11, 11 divides 396, $11^2$ divides 9801, 1103 is prime, cube edges in dimension 3 equal 12, and cube vertices in dimension 3 equal 8.
background
Recognition Science obtains π from the recognition circle forced by the eight-tick octave (T7). The module studies Ramanujan's series 1/π = (2√2/9801) Σₙ (4n)!(1103 + 26390n) / ((n!)^4 × 396^{4n}) and shows that the integers 396 and 9801 contain the RS topological count 11. passive_field_edges(d) is defined as cube_edges(d) minus active edges per tick; at D=3 this equals 11 by the theorem passive_edges_at_D3. cube_edges(d) := d · 2^{d-1} and cube_vertices(d) := 2^d are the standard hypercube counts used throughout AlphaDerivation.
proof idea
The declaration is a structure definition whose fields are direct references to upstream results: passive_11 from passive_edges_at_D3, edges_12 from edges_at_D3, vertices_8 from vertices_at_D3, div_396 from eleven_divides_396, div_9801 from eleven_sq_divides_9801, and prime_1103 from one103_is_prime. No additional tactics or reductions are performed.
why it matters
The structure supplies the certificate required by the downstream definition ramanujanPiCert, thereby embedding the D=3 counts (T8) into the Ramanujan denominators. The module documentation states that 1103 remains outside RS integers and originates from the class-number theory of Q(√−163). It therefore closes one concrete link between the Recognition Composition Law geometry and a classical series while leaving open whether the full set of Ramanujan constants admits an RS interpretation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.