PrimeGapType
plain-language theorem explainer
This inductive definition enumerates the five admissible prime gap structures in the Recognition Science model of prime distributions. Number theorists analyzing gap ratios via J-cost minimization would cite the classification when bounding consecutive prime differences. It is realized as a direct inductive type with five constructors and automatic derivation of Fintype and decidability instances.
Claim. Let $G$ be the set of admissible prime gap types. Then $G$ consists of the five structures twin (gap 2), cousin (gap 4), sexy (gap 6), cousin-cousin (gap 8), and chain (longer sequences), each satisfying a small J-cost condition on the gap-to-$-ln(p)$ ratio.
background
Recognition Science models prime gaps as concentrating near phi-ladder spacings, where the ratio of consecutive gaps is bounded by J-cost arguments. J-cost is given by the functional $J(x) = (x + x^{-1})/2 - 1$, which quantifies deviation from self-similarity under the Recognition Composition Law. The module treats the five principal gap structures (twin, cousin, sexy, cousin-cousin, chain) as realizing configDim = 5 at the model level, not as a theorem; full verification requires external axioms such as Zhang-Maynard or Goldbach-type statements.
proof idea
The declaration is a direct inductive definition that introduces the five constructors without proof obligations or lemmas. Decidability, equality, and finiteness instances are derived automatically by the Lean compiler.
why it matters
This supplies the gap-type classification that feeds directly into the structure PrimeGapCert (asserting Fintype.card = 5 and canonical J-cost zero) and the theorem primeGapTypeCount. It realizes the model-level claim that admissible gaps correspond to configDim = 5 in the Recognition Science framework. The module notes that full verification would require Zhang-Maynard or Goldbach-type axioms, leaving the structural claim open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.