primeGapTypeCount
plain-language theorem explainer
The theorem counts the admissible prime gap configurations in the Recognition Science model at five. Researchers modeling gap distributions via J-cost would cite this to fix the configuration dimension. The proof applies a decision procedure to the explicitly enumerated finite type.
Claim. Let $T$ be the inductive type whose constructors are the gap classes twin, cousin, sexy, cousin-cousin, and chain. Then the cardinality of $T$ is 5.
background
The module develops prime gap distribution from J-cost arguments in Recognition Science. It posits that gaps concentrate near phi-ladder spacings, with admissible gaps having small J-cost for the ratio gap over ln(p). The five principal structures are twin, cousin, sexy, cousin-cousin, and chain, setting configDim D equal to 5 at the model level.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. With the inductive type deriving Fintype, decide evaluates the cardinality directly from the five constructors.
why it matters
This supplies the five_types component of primeGapCert, certifying the gap model. It realizes the module's claim that the five gap structures equal configDim D = 5. In the framework it aligns with the eight-tick octave and spatial dimension D = 3 by discretizing gap configurations. The model-level status leaves open the need for Zhang-Maynard axioms to prove the structures occur infinitely often.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.