eleven_sq_divides_9801
plain-language theorem explainer
11 squared divides 9801. Researchers tracing Recognition Science integers into Ramanujan's 1/π series cite this to confirm the squared passive-edge factor in the denominator. The proof is a direct term that supplies the quotient 81 and lets norm_num certify the multiplication.
Claim. $11^2$ divides 9801, where 11 is the count of passive field edges for spatial dimension 3.
background
The module deciphers the integers appearing in Ramanujan's 1914 series for 1/π, specifically the factor 9801 in the denominator. Recognition Science reads 9801 as 99 squared with 99 = 9 × 11, and 11 supplied by the passive field edges of the three-dimensional cube graph. Upstream, passive_field_edges d is defined as cube_edges d minus active_edges_per_tick; its doc-comment states that for D=3 the value equals 11 and these edges dress the interaction.
proof idea
Term-mode proof that directly constructs the witness 81 for the divisor relation and invokes norm_num to confirm 9801 = 81 × 121.
why it matters
Supplies the squared-divisibility fact required by the RamanujanPiCert structure that packages all RS connections inside Ramanujan's π-series. It instantiates the forcing-chain result that D equals 3 and passive edges equal 11, thereby placing the topological integer E_passive inside an efficiently convergent series for 1/π. The surrounding module notes that 1103 stays prime and is not claimed to be an RS integer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.