Inspect the artifacts behind our engineering claims: formal statements, model checks, runtime tests and the counterexamples they found. Each result applies to the code or model named beside it.
What this establishes. These records show which specified properties and tests were checked, under their stated assumptions. They do not certify the whole production pipeline, establish trading profitability, or guarantee that upstream network reports are correct. For the DePIN data you receive, start with live-data verification and each observation’s source and timestamp.
Page review: 20 September 2026. The published manifest was fetched over HTTPS and its artifact hashes checked again. The build and test records retain their original dates; this review is not a new compilation of the corpus.
The declaration counts come from the pinned source files. They combine different methods, repeated formulations, trivial statements and obligations that failed. They are not a count of independent proofs of production correctness. Runtime checks and property-based testing are tests; TLA+ results apply to the particular checked model.
| Method | Named declarations / checks | 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 — 20 of the 38 conclude True (13 literally, 7 under a binder); 18 have a non-trivial statement, and by content 2 say anything about this engine — see the audit below |
| 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: expected-SAT consistency checks and expected-UNSAT counterexample searches over separately encoded models |
| Runtime (DAG) | 38 | runtime_verify_dag.py (published in the manifest) — 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 |
Lean: the inventory discloses trivial statements and axioms. Other declarations include
arithmetic examples and generic identities. In particular, dag_acyclic establishes no
self-parent edge, which is weaker than graph acyclicity. Compilation does not prove every property
suggested by a theorem’s name.
Z3 and Dafny: these encode constraints and program models separately. The Z3 harness includes satisfiable consistency checks as well as counterexample searches. Neither harness imports and executes the deployed Python engine. The runtime and Hypothesis harnesses are the checks that exercise the named legacy engine implementation.
Failed checks remain part of the evidence. A refuted property, an underpowered experiment, and an invalid experiment have different meanings. Each limits the claims we can make; a later repair does not rewrite the historical result.
mkdir kairos-proof-review
cd kairos-proof-review
curl -fSLO https://kairossignal.com/proofs/MANIFEST.sha256
while read -r digest file; do
curl -fSLo "$file" "https://kairossignal.com/proofs/$file" || exit 1
done < MANIFEST.sha256
sha256sum -c MANIFEST.sha256Verify the downloaded hashes first, then compile in a separate directory. Compiled bytes may differ between prover versions. The manifest and retained build logs supply the provenance; a binary header alone is not a verification of the source.
Not 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) | Dated successful run retained; current CI coverage is not asserted here |
| Coq · Isabelle · Dafny corpus (98 obligations) | 2026-09-10, exit 0 — Rocq 9.2 · Isabelle2025 · Dafny 4.11.0 (full log) | Toolchains and dependencies required; see the retained run and caveats below |
| Corpus Z3 (42 checks) and Hypothesis property-based fuzzing (11 properties) | 2026-09-10 — Z3 42/42, Hypothesis 11/11 across 5,500 random inputs (log) | The fuzz harness needs the engine tree on PYTHONPATH, see below |
So the precise sentence, as of 2026-09-10: the corpus re-verifies on this
box. Rocq 9.2 exit 0 · Lean 4.33.1 exit 0 · Dafny 4.11.0 “27 verified, 0 errors” ·
the Isabelle session builds under quick_and_dirty = false, the setting that makes
sorry impossible rather than merely absent · Z3 42/42 · Hypothesis 11/11 across 5,500
random inputs. Until 2026-09-10 this row read “not on our box”; that was true when written and
is no longer. Two caveats belong here rather than in a footnote:
.vo is not byte-identical to the published one. Published:
55,053 bytes, 84ffa577…, built under Rocq 9.1.1. Rebuilt 2026-09-10 under Rocq 9.2:
55,259 bytes, 2912d760…. Same source, accepted by a newer prover — so if you run
coqc and then sha256sum -c, expect a mismatch on that one file and not a
forgery.ModuleNotFoundError: No module named 'core'. It imports the runtime engine, which lives in a
separate tree (sha256 a0491da6…, the same hash published in the runtime row above). With that
tree on PYTHONPATH it is 11/11. A missing import path, not a refuted property — stated here so
nobody reads the traceback as a failed proof.The original bounded model has passing and refuted properties, retained in the inventory and model-check report. Successor specifications repaired some model defects; they do not change the original result. Remaining counterexamples concern progress under faults and a requirement that a continuously fed pipeline become idle.
This is a proposed two-node architecture with acknowledgement queues and in-flight work. It is not a specification linked to the current deployment. Its counterexamples identify design requirements, not demonstrated outages in the live DePIN API.
The published diagnostic and its self-test probe the trading model architecture with random weights. In the recorded 10 September test, replacing a sample’s batch companions did not change its output; an injected BatchNorm layer made the control test fail. This supports the tested architecture and batches. It does not establish absence of every form of look-ahead, validate learned weights, or measure predictive performance.
Deployment scope: the legacy kairos_dag_v5.py runtime checks do not certify
the paper trader’s different DreadnoughtByteDAG implementation. Passing checks for one
implementation must not be transferred to another.
Use these artifacts to inspect particular engineering claims and their limits. They complement the source URLs, timestamps and replay evidence supplied with our DePIN observations. They do not establish end-to-end production correctness or the accuracy of every upstream report.
The source artifacts remain unchanged. Corpus provenance records their origin and corrections to earlier claims. We publish counterexamples alongside successful checks so buyers can judge the scope of the evidence.
Institutional tier → Verify our live data → Corpus provenance →
Page scope reviewed 2026-09-20. Build and model-check dates are stated with their evidence. No whole-system certification is claimed.