What ZTL does not do

Each item is one plain sentence, then the evidence: a Lean theorem, a script or a file in inventor1975/ZTL, read on 2026-10-30. Counts marked MEASURED were produced by running the named script on 2026-10-30, on a checkout at commit 4622dbe; the last commit that changed lean/ is b84526e, and 4622dbe changes only CI workflow files. A count holds for what the script enumerates, not beyond it. The repository keeps its own list of ceilings and unfinished work in KNOWN-LIMITS.md; this page does not replace it.

What it judges

ZTL does not check grounds: it judges whether a claim follows from the grounds as you declare them. Evidence: the signed receipt says so in its attests field, and admitted: true means only that the claim follows from the declared grounds (signed verdicts). A row there is one line of the document's table: a name, what it means, and its status; anyone can give a row the status verified.

It does not know what is in a Z box. Z says only that an input is not verified and may differ between two reads; it carries no probability, no reason and no source, and a "no" on a Z is "not established", not "false". Evidence: the rule. For the finite threshold model in lean/ZIgnorance.lean: when the threshold lies strictly inside the known range, the verdict is Z and stays Z under every strictly increasing relabeling (ZIgnorance.verdict_reparam_invariant), while uniform priors on the quantity and on its square give different numbers (ZIgnorance.bertrand_two_numbers, one numeric inequality, 2/5 against 2/17). A missing subject is a different case, and the judge sees it only when you declare it (the E marking in ztljudge.py).

It cannot tell whether two external documents are independent, or whether two names refer to one external document. Between claims it can: a shared ancestor refutes a declared independence by name. Evidence: KNOWN-LIMITS.md, "Ceilings": both are recorded as unverifiable between external documents; the ledger discloses the assumption and prices it, but does not detect it. The check between claims is stated there too.

It finds only the dependencies someone wrote down. A ground nobody linked to a claim is invisible to it. Evidence: KNOWN-LIMITS.md, "Citations are honoured, never discovered".

What a verdict promises

A T as written can be on credit: a later verification can turn it into F. ¬¬p with p unverified is T as written, and F once p is verified F. Evidence: ¬¬Z = T (ZNull.not_the_greedy_register, lean/ZNull.lean), and at p = F the value is classical F (evalF_agrees); judge in ztljudge.py labels ¬¬p on a dirty p ON CREDIT (computed on 2026-10-30, see ZTL and other logics). In general, the decisive ¬ and ∧ are not monotone in the information order (V.eager_not_not_monotone, V.eager_and_not_monotone, lean/ZTL.lean).

It does not certify classical tautologies on unverified input. p → p and p ∨ ¬p are F as written when p is Z. Evidence: V.imp_refl_needs_ground, V.lem_needs_ground (lean/ZTL.lean); not_conversely (lean/ClassicalAgreement.lean). MEASURED over the regression pool (every formula of depth at most two over p and q, 2 906 distinct): ZTL validates 212 formulas when atoms may be Z, against 584 on verified valuations (publications/core-logic/paper_numbers.py, sections A and D). These counts describe the pool, not the logic. The judge reports p → p as EARNED IF STABLE, not EARNED (next section).

Fourteen of the twenty-six classical laws on its list do not hold when an atom is Z, among them both De Morgan laws, double negation, contraposition and excluded middle. Evidence: the 26 laws, each with a counterexample and a Lean theorem; MEASURED, audit.py: 12 hold with Z, 14 do not.

The deduction theorem works in one direction only: p → p is not T on a dirty p, though concluding p from p is trivial. Evidence: V.dt_one_way (lean/ZTL.lean) states only Z → Z = F, the failing direction; the other direction is a trivial rule and is not stated as a theorem.

A compound formula never answers Z. ZTL cannot express a function that returns "unknown" for a compound; it answers T or F at the first connective. Evidence: V.evalF_classical (lean/ZTL.lean). MEASURED by exact enumeration of all binary functions on T, F, Z (paper_numbers.py, section C): the binary functions ZTL defines are the 2 projections and the 512 functions into T and F, 514 in all; only the projections take the value Z.

Verifying is not the only thing that happens to data, and the other things are not covered. An expiry or a revocation can undo a verdict that no verification could undo. ZTL has no physical clock. Evidence: ZClock.revocation_breaks_hereditary, ZClock.only_revocation_takes_back (lean/ZClock.lean); the preprint, section 7 ("ZTL owns no physical clock").

The judge's caveats

EARNED IF STABLE assumes that each dirty atom stands for one fact at all its occurrences. If a value can change between two reads, the claim was not shown true under every reading; only EARNED (strong Kleene T) was. Evidence: the docstring of judge in ztljudge.py; V.Speak.lnc_if_stable (lean/ZSpeaks.lean): ¬(p ∧ ¬p) on a dirty p is EARNED IF STABLE while its strong Kleene value is not T. MEASURED over the 14 530 dirty cells of the regression pool (paper_numbers.py, section P): 2 440 EARNED IF STABLE and 1 470 REFUTED IF STABLE, none of them strong Kleene T or F. Of the 2 440, 950 are also a hereditary T as written (T now, and under every partial verification); the other 1 490 are not: their value as written is F, or some partial verification changes it.

