pith. machine review for the scientific record.
sign in
module module high

IndisputableMonolith.Foundation.HierarchyMinimality

show as:
view Lean formalization →

This module defines the minimal discrete hierarchy as a geometric scale ladder closed under the first non-trivial composition step in a J-cost ledger. Researchers in Recognition Science cite it to ground the emergence of the golden ratio from self-similar discrete structures. It assembles the hierarchy directly from the forcing axioms in the imported PhiForcing and PhiForcingDerived modules.

claimA minimal discrete hierarchy is a geometric sequence of scales $s_k = r^k$ ($k$ integer) closed under the first non-trivial step of the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$.

background

The module sits inside the Recognition Science derivation of physics from a single functional equation. It imports PhiForcing, which shows that φ is forced by self-similarity in a discrete ledger equipped with J-cost, and PhiForcingDerived, which obtains $r^2 = r + 1$ from the axioms of a discrete scale sequence together with additive ledger composition. The supplied doc-comment states the module's object as the minimal discrete hierarchy: a geometric scale ladder closed under the first non-trivial composition step.

proof idea

This is a definition module. It assembles the MinimalHierarchy object and the two sibling statements hierarchy_forces_golden_equation and hierarchy_forces_phi by direct reference to the closure properties already established in the imported PhiForcing modules.

why it matters in Recognition Science

The module supplies the minimal hierarchy definition that HierarchyEmergence consumes to prove that a zero-parameter comparison ledger with multilevel composition necessarily produces a minimal hierarchy and therefore forces φ as the unique admissible scale. It occupies the intermediate position in the T0–T8 forcing chain between the phi derivation and the full emergence theorem.

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)