offset_7_eq_24_inv_mod_7
plain-language theorem explainer
Verification that 24 times 5 is congruent to 1 modulo 7 confirms the offset value for the congruence prime 7 in the Q3 framework. Number theorists studying partition congruences or mock theta functions reference this result when tracing how the directed flux count 24 determines the Ramanujan offsets. The proof reduces to a single arithmetic check performed by the norm_num tactic.
Claim. The modular inverse of 24 modulo 7 equals 5, i.e., $24 · 5 ≡ 1 mod 7$.
background
The module shows that mock theta orders {3,5,7} and congruence primes {5,7,11} both derive from the single number 24 = directed_flux(Q3). Congruence primes are the smallest primes p coprime to 24 with p > 3, and their offsets satisfy offset_p = 24^{-1} mod p. This supplies the explicit offset for p=7 as 5. Upstream structures include the collision-free empirical program and simplicial ledger edge lengths that feed the forcing chain to the Q3 flux count.
proof idea
The proof is a one-line wrapper that applies the norm_num tactic to discharge the arithmetic goal.
why it matters
This result completes the offset computation for the prime 7 within the Q3 unification of Ramanujan congruences. It supports the module claim that offsets {4,5,6} for primes 5,7,11 are determined by the inverse of the directed flux 24. In the Recognition Science framework it ties the eight-tick octave to the arithmetic structure via the phi-ladder and RCL, with 7 arising as the count of non-DC DFT modes in the 8-tick window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.