mock_orders_coprime_to_8
plain-language theorem explainer
The declaration asserts that the mock theta orders 3, 5, and 7 are each coprime to 8. Researchers modeling Ramanujan's mock theta functions inside the eight-tick Recognition Science framework cite it to confirm these periods generate unclosed windows. The proof reduces to three direct evaluations of the coprimeness predicate via the decide tactic.
Claim. The orders 3, 5, and 7 of Ramanujan's mock theta functions are each coprime to the eight-tick period: $3$ and $8$ share no common divisors greater than $1$, likewise for $5$ and $8$, and for $7$ and $8$.
background
In the Recognition Science setting the eight-tick window is the period-8 octave forced by the self-similar fixed point phi (T7). A true modular form corresponds to a closed window whose net defect is zero; mock theta functions arise when the period is coprime to 8, leaving an unclosed window whose pending balance is identified with phantom magnitude. The module doc-comment states that the orders {3,5,7} are exactly the non-trivial odd numbers less than 8 and that their coprimeness to 8 forces mock rather than true modularity. The upstream theta definition supplies the Cayley transform used in related Riemann-hypothesis work but is not invoked in this proof.
proof idea
The term proof opens with constructor to split the three-way conjunction, then applies the decide tactic to each conjunct. Decide computes the gcd of each pair directly and confirms that each equals 1.
why it matters
The result supplies the coprimeness premise required by the MockThetaPhantomCorrespondence and phantom_completes_to_balanced theorems in the same module. It fills the T7 eight-tick octave step by showing why orders 3, 5, and 7 cannot close inside the window, thereby linking Ramanujan's examples to the phantom-light projection that restores full symmetry. The declaration therefore anchors the RS translation of Zwegers' shadow as the constraint from future balance debt.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.