Every data vendor says their pipeline is sound. We wrote the invariants down as theorems and put them through Coq, Isabelle/HOL, Lean 4, Dafny, Z3, TLA+ and property-based fuzzing. The artifacts are on this page — source and compiled — so the claim does not rest on us saying it.
These numbers were produced by counting declarations in the files below on 2026-09-04, not quoted from a summary. The method is in the last column so you can repeat it.
| Prover | Obligations | Artifact | Counted as |
|---|---|---|---|
| Coq / Rocq 9.1.1 | 39 | KairosDAGV5.v · .vo (compiled) | Theorem|Lemma|Corollary|Proposition |
| Lean 4 (file header 4.32.2; box has 4.33.1) | 38 | KairosDAGV5.lean | theorem|lemma — 12 of the 38 conclude True; 26 are substantive |
| Isabelle/HOL 2025 | 32 | KairosDAGV5.thy · ROOT | theorem|lemma|corollary |
| Dafny 4.11.0 | 27 | KairosDAGV5.dfy | lemma|method|function|predicate |
| Z3 SMT 4.15.4 | 42 | z3_verify_dag.py | check_prop() calls, each unsat-of-negation |
| Runtime (DAG) | 38 | runtime_verify_dag.py (in the manifest, not published here) — executed 2026-06-06 against core.kairos_dag_v5; the engine was located 2026-09-06 in a separate tree (sha256 a0491da6…, dated 2026-06-06) and the harness re-run: 38/38 | check functions; re-run 2026-09-06 (38/38) |
| TLA+ | 10 | KairosDistributed.tla | 6 safety invariants + 4 liveness properties (TypeOK not counted). No TLC configuration was retained, so until 2026-09-06 these were stated, not model-checked. Model-checked 2026-09-06 (TLC 2.19 on a small labelled model, corpus file unmodified): 5 hold (NoDeadlock, GPULimit, DAGMonotonic, LedgerAppendOnly, SignalConservation) and 5 are refuted — QueueBounds (channel_ack is never bounded) and all four liveness properties (Spec asserts WF_vars(Next) only, so an error/recover loop is a fair behaviour in which nothing else runs). Every counterexample is a real action cycle, not a bound artefact. Model, configs, logs and report: tla_recheck_20260906/ |
| Hypothesis (PBT) | 11 | hypothesis_fuzz_dag.py | @given properties |
| Total | 237 | MANIFEST.sha256 | 136 theorem-proved in 4 provers (124 once the 12 Lean True declarations are set aside) |
The compiled Coq object KairosDAGV5.vo is 55,053 bytes and begins with the magic
bytes Coq!. That file cannot exist unless coqc accepted the source. The
Isabelle session runs under quick_and_dirty = false, which means no sorry
was permitted anywhere in it — check ROOT yourself.
Read before counting (audit of 2026-09-05). Of the 38 Lean declarations, 12 have the
statement True, and 6 of the file’s 7 axioms do too — they compile, they assume and
prove nothing, and they sit in the count above because the count is a grep. The substantive Lean figure is 26.
Seven of the 32 Isabelle lemmas close by a one-line simp. The runtime row was executed once, on
2026-06-06; on 2026-09-06 the engine it targets was found in a separate tree and the harness re-run at 38/38, so it
is re-runnable after all. The TLA+ row was never model-checked until 2026-09-06, when 5 of its 10 properties were
refuted (table above); the corpus still counts them because they are stated obligations, and stated obligations
that fail are reported, not dropped. The manifest lists 16 files; 9 are
served on this page and 7 are not (Coq build by-products .glob .vok .vos .aux .lia.cache and the two
Python harnesses runtime_verify_dag.py, system_verify_all.py), so
sha256sum -c on the manifest will report those 7 as missing here. The obligations are what they are;
this paragraph exists so nobody counts them as more.
curl -O https://kairossignal.com/proofs/MANIFEST.sha256
curl -O https://kairossignal.com/proofs/KairosDAGV5.v
curl -O https://kairossignal.com/proofs/KairosDAGV5.vo
sha256sum -c MANIFEST.sha256 # our hashes, your machine
coqc KairosDAGV5.v # if you have Coq 9, reproduce the .voNot a new result; an independent replication with a Lean build behind it. On 5 September 2026 we derived n₀(5) = 14, n₀(6) = 16, n₀(11) = 27 and the boundary values g(14,5) = 10, g(16,6) = 12, g(27,11) = 23 for Erdős–Trotter problem #776 by the cascade Kruskal–Katona profile criterion. The literature check that followed found that M. Thiim's proof claim #78 (17 July 2026) already proves n₀(r) = 2r+4 for 4 ≤ r ≤ 10 and 2r+5 for r ≥ 11 with a full Lean 4 formalization, by the same method. We claim no priority.
| Artifact | What it shows | Checked |
|---|---|---|
| profile_check.py · certificate.json · verify_certificate.py | 3 obstruction traces (D₂ = 92 > 91, 121 > 120, 352 > 351) and 61 explicit antichains covering every n up to He–Tang's cutoffs | 1,813,031 pairwise containment tests, 0 failures; criterion equals exhaustive enumeration for n ≤ 5 |
| thiim_axiom_audit.log | Thiim's package built from source here (Lean 4.30.0, 1,064 targets, exit 0) | audit allowlist reproduced: standard axioms + 3 native_decide certificates, no sorry |
| KairosCases.lean · compile log | n₀(5), n₀(6), n₀(11) in the published formulation as corollaries of erdos776_threshold; exact values via explicit witnesses and a proved soundness lemma | 2026-09-05, 3.4 s, exit 0, no sorry; #print axioms in the log |
| MANIFEST.sha256 · .ots · PROVENANCE.md | Hashes of the release and its OpenTimestamps proof (Bitcoin-anchored once the calendar attestation confirms), plus the full timeline and attribution | sha256sum -c · ots verify |
Repository: github.com/OV3RK177/erdos776-three-cases. Credit for the theorem: Thiim's package; for the bounds and r = 2, 3: He and Tang (arXiv:2602.09803).
Two facts, stated side by side rather than one hidden behind the other.
| Layer | Last verified | Reproducible on demand |
|---|---|---|
Lean 4 — 25 theorems over the five production invariants, plus 28 Z3 / property cases (the separate hyperliquid_paper/formal_verification suite) | 2026-09-05, exit 0 (Lean 4.33.1) | Yes — runs in CI on every change |
| Coq · Isabelle · Dafny corpus (98 obligations) | 2026-06-06, artifacts retained | Not on our box — coqc 8.15 is installed but the corpus was compiled under Rocq 9.1 and does not build on 8.15; Isabelle and Dafny are not installed here |
So the precise sentence is: the Lean and Z3 layers re-run green today; the Coq, Isabelle and Dafny corpus compiled in June and its artifacts are published above. We will not write "reproducible on demand" over the second row until the toolchains are back and it runs green. If you have Coq 9, Isabelle 2025 or Dafny 4.11 installed, you can reproduce it before we can — and we would rather you did.
They are about our machinery, not about markets. They do not predict anything, and we do not sell them as edge. What they buy is narrower and more useful: when we say a value was not constructed with look-ahead, that a gate failed closed, that a derivation graph is acyclic, or that a cost identity holds — those are kernel-checked properties, not assurances from a vendor.
The same discipline runs against the live product daily. Our claim checker grades every published number on this site against live truth and fails in both directions, because overstatement and understatement are both errors. When our dilution engine served a septillion-dollar FDV, the fix shipped with the correction attached to the value, naming the source we rejected.
How these numbers are produced. Every figure in the table above is counted directly from the published artifacts, not read from a summary banner — a verifier banner carrying hard-coded per-prover counts is why an earlier figure of 255 circulated, and the counted total is 237. The corpus itself is pinned to git: all sixteen files were confirmed on 2026-09-03 to be byte-identical to their git blobs, which is the check that settles whether an artifact on disk is the one that was committed.
Institutional tier → Verify our live data → Corpus provenance →
Obligation counts produced by direct declaration counts over the published artifacts
on 2026-09-04. Live layer re-run 2026-09-04T00:41:25Z, exit 0. Corpus provenance: propintel commits
f1d646f / 727ee61, 2026-06-06.