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
Exposure length, then standard withdrawal. Too short and rejuvenation never reaches threshold; too long and the cell commits and cannot return. The kernel certifies every cell in the band.
Endpoint of exposure length n (OSK ticks) followed by withdrawal. pulse21_too_short, recoverable_through_26, and pulse27_not_recoverable together place the loss-of-recoverability time in (26, 27].
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
A supermartingale (barrier) certificate yields an all-horizons escape bound P(escape) ≤ 2^(−m) from recoverability margin m — so the somatic region is held with probability ≥ 1 − 2^(−m). Finite integer arithmetic, no measure theory.
geometric_committor_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
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 three certificate families: model rates/structure, forward-invariant interval basins, and stochastic-escape barriers — all propose-in-Python, verify-in-kernel.
Model competition
Evolve structure × rates to fit registered outcomes under a parsimony penalty; the kernel certifies the structural champion.
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.