The stability search stops at 16 repeated dirty atoms. With 17 or more, the judge does not search the cleanings; a claim true in every cleaning can then be reported OPEN, with "stability not searched" in its reason. Evidence: the constant _STABLE_CAP = 16 in ztljudge.py (at most 2^16 passes). MEASURED on 2026-10-30 with the snippet under Recompute: on the disjunction of (pᵢ → pᵢ) over n dirty atoms, n = 16 gives EARNED IF STABLE and n = 17 gives OPEN. Above the cap the judge can still report IF STABLE when the warranty grade settles the claim.

Deciding exactly whether a T survives every verification is coNP-hard, so no exact fast check is expected unless P = NP; the one-pass gate that is proved sound does not pass some claims that are in fact safe. Evidence: ZHeredTaut.hereditary_iff_taut proves that, for one family of formulas, surviving every verification is equivalent to being a tautology; coNP-hardness follows by the standard result on tautology checking, which is not formalized. ZRuntimeGate.gate_sound: what the gate passes survives every verification. ZRuntimeGate.gateC_steps: in the Lean cost model, one step per formula node; the Python run time is not proved. ZRuntimeGate.gate_incomplete: ¬(a ∧ ¬a) with nothing verified survives every verification and the gate does not pass it.

Your modelling choices

Which atoms are dirty is your input, and ZTL does not check it. Evidence: the rule; ztljudge.py: a marking says which atoms are verified and which are not.

Whether two occurrences are the same read is your choice. ZTL reads each occurrence of a dirty atom on its own; if your program reads a value once, write it once. Evidence: the rule; the result can differ: p ∧ p is F at p = Z, and p is Z (the idempotence row of the 26 laws, V.and_idem_needs_ground).

That ¬Z = F is the right table is a design choice, not a theorem. What is proved is narrower: if every connective must return the strong Kleene value settled to T or F when applied to atoms, then every compositional semantics that does so agrees with ZTL on every formula, and none of them keeps De Morgan's law. Evidence: V.ztl_unique_compositional, V.verdict_everywhere_excludes_de_morgan (lean/ZDirty.lean); the preprint, section 7: the fourteen refutations follow from three fixed design forks.

Proof and program

The Lean proofs are about the Lean definitions. Whether those definitions match the prose on this site is for the reader to judge. Evidence: what is proved. The repository's CI runs inventory/axiom_audit.py, which checks with #print axioms that every theorem depends on no axiom. On 2026-10-30 the CI runs for commit b84526e (the last change to lean/) finished with success, the Lean build and the regression suite both; for 4622dbe the Lean run had succeeded and the regression run was still in progress when this page was written. This page did not re-run the audit locally.

The Python judge is not proved, and only part of it is cross-checked. The Lean model in lean/ZSpeaks.lean has six dispositions and proves that every claim gets at least one (V.Speak.dispositions_partition; that they exclude each other is not part of that theorem). The program is a separate implementation, with a seventh disposition, E, for a subject declared missing. Evidence: MEASURED, paper_numbers.py, section P: on 14 530 dirty cells, the program's EARNED (2 450) and REFUTED (1 274) agree with an independent strong Kleene evaluation. EARNED IF STABLE, REFUTED IF STABLE, ON CREDIT and OPEN are compared with no independent computation: the same section checks only that strong Kleene is undecided there and that the counts match the stored ones. conformance/ztl_table.py fingerprints the judge's output over every depth-two formula and marking; by its own description it records what the judge does and does not verify it. bridge.py compares Lean and Python on connective tables, both registers, the judge's label of dirty atoms and engine verdicts, not on dispositions. We found no script that compares the program's dispositions with the Lean model (searched 2026-10-30).

It is not a theorem prover for arbitrary mathematics. It judges claims built from atoms by connectives; its first-order proof search is proved sound, and complete only in its finite half. Evidence: ZParamHintikka.closed_or_stuck_decides, ZParamEngine.entails_of_closed; the remaining half ("a valid sequent closes at some fuel") is an argument, not a theorem (section XVI of useful theorems). KNOWN-LIMITS.md also records that nothing finds the relevant stored claims for a new question (no premise selection).

A measured count holds for what was enumerated. Three kinds of count appear on this page. Evidence: (1) over the regression pool, every formula of depth at most two over p and q, built by publications/ztl/core_logic_checks.py (MEASURED, paper_numbers.py, section A: 2 926 entries, 2 906 distinct): the 212 and 584 validities, the 14 530 dirty cells and the disposition counts; (2) exact enumerations of a finite space: the 514 binary functions, and the 26 laws over every assignment of T, F, Z (audit.py); (3) single runs of a stated example: the 16 and 17 repeated atoms below.

The scripts check numbers, not the sentences around them. A count can be reproduced while the prose that interprets it is wrong. Evidence: KNOWN-LIMITS.md, "Numbers, not prose". This page is prose too.

Recompute

From a clone of the ZTL repository, at its root:

python3 audit.py
python3 publications/core-logic/paper_numbers.py   # sections A, C, D, P
python3 -c "
import ztljudge
for n in (16, 17):
    claim = ' | '.join(f'(p{i} -> p{i})' for i in range(n))
    print(n, ztljudge.judge(claim, {f'p{i}': 'Z' for i in range(n)})['disposition'])"

The last command prints 16 EARNED IF STABLE and 17 OPEN.