mock_orders_require_multiple_windows
plain-language theorem explainer
The theorem shows that the minimum number of 8-tick windows required to close a periodic pattern equals 3 for order 3, 5 for order 5 and 7 for order 7, hence strictly exceeds one in each case. Researchers modeling Ramanujan mock theta functions inside Recognition Science would cite it to separate mock modular symmetry from true modular forms. The proof is a direct simplification that invokes the three explicit window-count equalities already proved for these orders.
Claim. Let $w(k) = $ lcm$(k,8)/8$ be the minimum number of complete 8-tick windows needed for a $k$-periodic pattern to complete one full cycle. Then $w(3) > 1$, $w(5) > 1$ and $w(7) > 1$.
background
The module interprets mock theta functions as partition functions of unresolved phase debt inside unclosed 8-tick windows. A true modular form corresponds to a perfectly balanced 8-tick window whose sum is zero; a mock theta function describes a configuration whose compensating balance has not yet arrived. The auxiliary definition min_windows_to_close(k) returns Nat.lcm(k,8)/8 and equals k precisely when gcd(k,8)=1. Upstream theorems already fix the values: min_windows_to_close 3 = 3, min_windows_to_close 5 = 5 and min_windows_to_close 7 = 7.
proof idea
The proof is a one-line simplification that substitutes the three upstream equalities min_windows_to_close 3 = 3, min_windows_to_close 5 = 5 and min_windows_to_close 7 = 7; each equality is visibly greater than 1, so the conjunction follows at once.
why it matters
The result isolates the structural reason odd-prime orders generate mock rather than true modular symmetry. It sits immediately downstream of min_windows_to_close and the three order-specific window theorems. Within the Recognition Science framework it supports the reading of mock theta functions as carriers of phantom balance debt across multiple 8-tick octaves (T7), explaining why their transformation law fails to close after a single window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.