westernCanon
plain-language theorem explainer
westernCanon enumerates the ordered list of eleven Western art styles with approximate emergence years from Renaissance in 1400 to Post-Modernist in 1960. Recognition Science researchers applying the J-cost model to cultural history would cite this list to anchor gap calculations. The definition is a direct enumeration matching the canonical sequence in the module documentation.
Claim. The Western canonical style succession is the list $[⟨Renaissance, 1400⟩, ⟨Mannerism, 1520⟩, ⟨Baroque, 1600⟩, ⟨Rococo, 1700⟩, ⟨Neoclassical, 1750⟩, ⟨Romantic, 1800⟩, ⟨Realist, 1840⟩, ⟨Impressionist, 1870⟩, ⟨Post-Impressionist, 1885⟩, ⟨Modernist, 1900⟩, ⟨Post-Modernist, 1960⟩]$, where each entry pairs a style label with its approximate emergence year.
background
ArtStyle is the structure consisting of a style label (String) and emergence year (natural number). The module derives visual-style succession from J-cost minimization, where J(x) = (x + x^{-1})/2 - 1 quantifies geometric coherence cost of period styles. The local setting tabulates eleven named Western styles ordered by emergence year, with successive gaps required to lie in [15, 90] years around the gap-45 reference. Upstream results include the ArtStyle definition together with structures from PhiForcingDerived and SpectralEmergence that calibrate the underlying J-cost and eight-tick dynamics.
proof idea
Direct definition by explicit list enumeration of the eleven styles and their emergence years. No lemmas or tactics are invoked; the body is the literal sequence of ArtStyle constructors.
why it matters
This definition supplies the concrete data list for the art-history application of the J-cost model. It is used by art_history_one_statement to assert eleven styles with average gap 56 years inside the gap-45 band, and by averageGap and StyleSuccessionCert to certify compatibility with the predicted interval. The construction realizes the module claim that style succession follows the J-cost trajectory, consistent with the phi-ladder and consciousness gap of approximately 45 years.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.