Reward-prediction models can fit the observed data while encoding different causal accounts of which action deserves credit. This report turns the proposed credit window into a formal relationship, calibrates it against published measurements, and checks the result with a Lean proof.
The analysis separates a supported hypothesis from competing rules that fail the same evidence and invariants.
The formal layer proves the relationship between the decay parameters and the point where the eligibility signal reaches 1/e of its peak. The empirical layer then checks whether the published dopamine measurements fall inside that interval.
Evidence stays scoped. The result supports this credit-window hypothesis for the cited paradigm. It does not turn one experiment into a universal claim about every reward-learning system.
A natural‑language claim, its formal statement, and a paradigm (paper, dataset, or instrumented simulator) it must hold against.
A verdict per verification layer, a sandwich bound on the key parameter, and a Lean proof that either closes the theorem or localises the counterexample.
theorem credit_window_is_one_over_e_decay (γ λ Δt : ℝ) (hgl_pos : 0 < γ * λ) (hgl_lt : γ * λ < 1) (hΔt : 0 < Δt) : Real.rpow (γ * λ) (creditWindowTau γ λ Δt / Δt) = Real.exp (−1)
In plain English: if the decay rate γλ lies strictly between 0 and 1, then exactly τc seconds after a reward, the eligibility signal has dropped to 1/e of its peak. No free parameters; the credit window is forced by γ, λ, and the simulator step Δt alone. The Tang 2024[1] data lives inside that bound, so the hypothesis survives this paper. Candidate rules that predict a wider or narrower window are rejected.
One concrete hypothesis, unpacked. The sliders are the paper's knobs, the formula is the relationship between them, the conditions below are the rules the hypothesis must obey, and the four candidates are the alternative theories Kairos compares against.
A real dopaminergic-learning paradigm is a multi-month, multi-mouse instrumented-wet-lab operation: Tang et al.\ 2024[1] trained 25 mice over three days; Greenstreet et al.[3] ran approximately 80. A single-shot frontier-model agent writes code but cannot close a Lean proof. A team of agents without a formal-verification layer still cannot calibrate against the paradigm’s own public data. A pure theorem prover takes a prose claim but cannot replay the paradigm. Kairos is the only apparatus that satisfies every capability the task requires and completes in minutes.
| Capability | Humans (wet‑lab) |
Claude Opus 4.6 | 3×Opus 4.6 (orch.) |
Aristotle (Harmonic) |
Kairos |
|---|---|---|---|---|---|
| Accepts natural-language hypothesis | ✓ | ✓ | ✓ | ✓ | ✓ |
Shared State type across paradigm encodings | ✗ | ✗ | ✗ | ✗ | ✓ |
| Simulates the Tang paradigm (Layer 3) | ✓ | ✗ | ✓ | ✗ | ✓ |
| Property tests at sampled parameters (Layer 2) | ✗ | ✗ | ✗ | ✗ | ✓ |
| Machine-checked Lean 4 proof (Layer 1) | ✗ | ✗ | ✓ | ✓ | ✓ |
| AST mutation catalog (Python + Lean) | ✗ | ✗ | ✗ | ✗ | ✓ |
| Calibrates against Tang and Sousa public data | ✓ | ✗ | ✗ | ✗ | ✓ |
| Spans four paradigm families in one framework | ✗ | ✗ | ✗ | ✗ | ✓ |
| Completes pre-publication | ✗ | ✓ | ✓ | ✓ | ✓ |
| Wall-clock | 3 months 10–80 mice | 4 min | 19 min | 30 min – 2 h | 16 min |
How to read. Each row is one capability the Tang 2024[1] credit-assignment paradigm actually demands. A ✓ means the alternative satisfies it; ✗ means it does not. Aristotle is Kairos’s independent cross-check arm on the hardest theorems. Kairos does not depend on it and completes every main-text claim without it.
Each row is one way Kairos can check a candidate rule. The five run in parallel; a rule has to pass every applicable row to survive.
For each candidate rule, Kairos ships a typed artifact per modality. Pick a tab to see the Lean theorem, property-test outputs, simulation trace, or mutation coverage for that rule.
-- off-state updates are identically zero theorem td0_cannot_produce_temporal_window (α γ : ℝ) (V : ValueFn) (s s' : State) (r : Reward) : ∀ x : State, x ≠ s → tdUpdate α γ V s r s' x = V x := by intro x hx exact td0_one_step_support α γ V s s' r x hx
Two bounds on the key parameter, plotted together. The left line is the lower bound derived from experimental data; the right line is the upper bound derived from the analytic formula. A rule is consistent with the data only if the real value lives inside that band. Kairos reports the gap between the two bounds.
The per-layer outcome, collapsed to one line. Refuted means at least one verification layer caught a contradiction. Supported means every applicable layer passed and the sandwich bound held, which is the strongest statement Kairos can make without claiming absolute certainty.