styleSuccessionCert
plain-language theorem explainer
styleSuccessionCert assembles four sibling results into a single certificate asserting that the Western canon lists eleven styles whose average inter-style gap equals 56 years and lies inside the gap-45 band. Cross-domain modelers and art historians cite it when checking whether observed style cycles match the J-cost-derived gap-45 prediction. The definition is a direct record construction that supplies the four required fields from the corresponding lemmas plus a reflexivity step for the gap45 equality.
Claim. Let the western canon be the ordered sequence of eleven major styles from Renaissance through Post-Modernist. Then the average inter-style gap equals 56 years, satisfies $15$ yr $≤$ average gap $≤ 90$ yr, exceeds the gap-45 reference value, and the gap-45 reference itself equals 45 yr.
background
The module derives visual-style succession from J-cost dynamics (Track I9). It treats the ordered list of eleven Western styles as a concrete instance of the gap-45 prediction, where successive emergences are expected to fall inside the interval [15, 90] yr with average near 45 yr. gap45 itself is imported from CardinalitySpectrum as the product Dspatial² · Dconfig and fixed at 45 by the decide tactic in gap45_eq. StyleSuccessionCert is the structure that packages the four numerical claims (canon length, average gap, band membership, and comparison to gap45) into one certificate object.
proof idea
The definition is a one-line record constructor. It assigns canon_length to the theorem westernCanon_length, average_gap_eq to averageGap_eq, average_gap_in_band to averageGap_in_gap45_band, average_above_gap45 to averageGap_above_gap45, and gap45_eq to rfl. No further tactics are required once the four sibling lemmas have been established.
why it matters
This definition supplies the master certificate referenced by the module's one-statement summary of art-history succession. It closes the concrete verification step that links the J-cost trajectory to the observed 1400–1960 Western canon, thereby instantiating the gap-45 band prediction inside the Recognition framework. The falsifier stated in the module doc (a >100 yr gap with no style transition, or >5 transitions in 50 yr) remains the open empirical test for the claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.