pith. sign in
theorem

hierarchy_emergence_forces_phi

proved
show as:

Why this theorem is linked from Language-driven Semantic Segmentation unclear

Pith linked this Lean declaration because the review connected a specific passage in the paper to this theorem. The relation tag says how strong that connection is; it is not a generic placeholder.

This allows LSeg to generalize to previously unseen categories at test time, without retraining or even requiring a single additional training sample.

Relation between the paper passage and the cited Recognition theorem.

module
IndisputableMonolith.Foundation.HierarchyEmergence
domain
Foundation
line
95 · github
papers citing
133 papers (below)

plain-language theorem explainer

A uniform scale ladder with additive closure at level 2 forces the scaling ratio to equal the golden ratio φ. Recognition Science derivations of the self-similar fixed point cite this as the unconditional bridge from zero-parameter multilevel composition to the unique admissible scale. The proof builds a GeometricScaleSequence, confirms closure via the locality theorem plus linear arithmetic, and invokes the uniqueness result for closed ratios.

Claim. Let $L$ be a uniform scale ladder: a sequence of positive real level sizes with uniform scaling ratio $σ > 1$. If the levels obey additive closure $L_2 = L_1 + L_0$, then $σ = φ$ where $φ = (1 + √5)/2$.

background

The HierarchyEmergence module shows that a zero-parameter comparison ledger with multilevel composition produces a minimal hierarchy and forces φ as the unique admissible scale. UniformScaleLadder is the structure of positive level sizes with a single uniform ratio σ > 1 between adjacent levels, extracted from composition without free parameters. Locality_forces_additive_composition establishes that additive closure at the second level implies the quadratic relation σ² = σ + 1. Closed_ratio_is_phi then identifies the unique positive solution as φ.

proof idea

The tactic proof constructs a GeometricScaleSequence S from the ladder's ratio and positivity data. It proves S.isClosed by unfolding the closure predicate, applying locality_forces_additive_composition to recover the recurrence, and discharging the resulting arithmetic with nlinarith. The final step applies closed_ratio_is_phi to conclude the ratio equals φ.

why it matters

This theorem is the core unconditional bridge B1 inside HierarchyEmergence. It feeds directly into bridge_T5_T6 (the T5→T6 link in the forcing chain), realized_hierarchy_forces_phi, hierarchy_forced_gives_phi, and posting_extensivity_forces_phi. The result realizes the module's fourth step: minimal nondegenerate closure forces the Fibonacci recurrence, hence σ² = σ + 1 and σ = φ, aligning with T6 where φ is forced as the self-similar fixed point.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.