pith. sign in
module module moderate

IndisputableMonolith.Foundation.PhiForcingDerived

show as:
view Lean formalization →

This module defines the geometric scale sequence with positive ratio r and derives lemmas on ledger composition and J-cost properties under self-similarity. Researchers working on discrete ledgers in Recognition Science cite it to establish the algebraic prerequisites for forcing the golden ratio. The module organizes core definitions of sequences, ledgerCompose, and J, followed by lemmas on commutativity, associativity, and closure conditions that imply the golden equation.

claimA geometric scale sequence is a sequence \((s_n)_{n \in \mathbb{Z}}\) satisfying \(s_{n+1} = r \cdot s_n\) for fixed ratio \(r > 0\).

background

The module sits in the foundation layer and imports the RS time quantum (\tau_0 = 1) tick together with the J-cost structure. It introduces the geometric scale sequence as the basic discrete object for modeling self-similar scaling. Additional definitions cover ledgerCompose for combining scales at different levels and the J function satisfying the recognition composition law together with its decomposition and additivity for independent elements.

proof idea

The module first defines the geometric scale sequence and the J function, then proves commutativity and associativity of ledgerCompose, followed by lemmas establishing that closure forces the golden equation and that the closed ratio equals phi.

why it matters in Recognition Science

This module supplies the geometric scale sequence and J-composition lemmas that feed the PhiForcing module, which proves that (\phi) is forced by self-similarity in a discrete ledger with J-cost. It also supplies the minimal algebraic hierarchy data used by HierarchyMinimality and contributes to the T0–T8 derivation chain in StillnessGenerative. It fills the step between basic cost structure and the forcing of the golden ratio at landmarks T5 and T6.

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (14)