economicPhases
plain-language theorem explainer
economicPhases is defined as the octave period divided by the fundamental tick, producing the integer count of phases per octave. Researchers applying the Recognition Science forcing chain to economic periodicity cite it to connect the eight-tick structure to business-cycle modeling. The definition is a direct division that reduces to eight once the octave is expanded using its upstream relation to the tick unit.
Claim. Define the economic phase count per octave by $8 / 1$, where the numerator is the octave length expressed in units of the fundamental time quantum $τ_0 = 1$ (tick).
background
In Recognition Science the tick $τ_0$ is the fundamental time quantum, normalized to 1 in native units. The octave is the fundamental evolution period, defined as exactly eight ticks and corresponding to the eight-tick octave (T7) in the forcing chain. The LedgerEconomics module uses this ratio to translate the universal octave into an economic phase count. Upstream definitions establish the octave as eight times the tick and the tick as the base unit; the MusicalScale and Constants modules supply the octave value of 2 in ratio form and the tick value of 1.
proof idea
The declaration is a one-line definition that performs the division octave / tick. It relies on the upstream constants that set the octave to eight ticks and the tick to one; no additional lemmas or tactics are required beyond the direct substitution.
why it matters
This definition supplies the phase count that the downstream theorem eight_economic_phases proves equals eight, thereby realizing the T7 eight-tick octave landmark inside economic modeling. It closes the link from the universal forcing chain to ledger conservation and business-cycle bounds. The construction inherits the self-similar structure already fixed by the phi-ladder and the RCL without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.