HierarchicalLedger
plain-language theorem explainer
A hierarchical ledger packages a geometric scale factor greater than one with a positive level-size sequence that scales uniformly and obeys the two-step composition law level at 2 equals level at 1 plus level at 0. Anyone deriving that hierarchy forces the golden ratio cites this interface. Pure structure definition: data plus four axioms, no proof body.
Claim. A hierarchical ledger consists of a real scale factor $\sigma>1$, a map $\ell:\mathbb{N}\to\mathbb{R}$ with $\ell(k)>0$ for all $k$, the uniform scaling law $\ell(k+1)=\sigma\cdot\ell(k)$ for every $k$, and the composition identity $\ell(2)=\ell(1)+\ell(0)$.
background
In the exclusivity hierarchy module the aim is to show that any ledger with hierarchical structure is forced onto the golden ratio. This structure is the axiomatic package for that argument: an abstract scale greater than one, a positive sequence of level sizes, geometric progression of those sizes, and a single additive composition step at the bottom of the ladder.
Uniform scaling is discrete self-similarity. Composition at levels 0, 1, 2 is the Fibonacci-type relation that, once fed through geometric progression, yields the characteristic equation $\sigma^2=\sigma+1$. Upstream, geometric scales appear as powers of $\varphi$ in large-scale structure constructions, and scale factors appear in recognition-stability audits; here the scale is left free so it can be identified with $\varphi$ later.
proof idea
No proof body: this is a structure definition. It bundles two data fields (scale and level_size) with four propositional fields (scale greater than one, positivity of every level size, uniform multiplicative scaling, and the two-step composition identity). Downstream theorems simply project these fields and rearrange them algebraically.
why it matters
Direct input to hierarchy_forces_fibonacci_recurrence, which derives $\sigma^2=\sigma+1$ from uniform scaling plus composition, and to bridge_B1_hierarchy_implies_phi, which concludes scale equals $\varphi$ by uniqueness of the positive root greater than one. That bridge is the exclusivity step "hierarchical structure implies scale $=\varphi$", using the existing phi-forcing infrastructure. Framework landmark: T6, $\varphi$ as the self-similar fixed point. The structure isolates exactly the discrete self-similarity hypotheses needed before invoking root uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.