Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PhiForcingDerived

show as:
view Lean formalization →

Derived algebraic core that forces the golden ratio from a self-similar discrete geometric ledger equipped with J-cost. It defines geometric scale sequences, ledger composition, and the closure identity that pins the scale ratio to φ. Downstream modules (PhiForcing, UnifiedForcingChain, HierarchyMinimality, CostProjectorGolden) import this as the forcing substrate for T6. The argument reduces self-similarity plus additive J decomposition to the golden equation.

claimA geometric scale sequence with ratio $r>0$ carries a commutative, associative ledger composition. Under the minimal closure that scale $0$ plus scale $1$ equals scale $2$, the ratio satisfies the golden equation and equals $\varphi=(1+\sqrt{5})/2$. The cost $J$ decomposes additively on independent factors and motivates that composition law.

background

Recognition Science builds physics from a single cost functional $J$ on positive reals. The unique symmetric cost (T5) is $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$, and obeys the Recognition Composition Law. Constants and Cost supply the RS-native units and the $J$ infrastructure this module reuses.

A geometric scale sequence is a discrete ladder of scales with fixed ratio $r>0$. Ledger composition is the algebraic operation that combines two such scales; the module records that this operation is commutative and associative. Self-similarity means the ledger can reference itself at different rungs of the ladder.

The local setting is the B1-style hierarchy data later isolated in HierarchyMinimality: a discrete geometric ledger together with the smallest closure condition (scale $0$ + scale $1$ = scale $2$). That closure is what turns an arbitrary positive ratio into a fixed-point equation for $\varphi$.

proof idea

The module is a derived-lemma pack, not a single theorem. It first introduces geometric scale sequences and the ledger composition operation, then proves commutativity and associativity of that operation. Closure of the first three scales is rewritten as an algebraic identity in the ratio $r$; solving yields the golden equation, so any closed ratio equals $\varphi$.

Parallel lemmas treat $J$: a composition decomposition, additivity on independent factors, and a short motivation that additive $J$-cost selects the ledger composition law. The package is capped by a completeness statement that the self-similar discrete ledger with $J$-cost forces $\varphi$. Downstream importers treat these as the algebraic substrate rather than re-proving the golden fixed-point step.

why it matters in Recognition Science

This module is the derived algebraic engine behind T6 in the forcing chain: $\varphi$ as the self-similar fixed point. PhiForcing imports it to state that $\varphi$ is forced by self-similarity in a discrete ledger with $J$-cost. UnifiedForcingChain and TMinus1ToT8Bridge pull the same material into the public T-1 through T8 spine, where T6 sits between J-uniqueness (T5) and the eight-tick octave (T7).

HierarchyMinimality reuses the minimal ledger-plus-closure data for the B1 step. CostProjectorGolden sits one layer up: once projectors force golden operators on the Hessian side, the ratio pinned here is the same $\varphi$ that appears in the golden operator algebra. Without this pack, each of those parents would have to re-derive the golden equation from scale closure and $J$-additivity.

scope and limits

used by (5)

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)