GeometricScaleSequence
plain-language theorem explainer
GeometricScaleSequence encodes a discrete geometric ladder of scales with common ratio r > 0 and r ≠ 1, where the nth scale equals r raised to n. Researchers deriving the golden ratio from ledger closure axioms in Recognition Science cite it to model uniform scale ladders. The definition is a structure declaration with a direct power definition for scale and a positivity lemma obtained by unfolding and applying pow_pos.
Claim. A structure consisting of a real number $r > 0$ with $r ≠ 1$, together with the sequence of scales $s_n = r^n$ for each natural number $n$.
background
This module derives the equation $r^2 = r + 1$ from three axioms: a discrete geometric scale sequence, additive ledger composition when recognition events combine, and closure under composition. The J-cost function $J(x) = ½(x + 1/x) - 1$ is additive for independent events, which motivates treating scales as additive under composition rather than multiplicative. Upstream results include the scale definition $phi^k$ in LargeScaleStructureFromRS and the total J-cost definition in ObservabilityLimits.
proof idea
The structure is introduced directly by its three fields: ratio, ratio_pos, and ratio_ne_one. The scale function is defined by direct exponentiation as ratio raised to n. The scale_pos lemma unfolds the scale definition and applies the pow_pos lemma from Mathlib to conclude positivity for every n.
why it matters
This structure supplies the discrete scale sequence axiom used in hierarchy_emergence_forces_phi and ledger_forces_phi, which derive that the ratio equals phi from uniform scale ladder plus additive closure. It fills the first axiom in the module's derivation of the golden ratio equation and is instantiated to build MinimalHierarchy and RealizedClosedScaleModel. It connects to the T5 J-uniqueness and T6 phi fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.