modes_from_8_tick
plain-language theorem explainer
Eight-tick phase patterns fix the set of available modes for heat capacity calculations in Recognition Science. A physicist deriving quantum corrections to equipartition from the fundamental octave would cite this when counting active modes above the Planck threshold. The proof is a one-line triviality that registers the 8-tick structure without further reduction.
Claim. The modes available for thermal excitation are those selected by the eight-tick phase patterns, with activation when $T > hbar omega / k_B$ and suppression otherwise.
background
The Thermodynamics.HeatCapacity module derives heat capacity from 8-tick mode counting. Heat capacity is defined as $C_V = (partial U / partial T)_V$, with the classical limit each quadratic mode contributing $kT/2$. In Recognition Science each spatial direction admits eight phases, but only active modes above the temperature threshold contribute. The upstream tick is the fundamental time quantum $tau_0 = 1$, and the eight-tick octave is the fundamental evolution period of length eight ticks. Modes themselves are finite sets obtained by Galerkin truncation in two dimensions.
proof idea
The proof is a one-line wrapper that applies trivial to establish the proposition that eight-tick phases determine available modes.
why it matters
This declaration anchors mode counting in the eight-tick octave (T7) of the forcing chain. It supports later derivations of monatomicCv and diatomicCv within the same module by supplying the discrete phase structure that yields the Planck distribution for single-mode energy. The result connects the Recognition framework's discrete time quantum directly to thermodynamic observables without invoking the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.