Pith. sign in
module module high

IndisputableMonolith.Foundation.HierarchyMinimality

show as:
view Lean formalization →

Defines the minimal discrete hierarchy: a geometric scale ladder closed under the first nontrivial composition step. Anyone tracing why self-similarity forces the golden ratio cites this package. The module packages the hierarchy structure and proves that any such ladder satisfies the golden equation and therefore pins the unique positive scale factor to φ.

claimA minimal discrete hierarchy is a geometric scale ladder $\{1, r, r^2, \ldots\}$ closed under the first nontrivial composition step. Any such hierarchy forces the golden equation $r^2 = r + 1$, and hence the unique admissible positive scale is $\varphi = (1+\sqrt{5})/2$.

background

Recognition Science builds physics from a discrete ledger equipped with a J-cost. Upstream, PhiForcing shows that self-similarity in such a ledger forces φ; PhiForcingDerived derives the golden equation $r^2 = r + 1$ from three axioms: a discrete geometric scale sequence, additive ledger composition (scales add when recognition events combine, because the ledger tracks total recognition work), and a closure condition under the first nontrivial composition.

This module isolates the hierarchy object itself: the smallest geometric ladder that is closed under that composition step. The local setting is pure foundation work before the full T0–T8 forcing chain; the only structural input is the discrete scale sequence and the additive composition law already fixed upstream.

proof idea

The module introduces a structure MinimalHierarchy capturing a geometric ladder closed under the first nontrivial composition. Two theorems then discharge the forcing: one shows any such hierarchy satisfies the golden equation $r^2 = r + 1$ by matching the additive composition of scales against the geometric progression; the other specializes the unique positive root to $\varphi$. The argument is algebraic reduction from the upstream closure axioms, not a new analytic construction.

why it matters in Recognition Science

HierarchyEmergence imports this module to prove that a zero-parameter comparison ledger with multilevel composition necessarily produces a minimal hierarchy and hence forces φ as the unique admissible scale. UnifiedForcingChain uses it inside the absolute-floor argument that all of T0–T8 are inevitabilities from the cost foundation (Recognition Composition Law), with T6 the landmark that φ is the self-similar fixed point. Verification.Exclusivity.HierarchyTheorem also depends on it for the exclusivity side of the hierarchy claim. Without a clean minimal-hierarchy package, the later emergence and forcing-chain modules would have to re-derive the golden equation inline.

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 (3)