ArtStyle
plain-language theorem explainer
ArtStyle is a record pairing a string label with a natural-number emergence year for historical styles. Recognition Science researchers modeling cultural sequences via J-cost would cite it to build the Western canon list and compute inter-style gaps. The declaration is a direct structure with derived decidable equality and representation.
Claim. An art style consists of a string label together with a natural number denoting its approximate emergence year.
background
The module Visual-Style Succession from J-Cost treats art-history transitions as realizations of the gap-45 band that follows from the Recognition Composition Law and the eight-tick octave. ArtStyle supplies the minimal carrier type whose fields are a label and an emergence year in the natural numbers. Upstream canonical objects supply the arithmetic (Peano surface), the 45-year beat cycles, and the prime-based non-resonant schedule that prevents parasitic alignments in the style sequence.
proof idea
The declaration is a direct structure definition with two fields and automatic derivation of DecidableEq and Repr. No lemmas or tactics are invoked; the type is introduced to serve as the element type of the westernCanon list and the domain of styleGap.
why it matters
ArtStyle anchors Track I9 by providing the data type for the eleven-style Western succession whose average gap is shown to lie inside the gap-45 band. It feeds styleGap and westernCanon, which in turn realize the J-cost trajectory prediction from the UnifiedForcingChain. The module falsifier is a documented century without style change or five transitions inside fifty years.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.