CivilizationalStage
plain-language theorem explainer
The inductive type enumerates five canonical stages of civilizational development drawn from historical rise-and-fall patterns. Sociologists or historians working inside Recognition Science cite the enumeration when modeling cohesion as a recognition coherence field whose cycles sit on phi-ladder timescales. The declaration is introduced as a direct inductive definition that automatically derives decidable equality, representation, boolean equality, and finite-type structure.
Claim. Let $S$ be the finite set of civilizational stages given by $S = $ {emergence, growth, consolidation, decline, transformation}, equipped with decidable equality and finite cardinality.
background
In the Recognition Science treatment of sociology, civilizational cohesion is identified with a recognition coherence field whose dynamics generate rise-and-fall cycles on phi-ladder timescales. The module fixes five canonical stages that realize configuration dimension D = 5. These stages are emergence, growth, consolidation, decline, and transformation. The local setting assumes zero axioms and zero sorry statements, with the explicit RS prediction that adjacent cycle durations stand in the ratio phi.
proof idea
The declaration is a direct inductive definition that lists the five constructors and immediately derives the instances DecidableEq, Repr, BEq, and Fintype. No lemmas are invoked; the structure is primitive.
why it matters
This definition supplies the finite set of stages required by the downstream theorem civilizationalStageCount, which establishes cardinality exactly five, and by the structure CivilizationCyclesCert, which encodes the universal phi-ratio property for cycle durations. It realizes the RS prediction that civilizational cycles operate on phi-ladder timescales inside a five-dimensional configuration space. The construction closes the sociological tier by providing the discrete stages that feed into quantitative cycle certification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.