pith. sign in
module module high

IndisputableMonolith.Foundation.PhiForcingDerived

show as:
view Lean formalization →

The module defines geometric scale sequences with positive ratio r and derives their J-cost composition laws. It establishes commutativity, associativity, and closure results that force the golden equation with closed ratios equal to phi. Researchers tracing discrete ledgers to self-similar fixed points cite these algebraic derivations. The content proceeds via direct identities on the imported cost structure.

claimA geometric scale sequence is a discrete structure scaled by fixed ratio $r > 0$. Ledger composition is commutative and associative. The J-cost obeys the decomposition $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. Closure conditions force the ratio to satisfy the golden equation.

background

This module sits in the Foundation domain and imports the RS time quantum τ₀ = 1 tick together with the cost structure. It introduces geometric scale sequences as discrete ledgers with constant positive ratio r. Ledger composition is defined to be commutative and associative, while the J-cost function supplies the additive decomposition for independent scales. These objects supply the minimal algebraic data for subsequent closure arguments.

proof idea

The module opens with definitions of the geometric scale sequence and ledger composition. It verifies commutativity and associativity by direct algebraic check. Later lemmas apply the J decomposition identity to show that closure forces the golden equation and that closed ratios equal phi.

why it matters in Recognition Science

These definitions and lemmas feed the Phi Forcing module, which proves φ is forced by self-similarity in a discrete ledger with J-cost. They also supply the discrete geometric ledger required by Hierarchy Minimality for the B1 closure step with scale 0 + scale 1 = scale 2. The Stillness Generative module draws on the ground-state properties established here. The material advances the chain from J-uniqueness to the self-similar fixed point.

scope and limits

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)