hierarchy_forced_gives_phi
plain-language theorem explainer
A nontrivial multilevel composition with uniform adjacent ratios, base ratio exceeding one, and additive composition at the second level forces the extracted scale ratio to equal the golden ratio φ. Researchers closing zero-parameter derivations of physical constants cite this when linking forced hierarchies to self-similar fixed points. The proof is a direct one-line application of the emergence-forces-phi result to the uniform ladder constructed from the input data.
Claim. Let $M$ be a nontrivial multilevel composition (a map from natural numbers to positive reals with at least three levels). If adjacent ratios are identical for all levels, the base ratio satisfies $M(1)/M(0)>1$, and additivity holds as $M(2)=M(1)+M(0)$, then the ratio of the induced uniform scale ladder equals the golden ratio $φ$.
background
NontrivialMultilevelComposition is a structure requiring a levels map from naturals to positive reals together with positivity and the existence of at least three levels. The module addresses Gap 2 of the axiom-closure plan: deriving hierarchical structure from a zero-parameter ledger. UniformScaleLadder is the target type produced by hierarchy_forced; it packages a constant ratio together with the level sequence. The upstream result hierarchy_emergence_forces_phi states that any UniformScaleLadder obeying additive closure at the base levels has ratio exactly φ.
proof idea
One-line wrapper that applies hierarchy_emergence_forces_phi to the UniformScaleLadder returned by hierarchy_forced (using the no-free-scale and ratio-gt-one hypotheses) together with the supplied additive equation.
why it matters
The declaration completes the forcing step for the scale ratio inside the HierarchyForcing module, directly supplying the self-similar fixed point φ required by the Recognition Science chain (T6). It feeds the derivation of constants such as ħ = φ^{-5} and the alpha band by converting the abstract uniform ladder into a concrete numerical ratio. No downstream uses are recorded yet; the result remains internal to the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.