A kernel-verified model of safe cell rejuvenation
Partial reprogramming promises to roll back cellular age — but push the Yamanaka factors too far and the cell loses its identity for good. Cairn is a dynamical-systems model of OSK/OSKM reprogramming that turns that trade-off into theorems: a certified intervention window, a sharp point of no return, and provable recovery basins.
Every consequence is replayed through the Lean kernel — the proof, not the simulation, is the witness.
The control problem
Rejuvenate without erasing identity
Transient expression of Oct4, Sox2, Klf4 (± c-Myc) lowers markers of cellular age. But the same factors, applied long enough, drive a somatic cell across a chromatin-gated threshold into a self-sustaining pluripotent state — and that crossing is effectively irreversible. The therapeutic question is a control question: how far can you push, and for how long, before recovery is lost?
Cairn answers it inside a discrete dynamical system over five normalized coordinates — somatic activity, pluripotency, the slow somatic and pluripotency gates, and age burden — with saturating, fixed-point arithmetic so that every trajectory is exactly computable. The reprogramming protocol is the control signal; the endpoints after withdrawal are the verdict.
The certified window
Twenty-two to twenty-six ticks — proved, not simulated
Exact post-withdrawal endpoints from the model. Each bar is the endpoint age burden after n OSK ticks: it falls a constant 22 per tick, crossing the Young threshold (≤ 500) precisely at n = 22. Recoverability is lost between 26 and 27 — yet age keeps dropping past the cliff. You keep getting younger; you just can’t come back.
OSK exposure ticks (n), then standard withdrawal
Values are exact kernel-model endpoints, not a fit. At n = 21 the endpoint age is 518 (not young); at 22 it is 496 (young). The cell is recoverable through 26 and not at 27 — so pulse21_too_short, recoverable_through_26 and pulse27_not_recoverable place the loss-of-recoverability time in (26, 27].
The bistable switch behind the cliff
endpoint coordinates · scale 1000Age falls smoothly, but identity does not: somatic activity holds at 1000 through n = 26 then collapses to 0, and pluripotency is its mirror image. The switch is all-or-nothing at 26 → 27.
The last warning. The recoverability reserve — the slow somatic gate — has already eroded from 1000 to 706 at n = 26, the final recoverable dose, before dropping to 0 at the switch (window_edge_reserve_depleted).
The causal story
Five mechanistic hypotheses, made precise
The update rules encode a specific theory of why timing matters. Each hypothesis is a clause in the transition function — and each has a necessity theorem behind it.
Ablate any clause and a registered outcome breaks — the model competition arbitrates which hypotheses survive.
See the searchKernel-checked guarantees
The proof, not the simulation, is the witness
Each statement below is discharged by the Lean kernel’s decide — not native_decide — so it trusts the kernel alone, with a trusted axiom base of propext / Quot.sound. No floating point, no sampling, no compiler in the loop.
A nonempty safe intervention window
There exists an exposure length n with 22 ≤ n < 27 that both rejuvenates (lowers age burden past threshold) and remains recoverable after withdrawal. Below 22 the youthful threshold is not reached; at 24 it succeeds.
finite_safe_window_exists · pulse24_succeeds
A sharp point of no return
The reference cell is recoverable after every exposure ≤ 26 ticks, and not at 27 — pinning loss-of-recoverability to the half-open interval (26, 27]. A continuum version certifies a whole box of nearby cells.
recoverable_through_26 · pulse27_not_recoverable
Forward-invariant recovery basins
Interval (box) transitions over-approximate the dynamics; a basin that maps into itself is invariant for every state it contains. Both the somatic recovery basin and the pluripotent commitment basin are certified over the whole continuum.
somatic_basin_stays_somatic · pluripotent_basin_stays_pluripotent
A stochastic return bound, grounded in the basin
A supermartingale (barrier) certificate bounds escape under noisy withdrawal by P(escape) ≤ 2^(−m). The margin m is read off the verified somatic basin's depth (300 somatic units ÷ 30 per level = 10), so a fully recovered cell escapes with probability ≤ 2^(−10) ≈ 0.001 for every horizon — no measure theory.
geometric_committor_bound · fully_recovered_escape_bound
An exact discretization-error bound
The discrete model is the Euler discretization (h=1) of a chromatin-gated hybrid automaton. Linear coordinates (age, gates) are Euler-exact; the one quadratic flow (pluripotency) is overshot by exactly k/2 after k ticks.
euler_p_error · euler_p_enclosure
Mechanism necessity, rate-robust
Inhibiting TET keeps the cell somatic but never young; ablating the pioneer gate keeps it from stable commitment. Both are proved for every structural ablation and every rate choice — not just the default constants.
tet_inhibited_never_young_MR · pioneer_ablated_never_pluripotent_MR
Learned-update enclosure (IBP)
A learned ReLU network with fixed integer weights is enclosed by an interval transition: interval bound propagation proves every point of an input box maps into the output interval — a verified over-approximation of a learned, nonlinear update for the whole continuum, not a sampled one.
lpBox_sound · learned_enclosure_width
Provenance-bound falsification
Every registered observation certificate is bound to real, recomputable SHA-256 digests of the model, classifier, protocol, and robustness analysis — no placeholder remains, and the binding is tamper-evident in CI. A future contradicting reading is a checkable falsification trigger.
registry_fully_bound · model_consistent_with_literature
Timing changes everything
Same dose, opposite fate
The sharpest prediction: an equal total OSK-on dose gives a different outcome depending on whether it is delivered in pulses with rests or in one continuous block. Rests let the slow somatic gate recover between doses; continuous exposure lets pluripotency latch.
This is the model’s rejuvenation-vs-commitment knife-edge — rest_changes_outcome, kernel-checked.
Pulsed exposure rejuvenates and returns to source identity after withdrawal.
The same total OSK-on dose, without rests, crosses into the self-sustaining basin.
Generate and verify
Search is untrusted; the kernel is the checker
A genetic-algorithm proposer explores in fast Python — rate constants, structural ablations, interval boxes, supermartingale barriers. Whatever it finds, the champion is replayed through the Lean kernel. A wrong search can only fail to find a good candidate; it can never certify a false claim.
The same engine drives several certificate families — model rates/structure, forward-invariant interval basins, and stochastic-escape barriers — all propose-in-Python, verify-in-kernel. It also arbitrates the mechanism set: under held-out perturbation testing the full gated model is the unique surviving structure.
Model competition
Evolve structure × rates to fit registered outcomes under a parsimony penalty; the kernel certifies the structural champion.
Held-out arbitration
Withhold each perturbation from the fit: four ablations are refuted held-out-robustly, fast-only is separated by timing — the full model uniquely survives.
Interval-basin search
Find the largest forward-invariant box in the somatic / pluripotent region; (stepBox B).Subset B by decide.
Barrier search
Find the steepest valid supermartingale; the kernel replays P(escape) ≤ W[m]/W[0] for every horizon.
Empirical grounding
Held to a control-first empirical standard
The dynamical-systems picture the model assumes is audited on public data with modality-matched nulls — a companion study that reports the non-detections as carefully as the detections, and constrains how strongly the geometric-attractor view can be claimed.
Companion manuscript: “A control-calibrated audit of attractor-like signatures in transcriptomic and chromatin-conformation data.” One pure-Python pipeline (attractor-audit, tier0/) with an 11-test control-validation suite over Paul 2015, Bintu 2018, Cook & Vanderhyden 2020, LARRY, Huang 2005, and Gabriele 2022.
Scope & honesty
What the model is — and is not
The value of a verified model is the precision of its claims. Cairn proves theorems about an idealized control problem; it does not assert calibrated biological rates.