KernelCert

KernelCert is a small, demonstrative Coq formalization of a Neural Tangent Kernel (NTK) and related concepts. This repository is part of a continuing series exploring formal proofs in machine learning and quantum computing. Each section is self-contained and focuses on a specific topic.

Neural Tangent Kernel (NTK)

This section isolates the core empirical NTK idea:

an NTK can be written as a Jacobian-feature inner product.

What is formalized here?

This Coq project proves a tiny but useful slice of NTK theory:

1. A finite-dimensional feature-map kernel [ K_\phi(x, y) = \langle \phi(x), \phi(y) \rangle ] is symmetric.
2. Its finite Gram quadratic form is nonnegative, i.e. it is positive semidefinite in the standard kernel sense.
3. For a scalar affine network [ f_{(w,b)}(x) = wx + b, ] the parameter-Jacobian feature is [ \phi(x) = (x, 1), ] so the induced NTK is [ K(x,y) = xy + 1. ]
4. A width-indexed NTK family converges pointwise to a limiting kernel under eventual feature stability (formalized in pointwise_limit_of_width_kernels).
5. If the Jacobian feature is parameter-independent, the NTK is constant across training time indices.
6. A polynomial Jacobian-map case study is embedded as an NTK feature source: the map is defined in Coq, the listed four preimages are proved to share the image (1,0,0), and the induced projected NTK inherits symmetry/PSD/convergence/constancy results from the core theory.

This is intentionally small and illustrative. It gives a concrete formal proof of the Jacobian-contraction picture, extends it with an explicit infinite-width convergence layer, and captures a training-time constancy theorem for parameter-independent Jacobians.

Theory and practice

Theory

The NTK of a model is the inner product of output derivatives with respect to parameters. For a scalar-output network f(θ, x), the empirical NTK is

[ K(x,y) = \left\langle \nabla_\theta f(\theta, x), \nabla_\theta f(\theta, y) \right\rangle. ]

In the infinite-width regime this kernel can become nearly constant during training, which is one of the key reasons NTKs are useful in theory: gradient descent can then be approximated by kernel regression dynamics. This repository includes a formal pointwise convergence theorem for width-indexed NTKs under eventual feature stability assumptions.

Practice

In practice, empirical NTKs are often computed by contracting Jacobians. This repository formalizes that core algebraic idea in the smallest setting where the proof is easy to read:

• a 2-dimensional parameter space,
• a scalar affine model,
• an exact closed-form kernel,
• and a proof that every finite Gram quadratic form is nonnegative.

File layout

• theories/NTK/Core.v: general finite-feature kernel machinery over 2D real features, including:
  • symmetry of kernel_of,
  • an explicit Jacobian-feature contraction theorem,
  • a Gram/quadratic-form identity,
  • nonnegativity of the induced quadratic form.
• theories/NTK/Asymptotic.v: asymptotic NTK statements, including:
  • an infinite-width convergence theorem from eventual feature stability,
  • a training-time NTK constancy theorem from parameter-independent Jacobians.
• theories/NTK/Affine.v: the affine network instance with feature (x, 1) and closed-form NTK xy + 1, plus concrete instantiations of the convergence and constancy theorems.
• theories/NTK/JacobianMap.v: a polynomial Jacobian-map case study that:
  • defines t = 1 + xy, q = t^2 z + y^2 (1 + 3t), and the 3D polynomial map,
  • proves the four stated points map to (1,0,0),
  • projects map components into a 2D NTK feature and reuses core symmetry/PSD/asymptotic theorems.
• theories/NTK/Examples.v: tiny sanity-check examples, including a direct demonstration of the Jacobian-feature contraction identity.

Build

If Coq is installed, build the project from this directory with:

make ntk

To build both NTK and Quantum proof targets together:

make all

To clean generated Coq artifacts:

make clean

Quantum Neural Tangent Kernel (QNTK)

This section introduces a formalization of quantum neural tangent kernel concepts, focusing on the physical principles of superposition and entanglement. The goal is to provide a rigorous foundation for quantum-kernel reasoning in the context of machine learning.

What is formalized here?

1. Fault Tolerance: A compact formal statement showing that a QNTK estimate remains bounded under a small circuit error rate.
2. Scalability to Large Quantum Systems: A simple linear-growth argument showing that a QNTK estimate scales predictably with increased system size.

File layout

• theories/Quantum/KernelProof.v: a compact proof layer for fault tolerance and scalability properties of a quantum neural tangent kernel estimate, including a basic formalization of those two design goals.

Build

If Coq is installed, build the project from this directory with:

make quantum

To clean generated Coq artifacts:

make clean

This project remains a pedagogical artifact focused on foundational principles, compiler-style formalization, and basic quantum-kernel reasoning rather than a complete production-grade quantum machine learning stack.

Riemann Hypothesis Roadmap

This section documents a formal, machine-checkable roadmap around the Riemann Hypothesis (RH). It does not claim an unconditional proof of RH. Instead, it encodes a conditional closure structure:

1. Gap A (rigid test-function framework) is represented as a closed component in the roadmap logic.
2. Gap B (uniform stability/remainder bounds) is represented as an explicit assumption.
3. Gap C (Hilbert-Polya style spectral/operator closure) is represented as an explicit assumption.
4. From A+B+C, the final RH target is derived conditionally.

What is formalized here?

• A Coq module that defines abstract closure assumptions for the three-gap pipeline.

• A machine-checked theorem that packages the dependency graph:

  Gap A + Gap B + Gap C -> RH

• A bundled theorem form suitable for CI checks and incremental formalization.

File layout

• theories/Riemann/Roadmap.v: machine-checkable logical skeleton for conditional RH closure, including:
  • abstract assumptions for Gap A/B/C,
  • intermediate propositions (NoOffLineZeros, SpectralReality),
  • final conditional theorem conditional_rh_closure.
• riemann_hypothesis.tex: mathematical draft detailing the theorem/lemma roadmap and open obligations.

Build

If Coq is installed, build the roadmap target with:

make riemann

To build all Coq targets currently wired in the Makefile:

make all

To compile the RH draft document (requires pdflatex):

make rh-pdf

License

This subproject is licensed under the MIT License. See LICENSE.