averageGap_in_gap45_band
plain-language theorem explainer
The theorem establishes that the average gap between successive Western art styles equals 56 years and satisfies 15 ≤ average gap ≤ 90. Art historians or Recognition Science practitioners would cite it when verifying that style succession periods align with the gap-45 prediction. The proof rewrites the average gap definition to its explicit value and applies numerical normalization to confirm the bounds.
Claim. Let $g$ be the average gap between successive styles in the Western canon, given by $g = (1960 - 1400)/10$. Then $15 ≤ g ≤ 90$.
background
The module treats visual-style succession as following J-cost trajectories of geometric coherence. It defines the average gap as (1960 - 1400) divided by one less than the number of styles in the canon. The gap-45 reference arises in Gap45.Derivation as the product of closure and Fibonacci factors, with the main theorem asserting equality to 45. Related gap functions from mass anchors equal ln(1 + Z/φ) / ln(φ). The setting is Track I9, which alternates low-J high-coherence styles with high-σ states and predicts ~45 yr transitions modulo φ-rational variation.
proof idea
The proof is a term-mode one-liner. It rewrites the goal using the lemma that equates the average gap to 56. It then refines the conjunction by applying norm_num to each inequality, confirming 15 ≤ 56 and 56 ≤ 90 by direct arithmetic.
why it matters
This supplies the band membership required by the styleSuccessionCert definition, which certifies that the Western canon follows the J-cost cycle. It anchors the art-history track to the gap-45 derivation and the phi-ladder structure. The result touches the open question of whether the same periodicity governs non-Western style successions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.