CivilizationCert
plain-language theorem explainer
CivilizationCert packages the claim of exactly five complexity tiers whose thresholds are positive and scale by phi squared. RS modelers of societal evolution cite it when encoding the Z-rung substrate for archaeology. The declaration is a structure that directly bundles the cardinality of ComplexityTier, the positivity of tierThreshold, and the consecutive ratio property.
Claim. A structure whose fields assert: the set of complexity tiers has cardinality 5; the threshold function $\tau(k) > 0$ for every natural number $k$; and $\tau(k+1)/\tau(k) = \phi^2$ for every $k$, where $\tau(k) = 100 \phi^{2k}$.
background
The module identifies civilizational complexity with the Z-rung of the societal recognition substrate and adopts Turchin's scale via Bondarenko's five-tier classification. ComplexityTier is the inductive type with constructors band, tribe, chiefdom, state, empire; its Fintype.card equals 5 by construction. tierThreshold is the upstream definition tierThreshold(k) := 100 * phi^(2*k) that supplies the population cutoffs separating the tiers.
The local setting states that five tiers correspond to configDim D = 5 and that adjacent thresholds must ratio by phi^2, consistent with the phi-ladder scaling already present in the Recognition Science constants module.
proof idea
Structure definition that assembles the three properties directly from the ComplexityTier inductive type and the tierThreshold definition; no tactics or lemmas are applied.
why it matters
civilizationCert constructs an explicit instance of this structure, supplying the certificate that the five-tier model satisfies the RS phi^2 ratio prediction. The module doc links the construction to the forcing chain landmarks (T6 phi fixed point, T7 eight-tick octave) and notes the D = 5 assignment for tiers. It closes the scaffolding step that lets downstream archaeology results treat the tier thresholds as phi-ladder objects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.