averageGap
plain-language theorem explainer
AverageGap defines the mean interval between the eleven Western art styles as (1960-1400) divided by ten, equaling 56 years. Researchers tracing cultural patterns to the J-cost functional equation would reference this value when checking consistency with the gap-45 band. The definition is a direct arithmetic reduction using the length of the canonical style list.
Claim. The average inter-style gap for the Western canon is defined by $ (1960 - 1400) / (n - 1) $ where $n$ is the length of the list of eleven styles.
background
The module derives visual-style succession from the J-cost trajectory of period-style geometric coherence. Eleven named Western styles are ordered by emergence year, with inter-style gaps required to lie in [15, 90] yr. The upstream westernCanon definition supplies the list of styles and years. This setting follows from the Recognition Science forcing chain, specifically the eight-tick octave periodicity that predicts a 45-year consciousness gap.
proof idea
The definition directly computes the quotient (1960 - 1400) / (westernCanon.length - 1). It depends on the westernCanon list definition to obtain the length value of 11.
why it matters
This supplies the concrete 56-year value that enters the art_history_one_statement theorem and the StyleSuccessionCert structure. It realizes the gap-45 prediction for art history as an instance of the J-cost model, consistent with the Recognition Composition Law. The result closes one step in the Track I9 derivation while leaving open whether the same periodicity governs non-Western traditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.