tierThreshold_pos
plain-language theorem explainer
The theorem establishes that the tier threshold function, defined as 100 times phi to the power of twice the tier index, is strictly positive for every natural number tier index. Archaeologists modeling societal complexity scales in Recognition Science would cite this to confirm that all tier thresholds lie above zero. The proof is a direct one-line wrapper applying the mul_pos lemma to the positivity of the constant 100 and the power of phi.
Claim. For every natural number $k$, the threshold $100 phi^{2k}$ is strictly positive, where $phi$ is the golden ratio.
background
The module models civilizational complexity as the Z-rung of the societal recognition substrate, with five tiers (band through empire) matching configDim D=5 and population thresholds scaling by powers of phi. The upstream definition supplies tierThreshold(k) := 100 * phi^(2*k), which encodes the RS prediction that adjacent tier thresholds stand in ratio phi^2. This setting draws on Turchin's cultural complexity scale and Bondarenko's classification to embed archaeological tiers inside the phi-ladder.
proof idea
The proof is a one-line wrapper that applies mul_pos to the positivity of 100 (via norm_num) and the positivity of phi raised to the power 2k (via pow_pos using phi_pos).
why it matters
This supplies the threshold_pos field required by the CivilizationCert structure, which certifies the five-tier model together with tierCount and the phi-squared ratio. It closes the positivity requirement for the archaeological embedding of Recognition Science predictions, including phi-ladder scaling of societal sizes from the T5 J-uniqueness and T6 phi fixed-point steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.