eleven_divides_396
plain-language theorem explainer
11 divides 396 in the natural numbers. Researchers working on Ramanujan's 1914 series for 1/π cite this fact when confirming that the factor 11 appears in the denominator 396^{4n}. The proof is a direct term-mode construction supplying the quotient 36 and invoking norm_num to verify the product.
Claim. $11$ divides $396$ in the natural numbers.
background
Recognition Science assigns the integer 11 to the passive field edges of the three-dimensional recognition space Q₃. The module RamanujanPiFactors places this factor inside the denominator of Ramanujan's series 1/π = (2√2/9801) Σ (4n)!(1103 + 26390n)/((n!)^4 396^{4n}), where 396 = 2² × 3² × 11. The local setting is the RS decipherment of the classical series, which converges at roughly eight decimal digits per term and is tied to the eight-tick octave structure that forces π as the recognition-circle constant.
proof idea
The proof is a one-line term proof. It constructs the witness pair ⟨36, by norm_num⟩, where the equality 11 * 36 = 396 is discharged by the norm_num tactic with no additional lemmas.
why it matters
This theorem supplies the divisibility fact required by the RamanujanPiCert structure, which packages all RS connections in the π-series. It directly supports the claim that 11 = passive_field_edges D for D = 3 appears in the denominators. The result closes one link in the chain from the forcing sequence T8 (D = 3) to the observed integers in Ramanujan's formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.