Kernel-Gated Evolution: a Biomimetic Search with Apoptotic Checkpoints and Exact Dosage, Arbitrated by a Proof Kernel (Foundation Paper and Rust Reference Implementation)

Kernel-Gated Evolution (KGE) is a biomimetic search for programs whose acceptance is decided by a proof kernel rather than by the search itself. Three mechanisms borrowed from living systems are combined, each chosen because it earned its place under measurement: Darwinian variation and selection drives exploration; apoptotic checkpoints — one-sided exact screens that can remove a candidate but never confer survival — cull what cannot be right before any proof is attempted; and exact dosage analysis reports, for every locus of a genome, precisely how much its value reaches the phenotype, in one forward and one backward pass. The final judgement is a Lean 4 kernel: a survivor is rendered to Lean and must prove its obligation with an axiom dependency free of sorryAx. Fitness guides; the kernel decides. A wrong fitness can waste search effort but cannot manufacture an acceptance. Everything is exact. Every quantity is an exact rational, so no step of the search is an approximation and every invariant is checkable. The dosage coefficients are verified against their two-evaluation definition on 500+ locus-point pairs (2,496 in the Python prototype); the required-value identity v* = v + (want − out)/B on 2,000+ pairs (24,303 in Python); and the checkpoint's one-sidedness by constructing a candidate that agrees at every sample point yet differs as a function — it survives the checkpoint and is rejected by the kernel. The gate costs one invocation per batch at any failure rate. A Lean compile reports a per-declaration verdict even when it exits nonzero, so a batch of eight candidates is verified in one invocation whether 0, 1, 2, 4 or 8 of them are false, with every culprit named and no false candidate accepted, against eight individual proofs (50.88 s). Acceptance never rests on the exit code; it rests on a forgery scan, a per-declaration axioms line and a whitelist free of sorryAx. Rust reference implementation with replayable seeds and six exact-arithmetic tests; a kge ladder binary that runs a calibration ladder of exact targets up to the Verlet position update, reports solve rates, distinct solutions and the inert (dead-code) fraction of each best individual, exercises the checkpoint as a control with a known answer, and writes Lean candidates for the gate. Results, a population-versus-hill-climbing comparison, and a landscape characterisation are reported in the paper. Where it applies: verified numerical kernels (integrator steps, stencils, update rules that must be proved equal to a specification); any synthesis with a formal acceptance criterion; exact dead-code analysis of evolved programs; and batching expensive verification in general. Limitations are stated plainly: one closed grammar in the reference implementation; solve rates fall steeply above targets of about nine nodes and the full Verlet target is unsolved at the tested budget — a cliff not explained by basin geometry and not relieved by recombination (eight operators tested under pre-registered bars; companion measurements in Paper I, DOI 10.5281/zenodo.23622868), which is why KGE is mutation-driven; the checkpoint is one-sided by design; dosage is instrumentation rather than steering; and about 97% of a Lean invocation is fixed overhead that batching amortises but a persistent kernel would remove. Future research: exploiting the affine structure to solve constant loci by exact linear algebra; representations with higher solution density at scale; a properly powered study of contribution-preserving transfer (positive signal p = 0.031 against its matched control, not surviving correction); a persistent kernel; adaptive checkpoints; and application to the project's Python-genome kernel path. Every number is produced by a committed script or test and checked against its artefact before deposit. Not peer reviewed.