MinimalHierarchy
plain-language theorem explainer
MinimalHierarchy packages a geometric scale sequence with its minimal closure under the first additive composition step. Researchers deriving the golden ratio from zero-parameter ladders in the B1 bridge cite this structure when passing from uniform scales to the forced ratio. The declaration is a direct structure bundling the sequence data with the isClosed predicate and carries no proof obligations.
Claim. A minimal hierarchy consists of a geometric scale sequence with positive ratio $r > 0$, $r ≠ 1$, together with the condition that the sequence is closed under the first non-trivial composition step (scale 0 + scale 1 = scale 2).
background
The HierarchyMinimality module isolates the smallest algebraic data required for the B1 closure step: a discrete geometric ledger equipped with the minimal closure condition scale 0 + scale 1 = scale 2. GeometricScaleSequence is the upstream structure supplying a ratio field together with the positivity and non-triviality hypotheses 0 < ratio and ratio ≠ 1. The local setting treats this package as the input to theorems that extract the self-similar fixed point from additive closure alone.
proof idea
The declaration is a structure definition that directly bundles the GeometricScaleSequence field with the minimalClosure predicate. No lemmas are applied and no tactics are invoked; the object is assembled by field assignment.
why it matters
MinimalHierarchy supplies the data type consumed by hierarchy_forces_phi and ledger_forces_phi, which conclude that the ratio equals φ. It implements the B1 step in the forcing chain where phi is forced as the unique positive self-similar fixed point. The structure therefore sits immediately upstream of the golden-equation extraction and the emergence theorems that derive φ from ledger primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.