IndisputableMonolith.Mathematics.PrimeGapFromJCost
The module defines types and certificates for prime gaps derived from the J-cost function. It identifies the canonical case of gap 2 with J(1) = 0, where the ratio to ln(p) is approximately 1. The module consists solely of definitions with no theorems or proofs.
claimThe canonical recognition gap satisfies gap = 2 with J(1) = 0, where the ratio to ln(p) approximates 1.
background
The module imports IndisputableMonolith.Cost to access J-cost definitions and Mathlib. It introduces PrimeGapType for classifying gaps, primeGapTypeCount for their enumeration, twin_prime_canonical for the twin-prime instance, PrimeGapCert for gap certificates, and primeGapCert for certificate construction. The setting derives prime gaps from the J function in Recognition Science.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the basic objects for prime gap analysis via J-cost, supporting extension of the Recognition framework to number theory. It directly encodes the canonical recognition gap J(1) = 0 from the module documentation. No downstream theorems are listed in the used_by relations.
scope and limits
- Does not contain any proved theorems or lemmas.
- Does not depend on modules beyond Cost and Mathlib.
- Does not address gaps other than the canonical case of size 2.
- Does not connect explicitly to the T0-T8 forcing chain.