module module high

`IndisputableMonolith.Mathematics.RamanujanBridge.RamanujanPiFactors`

This module supplies a collection of elementary factorization lemmas for integers that appear in Ramanujan's pi series, such as 396 = 4 × 99 and 9801 = 99² together with primality checks on 1103. It is cited by the RamanujanBridge module to furnish the concrete number-theoretic facts required for mapping Ramanujan's identities onto Recognition Science structures. Each lemma is established by direct algebraic verification or repeated divisibility checks with no external dependencies beyond basic arithmetic.

claim$396 = 4 × 99$, $9801 = 99^2$, $11^2$ divides 9801, 1103 is prime, and 11 does not divide 1103.

background

The module operates inside the RamanujanBridge effort that links Srinivasa Ramanujan's series to Recognition Science. It imports the RS time quantum τ₀ = 1 tick from Constants and the structural derivation of 4π via vertex deficits of the cubic ledger Q₃ from AlphaDerivation. The listed factorizations prepare the integer relations that later map onto the phi-ladder and J-cost constructions of the parent framework.

proof idea

This is a collection of small theorems, each proved by direct computation or repeated application of basic divisibility and squaring rules. No complex tactics or external lemmas beyond arithmetic are used.

why it matters in Recognition Science

The module feeds the RamanujanBridge module whose doc-comment states it provides the formal bridge between Ramanujan's deepest mathematical structures and Recognition Science. It supplies the concrete integer identities needed to interpret Ramanujan's pi approximations inside the RS-native constants derived from the cubic ledger.

scope and limits

Does not derive any new analytic identities or series expansions.
Does not perform the mapping from these integers to RS constants; that step occurs in the parent RamanujanBridge module.
Does not invoke advanced number theory such as modular forms or elliptic integrals.
Does not address physical interpretations or units; those remain in AlphaDerivation and Constants.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Mathematics.RamanujanBridge module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.AlphaDerivation module_import

declarations in this module (19)

theorem three96_eq_4_times_99 L69
theorem three96_factorization L72
theorem factor_11_in_396 L75
theorem eleven_divides_396 L80
theorem nine801_eq_99_sq L85
theorem nine801_eq_9_times_11_sq L88
theorem nine801_eq_81_times_11_sq L91
theorem eleven_sq_divides_9801 L94
theorem factor_passive_sq_in_9801 L97
theorem one103_is_prime L105
theorem eleven_not_div_1103 L108
theorem one03_not_div_1103 L113
def honest_boundary_1103 L120
theorem twenty6390_factorization L127
theorem eleven_not_div_26390 L130
theorem convergence_connection_to_8tick L144
theorem chudnovsky_prefactor_12 L159
structure RamanujanPiCert L165
def ramanujanPiCert L180