A Lean 4 Framework for Bounded Prime Gaps via Finite-Window Providers

This repository contains Version 4.0 of a self-contained Lean 4 framework formalising the finite combinatorial core of bounded prime-gap arguments. The development isolates a single abstract analytic hypothesis, expressed as a finite-window average inequality for the prime indicator, and formally verifies the purely finite reasoning that converts such an inequality into the existence of a bounded-gap prime pair. Version 4.0 is a structural generalisation of Version 3.0. All public theorems from v3.0 remain available with identical statements, but the core pipeline has been generalised from the fixed bound 600 to an arbitrary integer bound B : ℤ, with the 600 case retained as a convenient default interface. All results in this repository are conditional. No analytic number theory is implemented or assumed beyond the explicit hypotheses supplied by the user. In particular, the framework does not attempt to prove the existence of finite-window average inequalities. Instead, it treats them as externally provided certificates and focuses exclusively on verifying their finite combinatorial consequences. Every theorem is fully checked by the Lean 4 kernel and relies only on the standard classical axioms: propext, Classical.choice, Quot.sound The analytic input is intentionally minimal. A two-hit window witness asserts that for some finite setH ⊆ [0,B] and some integer shift n ∈ ℤ, the empirical average of the prime indicator function(equal to 1 on primes and 0 otherwise) over the shifted window is at least 2 / |H|. From this single assumption, the framework carries out three finite steps: • an average lower bound yields a lower bound on the sum of a 0/1-valued indicator;• a sum of at least 2 forces the existence of at least two distinct hits;• two hits in a window contained in [0,B] yield a pair of integers whose distance is at most B, and hence a bounded-gap prime pair. All remaining reasoning is finite, explicit, and purely combinatorial. Version 4.0 does not introduce new mathematical results beyond those already implicit in v3.0. Its purpose is architectural and verificational: to present a clean, modular, and fully audited formalisation of a finite combinatorial implication that frequently appears as a subcomponent of bounded-gap arguments, while keeping all analytic assumptions explicit and external. Included in this artifact The repository contains: • a pinned Lean 4 / mathlib toolchain ensuring reproducible builds;• the complete Lean source code for the finite-window combinatorial pipeline, both generic and 600-specialised;• a fully audited axiom report covering all public theorems;• a companion PDF documenting the framework, its interfaces, final theorems, and limitations;• API documentation describing the stable public interface. Purpose and scope This artifact is intended as formal mathematical infrastructure. It demonstrates how finite combinatorial reasoning commonly used in bounded prime-gap arguments can be isolated, modularised, and mechanically verified in Lean. The framework is designed to serve as a clean target for future analytic or computational certificates, to support alternative finite-window witnesses, and to enable reuse of the verified combinatorial core in related finite problems, while making no claims beyond what is formally proved.