tierThreshold_ratio
plain-language theorem explainer
The theorem establishes that consecutive thresholds on the civilizational complexity ladder differ by the factor phi squared. Archaeologists or complexity theorists modeling Turchin-style tiers via Z-rungs would cite the result to confirm the self-similar scaling built into Recognition Science. The proof is a short term-mode calculation that substitutes the explicit threshold formula, invokes positivity, rewrites the division, and finishes with ring.
Claim. For every natural number $k$, let $T(k) = 100 phi^{2k}$ be the population threshold for complexity tier $k$. Then $T(k+1)/T(k) = phi^2$.
background
The module models civilizational complexity as the Z-rung of a societal recognition substrate, adopting five tiers (band, tribe, chiefdom, state, empire) drawn from Bondarenko and aligned with Turchin's 0-50 cultural complexity scale. The upstream definition supplies the explicit form tierThreshold(k) := 100 * phi^(2*k), which encodes the Recognition Science claim that adjacent tiers scale by phi squared, consistent with the phi-ladder self-similarity.
proof idea
The term proof unfolds tierThreshold to replace both numerator and denominator with their explicit expressions. It establishes positivity of the denominator via mul_pos and pow_pos, rewrites the target equality with div_eq_iff, and lets ring perform the algebraic cancellation to phi^2.
why it matters
The result populates the phi_sq_ratio field inside the civilizationCert definition, which certifies the five-tier structure. It directly realizes the module's stated RS prediction that adjacent tier thresholds stand in the ratio phi^2, closing one link from the phi-ladder to archaeological observables with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.