styleGap
plain-language theorem explainer
styleGap computes the difference in emergence years between two ArtStyles. Researchers modeling cultural phase transitions via J-cost trajectories cite it to quantify intervals in the Western canon. The definition is a direct subtraction on the natural-number emergence fields of the ArtStyle structure.
Claim. Let $a$ and $b$ be ArtStyles with emergence years $y_a, y_b$. The style gap is defined as $y_b - y_a$.
background
ArtStyle is a structure pairing a descriptive label with an approximate emergence year in natural numbers. The module derives visual style succession from J-cost trajectories, predicting inter-style gaps near 45 years (the gap-45 band) with variation bounded by half-phi. Upstream, the gap definition in Gap45.Derivation is the product of closure and Fibonacci factors, yielding exactly 45. This local setting tabulates eleven Western styles from Renaissance to Post-Modernist and checks their gaps against the predicted band.
proof idea
The definition is a direct field subtraction: emergence year of the later style minus that of the earlier style.
why it matters
This supplies the basic interval measure for the art-history track of the J-cost forcing chain. It enables the average gap computation of 56 years (within gap-45 ± half-phi) and supports the StyleSuccessionCert. The module falsifier is a period exceeding 100 years without transition or more than five transitions in 50 years.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.