Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated

Verification records for L17

../

clean_gate/: The non-author clean gate of 2026-10-08 for L17: the committed Lean gate in clean mode over a fresh archive of the whole lean/ tree as it stood on 2026-10-08T13:58:11Z, exit 0, AUDIT PASS over 1 claim with 0 compiler axioms and the committed self-test stamp matched; the receipt, the captured log and the wrapper.

statement_fidelity/: The fidelity review, distinct grade, non-author clean gate, native binding and acceptance warrant for the first acceptance of L17, for the sources as they stood on 2026-09-25T03:40:15Z; the acceptance is kernel-only.

statement_fidelity_2/: The second independent statement-fidelity cycle of 2026-10-02 for L17: the blind review of Erdos.L17.statement against the frozen English statement, verdict refutation-failed, its distinct grade, pass with tier 2 asserted, kernel-only, bound to the lean/ tree the non-author clean gate of 2026-09-29 checked, and the reviewer's census scripts.


The current record holds the second-cycle independent whole-statement fidelity review of 2026-10-02, verdict refutation-failed, the distinct grade that asserts tier 2 for L17, kernel-only with zero compiler axioms, bound to the lean/ tree the non-author clean gate of 2026-09-29 checked and cited there, and the reviewer's census scripts; the assertion is in force from the filing that cites the grade and the gate together. The clean gate of 2026-10-08 holds the non-author runner's receipt, captured log and wrapper for the whole lean/ tree as it stood on 2026-10-08T13:58:11Z (exit 0, AUDIT PASS over 1 claim with 0 compiler axioms, the self-test stamp matched), the gate the card's standing cites with that grade; the claim's statement is unchanged in meaning from the tree the grade examined to that tree. The earlier record holds the first acceptance of 2026-09-25: its fidelity review, distinct grade, non-author clean-gate receipt with its log and wrapper, the native binding with the English subject's extraction rule, and the acceptance warrant, for a branch tree as it stood on 2026-09-25T03:40:15Z, which the default branch never carried; it is retained as an assessment of that subject, its extension rule reaches no later tree, and no delivery confirmation was filed under it.