tierCount
The declaration asserts that the finite type of civilizational complexity tiers contains exactly five elements. Archaeologists and complexity theorists applying Recognition Science to societal scales would cite this cardinality when certifying Z-rung mappings. The proof is a one-line decide tactic that evaluates the Fintype instance derived from the five-constructor inductive definition.
claimThe set of civilizational complexity tiers has cardinality five: $|$band, tribe, chiefdom, state, empire$| = 5$.
background
The module frames civilizational complexity C as the Z-rung of the societal recognition substrate, drawing on Turchin's 0-50 point scale across nine domains and Bondarenko's five-tier classification. The inductive type ComplexityTier enumerates these levels explicitly: band for Z-rung 0-2 (hunter-gatherer, <100 members), tribe for 3-5 (early agriculture, 100-2000), chiefdom for 6-8 (monumental architecture, 2000-20,000), state for 9-11 (writing, law, cities, 20,000-1M), and empire for 12+ (multi-ethnic, >1M). This yields configDim D = 5, with the module noting that adjacent tier thresholds should scale by phi squared approximately 2.618, consistent with the phi-ladder and eight-tick octave from the forcing chain.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to the equality Fintype.card ComplexityTier = 5. The tactic uses the derived Fintype instance on the inductive type with five constructors and computes the cardinality without invoking additional lemmas.
why it matters in Recognition Science
This cardinality supplies the five_tiers component of the downstream civilizationCert definition, which packages the tier structure for archaeological certification. It implements the module claim that five tiers equal configDim D = 5 and supports the Recognition Science prediction of phi-squared threshold ratios, linking to the T5 J-uniqueness and T6 phi fixed-point steps in the unified forcing chain. The result closes a small scaffolding step toward deriving the phi-based ratios in tierThreshold_ratio.
scope and limits
- Does not assign explicit Z-rung intervals to each tier.
- Does not derive the phi-squared ratio between adjacent thresholds.
- Does not connect to the mass formula or Berry creation threshold.
- Does not provide empirical validation against historical datasets.
Lean usage
theorem usesTierCount : Fintype.card ComplexityTier = 5 := tierCountformal statement (Lean)
33theorem tierCount : Fintype.card ComplexityTier = 5 := by decide
proof body
34