pith. sign in
module module high

IndisputableMonolith.Foundation.HierarchyMinimality

show as:
view Lean formalization →

This module defines a minimal discrete hierarchy as a geometric scale ladder closed under the first non-trivial composition step. Researchers tracing the origin of the golden ratio in Recognition Science cite it to connect self-similar ledgers to scale closure. The construction assembles directly from the discrete sequence and additive composition axioms supplied by the imported PhiForcing modules.

claimA minimal discrete hierarchy is a geometric scale sequence $1, r, r^2, r^3, ...$ that remains closed under the first non-trivial additive composition step of the ledger.

background

The module sits inside the Recognition Science foundation layer and imports the self-similarity argument from PhiForcing together with the three-axiom derivation of $r^2 = r + 1$ from PhiForcingDerived. Those upstream results start from a discrete ledger equipped with J-cost and impose self-similarity plus additive composition of recognition work. The local convention is that scales form a geometric progression closed at the lowest non-trivial level of composition.

proof idea

This is a definition module, no proofs. It introduces the MinimalHierarchy object and records the two immediate corollaries hierarchy_forces_golden_equation and hierarchy_forces_phi that follow from the imported axioms.

why it matters in Recognition Science

The module supplies the minimal hierarchy object required by the downstream HierarchyEmergence result, which shows that any zero-parameter comparison ledger with multilevel composition must produce exactly this structure and therefore forces φ as the unique admissible scale. It occupies the slot between the self-similarity forcing of T6 and the emergence of the full hierarchy in the T0–T8 chain.

scope and limits

used by (1)

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)