pith. sign in
module module high

IndisputableMonolith.Econ.LedgerEconomics

show as:
view Lean formalization →

The Econ.LedgerEconomics module applies the eight-tick octave to ledger systems and shows that this structure forces exactly eight economic phases. Researchers extending Recognition Science to cyclic economic models would cite the phase count and associated bounds. The module imports the base time quantum and derives the phase multiplicity plus conservation properties directly from the octave.

claimThe 8-tick octave forces exactly eight economic phases, with business cycle period bounded in an interval derived from the octave and ledger conservation ratio equal to one.

background

The module sits in the Econ domain and imports the fundamental RS time quantum τ₀ = 1 tick from IndisputableMonolith.Constants. It introduces economicPhases as the set of phases induced by the octave, businessCyclePeriod as the duration of one economic cycle, ledgerConservationRatio as the balance preservation factor in ledgers, and octaveGrowthMultiplier as the scaling factor over the full octave. These objects rest on the eight-tick structure of period 2^3.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module realizes the doc-comment claim that the 8-tick octave forces exactly eight economic phases, extending T7 of the forcing chain into economics. It supplies the phase count, positivity, bounds, and conservation equality that later economic applications would build upon, though no downstream theorems are recorded yet.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (11)