pith. sign in
module module high

IndisputableMonolith.Mathematics.RamanujanBridge

show as:
view Lean formalization →

The RamanujanBridge module aggregates eight submodules that map Ramanujan's mock theta functions, partition congruences, continued fractions, pi series, and the number 24 onto Recognition Science structures via J-cost and the phi-ladder. Number theorists and mathematical physicists working on q-series would cite it. The module itself is an organizational collection with no internal proofs.

claimThe Ramanujan bridge unifies mock theta functions of orders \{3,5,7\} with partition congruences for primes \{5,7,11\}, continued fraction evaluations to \phi, and \pi-series denominators through the J-cost function and \phi-ladder stability.

background

Recognition Science starts from the J-cost J(x) = (x + x^{-1})/2 - 1 and forces \phi as the self-similar fixed point, with the eight-tick octave and D=3 emerging later. The RamanujanBridge module sits in the mathematics domain and imports submodules that each resolve one classical Ramanujan mystery by recasting it in these RS terms.

The imported modules supply the following settings. CongruenceQ3Bridge notes that classical mathematics proves but does not explain from a single principle the mock theta orders {3,5,7} and partition congruences for primes {5,7,11}. ContinuedFractionPhi records Ramanujan's nested fractions that evaluate to expressions in \phi. DirectedFlux24 treats the exponent 24 in the modular discriminant \Delta(\tau) = \eta(\tau)^{24}. MockThetaPhantom addresses the structured error in mock theta functions. PhiLadderStability explains the "differ by at least 2" condition in Rogers-Ramanujan. RamanujanPiFactors places the topological integers in Ramanujan's 1/\pi series.

proof idea

This is a definition module, no proofs. The overall structure is the aggregation of the eight imported bridges (PhiLadderStability, DirectedFlux24, RamanujanPiFactors, MockThetaPhantom, ContinuedFractionPhi, ZeckendorfJCost, CongruenceQ3Bridge) that each translate one Ramanujan phenomenon into J-cost or phi-ladder language.

why it matters in Recognition Science

The module supplies the mathematical layer that feeds the UnifiedForcingChain (T5 J-uniqueness, T6 phi fixed point, T7 eight-tick octave, T8 D=3) by giving RS-native accounts of Ramanujan's results. It supports later derivations of constants such as \alpha^{-1} in (137.030,137.039) and the mass formula on the phi-ladder. No direct downstream theorems are listed.

scope and limits

depends on (7)

Lean names referenced from this declaration's body.