The modular Jacobsthal function on 1 mod 6: exact computation, unconditional super-linear growth, and Lean 4 certification

General Repository Abstract This repository provides the complete computational reproducibility and formal verification suite supporting the research article "The modular Jacobsthal function on 1 6: exact computation, unconditional super-linear growth, and Lean 4 certification". The package gathers executable interactive notebooks (Jupyter/Colab), standalone CUDA C++ and Python/Numba source code, raw experimental records, publication-grade vector plots, and the complete formalization project developed in Lean 4 (v4.35.0 / Mathlib4). This suite enables independent replication of three primary deliverables: GPU-Accelerated CRT Sieving: Exact evaluation of the modular Jacobsthal functions for all z ≤ 31 over fundamental periods up to M(31) ≈ 3.34 × 10¹⁰, alongside deterministic windowed lower bounds for z ∈ \37, 41, 43\. Pre-asymptotic Rigidity Analysis: Analytical solution of the trans-computational departure threshold (z^* ≥ 1014.5) separating the pre-asymptotic linear regime from asymptotic FKPT growth, supported by nonlinear model selection and 10⁴ bootstrap resamples. Machine-Checked Verification in Lean 4: Kernel-level verification of fifteen self-contained modules (57 certified theorems and 32 verified definitions at Level N1, with zero sorry gaps and zero global axioms), formalizing the canonical isomorphism, universal lower bound, and conditional modular parity barrier. 2. Mathematical Content of the Manuscript The accompanying paper (The_modular_Jacobsthal_function.pdf / LaTeX source) resolves the tension between apparent pre-asymptotic linearity and asymptotic super-linear growth in extremal runs of integers blocked by primes along fixed arithmetic progressions: Modular Jacobsthal Functions (jC₁(z), jC₅(z), jboth(z)): Defined for z ≥ 5 as the maximal run length of consecutive integers k such that each $6k+1$ (or $6k-1$) is divisible by some prime 3 < p ≤ z. Unconditional chiral symmetry jC₁(z) = jC₅(z) is proved via the isometric involution k ↦ -k. The Canonical Isomorphism: An affine change of variables k ↦ k + 6⁻¹ M(z) over the reduced primorial $M(z) = P(z)/6$ establishes an exact equivalence jC₁(z) = j(P(z)/6) with the classical Jacobsthal function $j(n)$, making classical sieve bounds directly applicable. Universal Lower Bound and Super-linear Growth: An interval pigeonhole argument modulo 6 yields the universal lower bound: jC₁(z) ≥ j(P(z))/6 Combined with the Ford–Konyagin–Pomerance–Tao (FKPT, 2018) theorem, this unconditionally refutes linear rigidity, establishing jC₁(z)/z → ∞ and z → ∞ jC₁(z)/j(P(z)) ≥ 1/6. The Departure Threshold (z^*): The empirical linear fit jC₁(z) ≈ 0.452\,z - 1.45 observed across z ≤ 43 is demonstrated to be a pre-asymptotic artefact. Because the FKPT modulation envelope satisfies the universal bound ψ(z) ≤ 0.19232, the curvature crossover threshold is bounded below by z^* ≥ 1014.5 under optimal sieve constants (and z^* ≥ 10⁶³⁰ under realistic constants), proving that linearity necessarily persists across all computationally accessible scales. Channel Decoupling and the Modular Parity Barrier: Isolating a single residue class modulo 6 (P₁ or P₅) reduces the sifting dimension to κ = 1/2. Under the Erdős–Rankin capacity hypothesis, this fractional dimension forces sublinear run lengths y(z) z / √log z = o(z), showing that super-linear runs require the coordinated action of primes from both coprime residue classes. Epistemic Stratification: The manuscript precisely delineates unconditional mathematical theorems, statements conditional on standard sieve hypotheses, and open conjectures. Keywords: Jacobsthal function, primorial sieve, modular arithmetic, Z/6Z, Ford–Konyagin–Pomerance–Tao, Lean 4 formalization, arithmetic combinatorics, GPU computing. 3. Structure of the Artifacts A. Executable Jupyter / Google Colab Notebooks L4_The_modular_Jacobsthal_function.ipynb: Automates environment provisioning: installs elan, synchronizes toolchains against Mathlib4 (v4.35.0), downloads precompiled caches, and builds the 15 formalization modules. Executes kernel-level checks on every file, verifying the absence of sorry placeholders and unproven axiom declarations. Audits all definitions and theorems, outputting the cryptographic SHA-256 manifest. EXP_The_modular_Jacobsthal_function.ipynb: Implements the hardware manifest and deterministic seeding (GLOBAL_SEED = 42). S2: Compiles and executes native CUDA C++ kernels and Numba sieves over full fundamental periods $M(z)$ for z ≤ 31, validating witness offsets against Lean 4 certificates. S2b: Executes 50-window searches (10⁸ integers each) to compute lower bounds for z ∈ \37, 41, 43\. S3: Fits five growth models via nonlinear least squares and calculates 95% bootstrap confidence intervals (B = 10⁴ resamples). S4: Solves the transcendental equation Φ(z^*) = 6a/c via Brent's method. S5 / S5b: Evaluates isolated-channel runs on P₁ and P₅, computing transversal gains. S6: Renders and exports publication-ready vector figures. B. Formal Verification Distribution Chiral_Jacobsthal_Lean4_Reproducibility_Suite.zip: Self-contained standalone package containing all 15 .lean source files under Chiral_Jacobsthal_Lean/, the project configuration (lakefile.toml), toolchain pins, and build manifests. Verified Checksum:SHA-256: 1f0c63e8e133c20c2ae57696fa61395cf914336cf0c66c6a13127fbdb338a239 C. Experimental Data bounds_z_37_41_43.json.gz: Gzip-compressed JSON file containing raw records for all 150 sampled windows across z ∈ \37, 41, 43\ (window start offset, local maxima for jC₁ and jboth, and run coordinates). D. Publication Figures (Vector PDF and 300 DPI PNG) departure_threshold_analysis.pdf / .png (Figure 1): Universal modulation bound ψ(z) ≤ 0.19232 and slope crossover curves between theoretical FKPT bounds and empirical linearity. empirical_models.pdf / .png (Figure 2): Growth model fits on exact data (z ≤ 31) and residual distributions across models. isolated_channel_collapse.pdf / .png (Figure 3): Empirical collapse under channel decoupling, illustrating the transversal gap between coupled and isolated sieving. 4. Lean 4 Formalization Audit Manifest The fifteen modules comprising the verification suite are certified at Level N1 (zero sorry gaps, zero unproven global axioms): Module Level Theorems Defs SHA-256 Digest (first 16 chars) Mathematical Content Certified AsymptoticRigidity.lean N1 2 0 ad0c1516076fcf30 Transitivity of Landau asymptotic dominance: O(z) ∘ o(jP) o(jP). CRTPeriodicity.lean N1 4 2 385659854cfd0212 Local and global periodicity modulo $M(z)$ via Chinese Remainder Theorem. CanonicalIsomorphism.lean N1 2 1 17ac4247f596b33a Local affine equivalence via Bézout identity; quotient $Q(z) = j(M)/j(6M)$. ChannelDecoupling.lean N1 2 1 bfb4f9febd6ad062 Asymptotic subjugation for channels constrained to fractional dimension. ChiralRigidity.lean N1 4 0 324d70ad9646b2fe Squeeze lemma: linear rigidity together with FKPT envelope decay forces Q(z) → 0. ChiralSymmetry.lean N1 2 2 7c88a4a8d5f3a5cc Isometric involution k ↦ -k exchanging channels C₁ and C₅. ComputationalWitnesses.lean N1 9 11 9bb5f00d87dca7af Decidable witness run verification via kernel reflection (by decide) for z ≤ 31. FKPTBound.lean N1 1 1 c71980772cc16b8c Envelope decay under explicit parametric FKPT super-linear growth hypothesis. GeometricBarrier.lean N1 15 2 91c411fa70aa36a0 Erdős–Rankin conditional chain: (ER) (PNT) (κ=1/2) y = o(z). IwaniecBound.lean N1 2 0 d329cdf9f07948af Transfer of the Kanold–Iwaniec quadratic upper bound under channel inclusion. JacobsthalHierarchy.lean N1 2 2 67d01a769490039e Logical inclusions (BC₁ BC₅) BC₁ and BC₅. MertensDivergence.lean N1 1 0 b8e52c82abb015ee Contradiction from bounding non-sublinear runs by O(log z) models. ModularChannels.lean N1 2 2 fe108f589c8c90fe Definitional framework and reflexivity of modular blocking predicates. ModulationBound.lean N1 2 6 dc1d10cacec57e19 Monotonic composition Φ(z) = (log z)ψ(z) under universal bound ψ ≤ 0.19232. UniversalLowerBound.lean N1 7 2 70e0c1db38f6e811 Pigeonhole principle in Peano arithmetic: L/6 ≤ countₘod6(s, L). Total N1 57 32 — Zero sorry gaps, zero unproven global axioms. 5. System Requirements and Reproduction Instructions Lean 4 Suite: Requires Lean 4 (v4.35.0) and Lake. Automated build: Bash unzip Chiral_Jacobsthal_Lean4_Reproducibility_Suite.zip cd Chiral_Jacobsthal_Lean lake update && lake exe cache get! && lake build Experimental Suite: Requires Python 3.10+, NumPy, SciPy, Pandas, Numba, Matplotlib, and CUDA Toolkit (tested on NVIDIA Tesla T4 with CUDA 12+). Both .ipynb notebooks run autonomously end-to-end within standard Google Colab GPU sessions. - Publication Status: Submitted to Journal of Number Theory (Elsevier) on October 27, 2026.