art_history_one_statement
plain-language theorem explainer
The Western canon comprises eleven named styles from 1400 to 1960 whose average inter-style interval equals 56 years and lies above the gap-45 threshold. Recognition theorists would cite the result as a quantitative consistency check that observed style transitions match the J-cost trajectory and consciousness-gap prediction. The proof is a term-mode conjunction that packages three prior results on list length, explicit gap arithmetic, and the numerical inequality.
Claim. Let $W$ be the ordered list of Western art styles with emergence years from 1400 to 1960. Then $|W|=11$, the average inter-style gap equals $(1960-1400)/(11-1)=56$, and the gap-45 threshold satisfies $45leq56$.
background
The declaration belongs to the ArtHistory module on visual-style succession from J-cost (Track I9 of Plan v5). westernCanon is the concrete list of eleven styles with approximate years: Renaissance (1400), Mannerism (1520), Baroque (1600), Rococo (1700), Neoclassical (1750) and six later entries up to Post-Modernist. averageGap is defined by the arithmetic expression (1960-1400) divided by (length minus one). gap45 is the base 45-year interval that the module treats as the predicted consciousness gap, with observed gaps required to lie inside the band [15,90] yr consistent with phi-rational variation.
proof idea
The proof is a one-line term-mode conjunction that directly supplies the three upstream results: the decidable length theorem for the canon list, the equality theorem obtained by unfolding the averageGap definition and substituting the length value, and the inequality theorem that rewrites the average to 56 then normalizes against the gap45 constant.
why it matters
This is the master statement for the art-history track, confirming that the eleven-style Western canon exhibits an average gap of 56 years inside the gap-45 band predicted by the J-cost model. It closes the empirical check for style succession and aligns with the phi-ladder and eight-tick octave cycle periods. The module document presents the result as a real derivation whose falsifier would be a documented century without style transition or more than five transitions inside fifty years.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.