Useful theorems

These are theorems of ZTL that have a human reading. The one criterion for the selection: a theorem must say something to a person — a lawyer, a philosopher, an investigator, an auditor — and not only about the inner workings of the calculus. Mechanics (congruences, lemmas used inside proofs, the connective tables themselves) is left out.

The selection was made by the author in September 2026 and extended on 2026-10-30 with theorems added to ZTL since then (sections XVIII–XXII, and the last entries of sections IV, IV-bis, VII and XI). Every theorem named below was opened and its current statement read on 2026-10-30, at commit b84526e of inventor1975/ZTL; the Lean files of the September entries are unchanged since commit 08f9df2, where they were first checked. Where a reading said more than the statement proves, the reading was narrowed to what is proved. The translation and the check were done with Claude (Anthropic); the author directs the work and is responsible for it.

Each entry has the same shape:

• a statement in bold, followed by what it means for the person handling a case;
• Proved — what the Lean statement says. The bold line and the reading claim no more than this line; where they add an interpretation, it is marked as one;
• Where — the file and the theorem's name, so you can go and check.

Many results are proved on a small test model or for a single example. They say so: one example refutes a general law, but it does not establish one.

No axioms. The theorems on this page use no axioms: no excluded middle, no choice. The repository's CI runs #print axioms on every theorem of the Lean corpus (inventory/axiom_audit.py) and fails if any one depends on an axiom; on 2026-10-30 the same check was also re-run locally for every name on this page. The one classical proof mentioned below (section VI) is kept outside the corpus on purpose. To check a theorem yourself, put #print axioms and its name (for example #print axioms V.no_gift) in a Lean file that imports its module; Lean answers 'V.no_gift' does not depend on any axioms.

Some entries also give a Measured figure: a count from a script run before the proof was written, over a bounded set of formulas. A measurement is not a theorem, and the page keeps the two apart. "The paper" below is the ZTL preprint (see what is proved).

Words used below. An atom is T, F or Z. Z marks a dirty atom: an input that is not verified, not yours, and may change between two reads (the rule). A ground is an input fact a claim rests on; a dirty ground is one marked Z.

ZTL reads a claim in two registers, and the words T, F and Z mean different things in each.

• The decisive register is the ZTL tables themselves (all 16 tables). In it every compound formula is T or F, never Z; Z stays on the atoms. This is the value as written, and it is what the page calls a verdict. Each connective returns T only if T is forced under every reading of the values it reads, but a compound reads the verdicts its parts already recorded. So a T as written need not be earned: ¬¬p with p dirty is T as written, and the judge calls it ON CREDIT. An F as written means "not established", not "shown false".
• The cautious register is strong Kleene logic. In it Z passes through to compound formulas: a claim it cannot decide is Z. Its T is earned — true under every reading of every occurrence of the dirty atoms — and the judge reports it as EARNED; its F is false under every reading, and the judge reports it as REFUTED.

To verify (or refine) is to replace some Z's by T or F; a completion — the judge's cleaning — replaces all of them. A T as written is hereditary if no verification changes it (section IV). Several newer files name this grade earned or Earned in their identifiers; it is not the judge's EARNED, which is the cautious T. The prose below says "hereditary T", or settled where a section defines it so.

---

I. A refusal and its reason

The newest part when this selection was made, and in the author's view the most useful in practice.

A refusal does not hide a ground that could change the answer on its own.

When the cautious reading leaves a claim undecided, the judge's receipt (the label) names dirty grounds. A dirty ground that is not on the label cannot change the answer when it alone is set to T or to F. Changes made to several unnamed grounds at once are not covered by this theorem.

Proved: if a dirty atom is not on the label, then setting that one atom to any value leaves the cautious answer where it was. The same holds for the decisive register.

Where: lean/Receipt.lean, V.receipt_complete; for the decisive register, V.receipt_complete_greedy.

And it names nothing extra — if the claim never reads one dirty ground twice.

This is the other side, and without it the first half is of little use in practice. A list in which half of the named items affect nothing does not let you work: you do not know where to start. The theorem says: in a claim where no dirty ground is read twice, every named ground is one the answer is really waiting on. Not "possibly important", but: there is a setting of the other open questions under which answering this one "yes" and answering it "no" lead to different outcomes.

Proved: if every dirty atom occurs at most once in the claim and an atom is on the label, then there are two ways of filling in the dirty grounds that differ only in this atom — T in one, F in the other — and give different cautious answers.

Where: lean/LabelExact.lean, V.label_exact_linear.

Measured before it was proved: 128,372 such claims (every formula of depth at most 2 over three atoms, plus random formulas of depth at most 6 over four), none where the label named something extra.

The importance of a ground cannot be tested one at a time.

A caveat without which the previous entry reads wrong. It happens that no open question changes anything on its own, while together they decide the case: in p ⊕ q (exclusive or) both grounds are rightly named, and neither moves the answer alone. So the test "what if we learned only this?" can declare unimportant what is important. The question has to be asked jointly: fix the rest, then look. The judge says so when it happens: "no single ground moves it".

Not a separate theorem: this is why the statement above fixes the other grounds jointly. The p ⊕ q example is given in the header of lean/LabelExact.lean and can be read off the strong Kleene table for ⊕.

A pending claim that reads no ground twice can still go either way.

If the cautious answer is undecided and no dirty ground is read twice, then some way of filling in the open questions gives "yes", and another gives "no". On such a claim, "not established" does not hide an outcome that is already settled.

Proved: if every dirty atom occurs at most once and the cautious answer is Z, there is a filling of the dirty grounds that makes it T and another that makes it F.

Where: lean/LabelExact.lean, V.drivable.

Measured before it was proved: 48,759 pending claims of this kind in the same bounded set, every one could be driven both ways.

Where this breaks — and it is the same place as in section XIII.

The condition "never reads one ground twice" is not decoration. In p ∧ ¬p the label names the dirty ground p, but answering p "yes" and answering it "no" give the same answer, F. This is proved as a counterexample, not left as a remark. For a lawyer: a document that relies twice on the same unverified witness is also where the verdict as written loses a conclusion (section XIII). In both cases the tables treat the two mentions as unrelated.

Proved: for p ∧ ¬p with p dirty, p is on the label, the claim reads p twice, and no pair of fillings that differ only in p gives different answers.

Where: lean/LabelExact.lean, V.clash_names_an_idle_atom.

When the cautious reading decides, nothing is left hanging.

If the cautious answer is T or F, the list of what still holds it up is empty: a case decided in the cautious register has no open debt.

Proved: if the cautious answer is T or F, the label is empty.

Where: lean/Receipt.lean, V.label_empty_of_decided.

The cautious register and the decisive one do not disagree.

When the cautious reading arrives at a definite answer, the decisive one gives the same answer. This is why the receipt works for both.

Proved: whenever the cautious register gives T or F, the decisive register gives the same value.

Where: lean/Receipt.lean, V.greedy_agrees_when_decided.

---

II. What cannot be had for free

All entries in this section are about the decisive register, unless they say otherwise.

A contradiction is rejected even on unverified data.

¬(p ∧ ¬p) is T for every value of p, Z included. Rejecting a contradiction does not require you to verify anything first.

Proved: ¬(p ∧ ¬p) is T for p = T, F and Z.

Where: lean/ZTL.lean, V.no_contradiction.

There are no two truths at once.

It never happens that p is T and ¬p is T at the same time. There are no "true contradictions".

Proved: for every value of p, not both p = T and ¬p = T.

Where: lean/ZTL.lean, V.no_gluts.

Modus ponens is alive.

If p is T and p → q is T, then q is T.

Proved: for all values of p and q: if p is T and p → q is T, then q is T.

Where: lean/ZTL.lean, V.modus_ponens.

In the decisive register the mark does not surface.

No compound formula takes the value Z there: what comes out is always T or F. On dirty data the uncertainty shows up as F — "not established" — rather than as a third value. (The cautious register does let Z through; that is its job.)

Proved: under every valuation, every formula that is not a bare atom is T or F in the decisive register.

Where: lean/ZTL.lean, V.evalF_classical.

No new laws are introduced.

Everything that is valid here is valid classically. Over its own valuations ZTL has fewer tautologies than classical logic and none that classical logic lacks: it takes away, it does not add. It is not weaker in what it can say: it can state, inside the language, that an input is unverified (section V).

Proved: a formula that is T under every ZTL valuation is true under every classical valuation.

Where: lean/ClassicalAgreement.lean, V.ztl_taut_is_classical.

Where nothing is dirty, ZTL gives the classical values.

On a valuation with no Z, the answers coincide with the usual ones, formula for formula.

Proved: on a valuation with no Z, every formula has its classical value.

Where: lean/ClassicalAgreement.lean, V.evalF_agrees.

There is a class of claims where a T as written cannot be taken back.

The most dangerous error of a judge is not a refusal but an unearned "yes": a refusal announces itself, while a T given on credit looks exactly like an honest one. (The judge reports such a T as ON CREDIT: true as written, and some verification would refute it.) The theorem names a condition under which this cannot happen: if no dirty ground stands under a negation — not under ¬, not in the "if" part of →, not inside ⊕ or ↔ — then a T as written survives every later verification, whichever grounds are settled and in whatever order. For an auditor: a claim built only from positive statements about unverified matters is covered by this guarantee; a claim that leans on "the opposite has not been shown" is not covered.

Proved: if every dirty atom of a claim stands only in such positive positions, a T as written stays T under every refinement — any subset of the dirty atoms verified, to any values.

Where: lean/NoGift.lean, V.no_gift.

Measured before it was proved: 323,530 claims in a bounded set, no T taken back inside the class.

Only "yes" is protected, and that is not an oversight.

p ∧ p with p dirty gives F — and comes alive when p is verified T. A refusal that later becomes a verdict is inquiry working; a verdict handed out on credit is a defect. Only the dangerous case is fenced off. Note that p ∧ p lies inside the class and reads p twice: the class protects against unearned T's, not against lost truths.

Proved: p ∧ p lies in the class, is F with p dirty, and is T once p is verified T.

Where: lean/NoGift.lean, V.F_is_not_protected.

But the class is narrow, and you need to know that before relying on it.

Most T's that do survive every verification lie outside the class. So the theorem gives something to build on, not a classification: "outside the class" does not mean "unreliable"; it means "without this guarantee".

Proved: one example — p → q with p dirty and q verified T is outside the class, is T, and stays T under every refinement.

Where: lean/NoGift.lean, V.fragment_is_not_necessary.

Measured: of the T's that survive every refinement, 66% lie outside the class on claims of depth 2, 97% at depth 5, 99% at depth 6.

The two halves lie on different axes.

Truth is lost through multiplicity (a ground read twice, section XIII) and given away through negation. In the measurements the two classes are not nested: there are claims where every ground is read once and a T is still given away, and claims inside the safe class where a ground is read twice and no T is given away. So the two defects need different cures, treated separately.

Measured, not proved: on the first of three measurement pools (lab/nogift/RESULTS.md in the repository), 594 claims that read each ground once give away a T; 184 claims in the safe class with a ground read twice give none away.

---

III. The price list: what survived and what fell

The value here is that this is a price list, not a complaint. Each line is a familiar move of reasoning that stops working when some grounds are unverified. On verified data every one of them holds, as it does classically (the 26 laws).

Survived (you may use them):

modus ponens · modus tollens · disjunctive syllogism · resolution · transitivity of implication · introduction and elimination of "and" · introduction of "or" · explosion (from a contradiction anything follows) · universal instantiation, proved only on a one-element domain.

Proved: each as a rule: if the premises are T, the conclusion is T, for every value of the atoms, Z included. Universal instantiation is proved as the law ∀x P(x) → P(a) on a one-element domain, with the strict "for all" (T only if the instance is T).

Where: lean/ZTL.lean, V.rule_modus_tollens, V.rule_disj_syllogism, V.rule_resolution, V.rule_transitivity, V.rule_and_intro, V.rule_and_elim, V.rule_or_intro, V.rule_explosion, V.ui_law.

Fell: excluded middle.

It is not true that p ∨ ¬p is always T. "Either yes or no" stops being a free truth when the matter is not verified.

Proved: not every value of p makes p ∨ ¬p T (it is F at p = Z).

Where: lean/ZTL.lean, V.lem_needs_ground.

Fell: removing a double negation.

"It is not true that it is not true" does not give "it is true". In practice: refuting a refutation is not a proof.

Proved: ¬¬p = p fails for some value of p; as a rule, "from ¬¬p is T infer p is T" fails too.

Where: lean/ZTL.lean, V.double_neg_needs_ground; the rule, V.rule_dn_elim_needs_ground.

Fell: De Morgan's laws.

¬(p ∧ q) is not the same as ¬p ∨ ¬q. You can no longer push a negation through a connective automatically.

Proved: each of the two De Morgan equalities fails for some values of p and q.

Where: lean/ZTL.lean, V.deMorgan1_needs_ground, V.deMorgan2_needs_ground.

Fell: contraposition as a LAW.

p → q and ¬q → ¬p stop being the same thing. The contraposition rule is still alive — the difference between "you may infer this way" and "these are the same truth".

Proved: p → q and ¬q → ¬p differ for some values; yet whenever p → q is T, so is ¬q → ¬p.

Where: lean/ZTL.lean, V.contraposition_needs_ground; the rule, V.rule_contraposition.

Fell: absorption.

p ∧ (p ∨ q) is no longer equal to p.

Proved: the equality fails for some values of p and q.

Where: lean/ZTL.lean, V.absorption_needs_ground.

The deduction theorem works in one direction only.

From "p → q is T" you may pass to "from p infer q" — that is modus ponens. The way back fails: the rule "from p infer p" is trivial, but the law "p → p is T" is not: on a dirty p it gives F. This is the shortest example of the fact that a rule and a law are different things, and the distinction is familiar to lawyers.

Proved: Z → Z is F. The forward direction is V.modus_ponens (section II).

Where: lean/ZTL.lean, V.dt_one_way.

---

IV. Verification can destroy a verdict

The decisive register is not monotone.

Learning more does not always strengthen a conclusion. Verifying an unverified ground can turn a verdict around — including a "yes" into a "no" (¬¬p with p dirty is T, and F once p is verified F). This is not a defect; it is the price of not treating the unverified as true.

Proved: the decisive ∧ and ¬ are not monotone in the information order (Z below T and F): replacing a Z by a value can change their output.

Where: lean/ZTL.lean, V.eager_and_not_monotone, V.eager_not_not_monotone.

The cautious connectives are monotone.

The cautious reading does not do this: for its ¬, ∧ and ∨, new knowledge never takes away what was reached. That is why there are two registers with different roles — one signs, the other waits.

Proved: the strong Kleene ¬, ∧ and ∨ are monotone in the information order.

Where: lean/ZTL.lean, V.kleene_not_monotone, V.kleene_and_monotone, V.kleene_or_monotone.

How deep you have to check for the guarantee to hold.

A verdict is sound if it agrees with every completion: whatever the dirty grounds turn out to be, it was right. It is hereditary if no partial verification can change it either. The second is stronger. The practical question: to certify the second, how deep do you have to look? For the family below, no check of fixed depth is enough: the depth must grow with the number of unverified grounds.

The device that shows it is simple: a chain of guards standing over the fallen law of identity. As long as at least one guard is unverified, the verdict "yes" stands. Verify all the guards as T, and behind them is a → a on an unverified a, which is F. A verdict that was sound changes because we learned more.

The practical reading: the guarantee "you can build on this" costs more the more unverified inputs a case has. For this family, this is proved, not just "we did not find a cheaper check" — up to one counting step, which is left in prose (see below).

Proved: for every number of guards, the claim (b₁ ∧ … ∧ b_{m−1}) → (a → a) with all atoms dirty is sound; it keeps its value under every verification of atoms to T that leaves at least one guard unverified; and it changes value when all guards are verified T while a stays dirty. It is therefore sound but not hereditary, for every number of guards.

Where: lean/ZFenceDepth.lean, ZFenceDepth.fence_depth_necessary, ZFenceDepth.sound_not_hereditary.

And the other half: a sound verdict cannot change once everything it reads is settled.

If a verification has settled every dirty ground the formula depends on, it agrees with a completion, and a sound verdict agrees with every completion. So a sound verdict can change only while at least one of the m dirty grounds it reads is still unsettled — that is, at depth at most m−1. Together with the first half: for a claim reading m dirty grounds, checking verifications up to depth m−1 is enough, and the guard family shows that in general less is not.

Proved: a sound verdict is unchanged by any verification that settles every dirty atom the formula depends on. Both halves are stated together as one theorem.

Where: lean/ZFenceDepth.lean, ZFenceDepth.resolved_all_marks_agrees; both halves, ZFenceDepth.fence_depth_exact.

One subtlety of wording. It is natural to say "a verification that changes the verdict LEAVES some dirty ground unsettled". But that "there is" is drawn out of a negation, and such a step needs an argument from the contrary — the whole file would have gone onto classical axioms for the sake of a nice sentence. So the positive form is proved: a verification that settled everything relevant agrees. The content is the same, read the other way round.

What is left in prose: that a check looking at fewer than m−1 grounds must miss some guard. That is finite counting, not logic, and it is stated in the file rather than formalized. Earlier, the necessity half had only been measured at m = 3, 4 and 5; the guard family is built by one rule for any m, so the proof covers every m.

Three strengths of "yes", strictly nested.

A "yes" on dirty data can hold at three strengths. The strongest is the cautious T (the judge's EARNED): true under every reading of every occurrence of the dirty grounds. Next comes a T as written that is hereditary: no verification of any of the dirty grounds, in any combination, changes it. The weakest is a claim that is T in every completion (above, sound). Each strength implies the next, and neither implication can be reversed. For the person relying on a verdict: the three are different promises, and a claim can have the weaker one without the stronger. The first implication strengthens section I (V.greedy_agrees_when_decided): a cautious T is not only the decisive value now, it is kept under every verification.

Proved: if the cautious value is T, the claim is T as written and stays T under every refinement (likewise for F); if a claim is T under every refinement, it is T in every completion. Both implications are strict: with a dirty, ¬(a ∧ ¬a) is T under every refinement while its cautious value is Z; a ∨ ¬a is T in every completion but F as written, so it is not hereditary.

Where: lean/ZTopology.lean, ZTopology.kleene_sub_earned, ZTopology.kleene_sub_refuted, ZTopology.earned_sub_super; strictness, ZTopology.not_a_and_not_a_earned, ZTopology.not_a_and_not_a_kleene_silent, ZTopology.excluded_middle_super, ZTopology.excluded_middle_not_earned. In this file earned names the hereditary T, not the judge's EARNED.

---

IV-bis. Why two registers, not one

A result of 5 September 2026 that came from someone else's field.

The algebra of provenance fits the cautious register; the decisive "or" and "and" have no neutral element.

Databases have had a ready-made tool since 2007: the provenance of a fact is written as a polynomial over its sources. A joint requirement is multiplication, an alternative route is addition, withdrawing a source sets its variable to zero. Question: does this algebra fit ZTL?

It fits the cautious register: that register satisfies all the laws of the algebra (commutativity, associativity, neutral elements, distributivity), and evaluating a polynomial in it preserves sums and products.

The decisive "or" and "and" fail at the first step: no value at all is neutral for either of them, so they do not form this algebra. The obstacle is the mark: F ∨ Z = F and T ∧ Z = F.

Interpretation, not a theorem: trust in derivations is computed in the cautious register and cashed as a decision in the decisive one, and the passage between them does not keep this structure. That is the author's answer to "why two registers — would one not do?": a single register would have to either lose the algebra or stop refusing.

Proved: evaluation sends a sum of provenance expressions to the cautious "or" and a product to the cautious "and"; the cautious "or" and "and" satisfy every semiring law (commutative, associative, F neutral for "or", T neutral for "and", F annihilating for "and", "and" distributing over "or"). No value is neutral for the decisive "or", and none for the decisive "and"; the obstacle is F ∨ Z = F and T ∧ Z = F.

Where: lean/ZProv.lean, ZProv.ev_add, ZProv.ev_mul and the semiring laws beside them (ZProv.kor_comm … ZProv.kand_distrib); the impossibility, ZProv.greedy_no_additive_unit, ZProv.greedy_no_multiplicative_unit; the obstacle, ZProv.greedy_obstruction.

Abstract interpretation: on threshold questions nothing is lost to the interval.

Program analysis after Cousot and Cousot (1977) replaces the exact set of values by a coarse approximation — an interval — and computes with it. The usual price is precision: the approximation is safe, but sometimes silent where an answer exists.

On a threshold question ("is the value below c?") the ZTL verdict from the interval coincides with the verdict from the whole set of values, in all three cells. For this kind of question, nothing is paid for the approximation.

Proved: for a threshold question, the verdict computed from the best interval equals the verdict over the whole value set — T, F and Z alike; and the interval abstraction is a Galois connection, in both directions.

Where: lean/ZAbsInt.lean, ZAbsInt.verdict_exact; the Galois connection, ZAbsInt.galois.

And where the price is paid: a repeated variable.

As soon as the same quantity enters twice, exactness can be lost. On the set {1, 3} every v − v is zero, so the answer to "is v − v below one?" is "yes". Interval arithmetic gives [0, 2] (in the file the values are natural numbers, where subtraction stops at zero) and answers "don't know". The witness is computed by the machine.

So the exactness theorem covers a single occurrence, and this counterexample shows it does not extend to a repeated one.

Proved: on {1, 3} the verdict over the values for v − v < 1 is T, while the interval computation gives Z.

Where: lean/ZAbsInt.lean, ZAbsInt.not_exact_on_repeated_variable.

The honest boundary. What is mapped is their algebra, not their database: K-relations and the annotated operators are not formalized. When this entry was written, one of the six engineering traditions the paper cites was mapped by a theorem; since then each of the six has had its algebraic core mapped (section XV) — the core, not the whole tradition. And separately: that these polynomials handle cascades, alternatives and "who was exposed" is their merit from 2007, not ours; whoever needs exactly that needs ProvSQL, not ZTL.

Dempster–Shafer theory: the verdict is a threshold on belief and plausibility.

Dempster–Shafer evidence theory has two numbers for every event: how far it is forced by the evidence (belief) and how far it is still possible (plausibility). Between them lies the gap of ignorance.

The ZTL verdict coincides with a threshold on these two numbers: "yes" exactly when belief is full; "no" exactly when plausibility is zero; the mark in between — for every finite set of possibilities, every proper assignment of evidence, and every event.

Proved: for every finite frame, every mass assignment that is proper (positive weights, no weight on the empty event, at least one piece of evidence) and every event: the verdict is T exactly when belief is full, F exactly when plausibility is zero, and Z otherwise.

Where: lean/ZDempster.lean, ZDempster.verdict_is_threshold.

And here the theorem caught an error that the measurement had not. The first version required only positive weights — and was false. If weight may sit on the empty event, or if there is no evidence at all, the F cell fails: the verdict comes out T vacuously while plausibility is zero. The fix is the standard condition of Dempster–Shafer theory: the empty event carries no weight, and there is at least one piece of evidence. On the one assignment where this had been measured, the condition held by itself and was invisible. One checked case cannot show a condition it happens to satisfy; that is one reason to prove as well as measure.

The two registers are one adversary with two scopes.

Picture the owner of a dirty ground as an adversary who answers each read of it so as to make the claim fail. If the adversary plans across the whole claim at once, what survives is exactly the cautious T. If every connective is a separate check — the adversary answers the reads of that check, and the check's result is recorded and passed on as a settled fact — what survives is exactly the decisive table. ¬¬p with p dirty shows the difference: it passes every separate check (the inner check fails and is recorded as failed; the outer one reads that record), but the whole-claim adversary simply reads p as false.

Interpretation, not a theorem: the decisive register is the logic of a procedure that records each check as it goes; the cautious register is the logic of one judgment over the whole claim. The answer to "why two registers" is then: two scopes of the same distrust.

Proved: a formula survives every strategy of the whole-formula adversary if and only if its cautious value is T; with one check per connective, the recorded result of each check is T exactly when the decisive value is T, and what a check reads of an argument is exactly the readings of that argument's decisive value; whatever survives the whole-formula adversary is T as written; ¬¬p with p dirty is T as written and does not survive the whole-formula adversary.

Where: lean/ZGames.lean, V.formula_scope_is_kleene, V.check_scope_is_ztl, V.formula_safe_implies_checks, V.scopes_differ. That reading each occurrence on its own is the cautious register: lean/ZDirty.lean, V.rd_is_kleene.

The decisive tables are not a free choice — and De Morgan's law is their price.

Suppose you want every single check — one connective applied to grounds — to return the cautious verdict and then settle it: T if the cautious value is T, F otherwise. Then there is nothing left to choose. Any compositional semantics that does this on each of the six connectives applied to atoms agrees with ZTL on every formula. And no such semantics can keep De Morgan's law ¬(p ∧ q) = ¬p ∨ ¬q. Applying the same settling step only once, at the end of the cautious reading, is not compositional at all.

Interpretation, not a theorem: the fallen De Morgan law (section III) is not a defect of these particular tables; it is the cost of having a verdict at every step.

Proved: any semantics given by tables for ¬, ∧, ∨, →, ⊕, ↔ that agrees, at every valuation, with "cautious value, then T if T, else F" on ¬p and on p ∘ q for each binary connective, agrees with ZTL on every formula at every valuation; ZTL's own connectives have this form; no semantics satisfying the hypothesis makes ¬(p ∧ q) and ¬p ∨ ¬q equal at every valuation; and no table computes the settled cautious verdict of ¬φ from the settled cautious verdict of φ.

Where: lean/ZDirty.lean, V.ztl_unique_compositional, V.verdict_everywhere_excludes_de_morgan; ZTL's connectives in this form, V.not_is_up_kleene, V.and_is_up_kleene and their neighbors; the end verdict, V.kleene_end_verdict_not_compositional.

---

V. Self-reference: the liar, revenge, the carousel

The liar has no value in the register of verdicts.

Negation has no fixed point in the decisive register: no value equals its own negation. The liar is homeless where signatures are issued.

Proved: for every value v, ¬v ≠ v in the decisive register.

Where: lean/ZTL.lean, V.liar_homeless.

…and has a home in the cautious register.

There ¬Z = Z. The liar lives there without breaking anything.

Proved: the strong Kleene negation of Z is Z.

Where: lean/ZTL.lean, V.liar_kleene_home.

Jourdain's carousel has no value in the decisive register.

"A has the same value as B" and "B has the value of not-A" cannot both hold for any decisive values — all nine pairs are checked. In the cautious register it does have one: both Z.

Proved: no pair of values a, b satisfies a = b and b = ¬a with the decisive negation; with the cautious negation, a = b = Z satisfies both.

Where: lean/ZTL.lean, V.carousel_no_model; the cautious fixed point, V.carousel_kleene_fp.

Quarantine is recognizable from inside.

"This ground is unverified" can be said inside the language: isZ x = ¬(x ↔ x), and it gives T exactly on an unverified value. That ability has a price, called the avenger's door: the revenge sentence "I am not true, or I am unverified", evaluated at Z, gives T as written — while the sentence itself is not granted truth.

Proved: isZ is T on Z and F on T and on F; ¬Z ∨ isZ(Z) is T.

Where: lean/ZTL.lean, V.isZ_detects, V.revenge_bullet.

Curry is the same: homeless among verdicts, at home in the cautious register.

Proved: no value v satisfies v → F = v in the decisive register; in the cautious register Z → F is Z.

Where: lean/Facts.lean, V.curry_homeless, V.curry_kleene_home.

Yablo: a wall that cannot be seen at any finite step.

Take an infinite queue of statements, each saying: "everyone standing after me is lying". None refers to itself — and still there is a contradiction.

Three things are proved, and together they locate the wall.

First. Every finite cut of this queue, of any length, allows only one assignment of T and F: the last statement is true (nobody stands after it, so its "everyone after me lies" is vacuously true), and all earlier ones are false. At a finite step there is nothing to see.

Second. The infinite queue admits no assignment of T and F at all.

Third. It does have a state in the cautious register: "everything Z" is admissible. The same pattern as for the liar and Curry: homeless where signatures are issued, housed where they are withheld. Only for Yablo this could not be seen at any finite step.

Proved: any admissible T/F assignment to a finite cut is the one described (that this assignment does satisfy the cut is a direct check, not stated as a separate theorem); no admissible T/F assignment to the infinite system exists; the all-Z assignment is admissible in the cautious register. Two things are assumed rather than derived: that each sentence carries T or F, and the reading of "every later one is false" as "every later value is F". A reader who rejects that reading rejects the theorem with it.

Where: lean/ZYablo.lean, ZYablo.trunc_unique, ZYablo.yablo_greedy_homeless, ZYablo.yablo_lazy_home.

And why this was worth doing here. The textbook proof of Yablo goes: "not everyone after me lies, so SOMEONE after me tells the truth." The second step pulls a witness out of a negation, and it is classical; here it would have moved the whole file to classical axioms.

It is not needed. If everyone after i lies, then everyone after i+1 lies too — and then i+1 must be telling the truth, though we just said it lies. Nobody extracts a witness. That the infinite queue has no T/F assignment is proved without a single classical step — and that, in the author's view, is worth more than the result itself.

---

VI. Identity and names

Identity cannot be laundered.

Equality is never earned through a marked reference. You cannot substitute an unverified name and obtain an established identity.

Proved: in the five-individual test domain of lean/ZEq.lean, if the equality of two references is T, neither reference is marked. (For any domain, see ZEqGeneric.no_laundering below.)

Where: lean/ZEq.lean, ZEq.no_laundering.

The symmetry law falls; the rule does not.

From "a is b" you may infer "b is a". But "a is b ↔ b is a" is not a truth when the equality itself is not established. Again: rule ≠ law, and here it is about the names of the parties.

Proved: in the test domain, the biconditional a = b ↔ b = a is not T for every pair of references; yet whenever a = b is T, b = a is T.

Where: lean/ZEq.lean, ZEq.symm_law_falls; the rule, ZEq.symm_rule.

Where identity is earned, substitution is lawful.

Leibniz substitution holds: like may be replaced by like, but only on what is earned.

Proved: in the test domain, if the equality of a and b is T, then a and b are the same object, and every predicate gives the same value on both. (For any domain, see below.)

Where: lean/ZEq.lean, ZEq.eq_forces_same, ZEq.leibniz_congr.

In the test domain, indiscernible does not mean the same.

Two references about which nothing is verified give the same answer to every check in the test domain: they are indiscernible there. It does not follow that you have one object before you. Leibniz's identity of indiscernibles falls — on the unverified. The practical reading: two cases, two accounts, two witnesses that nothing distinguishes do not thereby become one; to merge them, identity has to be earned, not inferred from the absence of differences.

Proved: in the test domain, where each of the eight listed predicates reads every marked reference as Z by construction, two marked references agree under all eight, while their identity stays Z — so "indiscernible implies identical" fails there.

Where: lean/ZIndisc.lean, ZIndisc.indiscernibles_not_identical; the witness, ZIndisc.witness_is_marked.

And it falls only where a reference is unverified.

Among verified references the law holds: if nothing tells them apart, they are the same. So the failure is not "identity broken in general" but a pointer to where indiscernibility cannot be trusted.

Proved: in the test domain, two verified references that no listed predicate tells apart have an earned identity. For any domain: if a family of predicates separates verified references, two verified references on which it agrees have an earned identity.

Where: lean/ZIndisc.lean, ZIndisc.holds_on_grounded; for any domain, lean/ZEqGeneric.lean, ZEqGeneric.indiscernible_grounded_identical.

The positive rules hold in any domain.

The rules of identity are proved for an arbitrary type with decidable equality and an arbitrary choice of which references are unverified: earned equality is real identity, substitution through it is lawful, equality cannot be earned through a mark, and self-identity is earned exactly on what is verified. The failure of the identity of indiscernibles stays a property of the test domain, as a counterexample should.

Proved: each of these, for any type with decidable equality and any marking; self-identity is T exactly when the reference is verified, and Z on a marked one.

Where: lean/ZEqGeneric.lean, ZEqGeneric.eq_forces_same, ZEqGeneric.leibniz_congr, ZEqGeneric.no_laundering, ZEqGeneric.refl_iff_grounded, ZEqGeneric.refl_marked.

The quantifier step this logic refuses is the step its own soundness proof cannot make without axioms.

To work with "for all" and "there exists" over any domain, the branch search has four rules. Three of the four are proved sound on the empty list of axioms. The fourth — "it is not true that all are such, so SOMEONE is not such" — was not: its proof needs a classical step. And that is exactly the step ZTL itself declares fallen: "not everyone lies" does not give "someone does not lie".

A subtlety: the problem is not that a single case cannot be checked — each single case can. It is the survey of the whole domain, which this logic everywhere refuses to count as an act.

What is not claimed: that no choice-free proof of the fourth rule exists. The usual argument does not give one; that is all the check shows.

Proved: three of the four quantifier rules are sound with no axioms; the theorem's fourth clause is a weaker statement, not the fourth rule. The fourth rule's proof is deliberately kept outside the corpus (inventory/probes/delta_all_classical.lean, inventory/probes/delta2_step_classical.lean), and a separate script (inventory/ПАРАМЕТР-ЯРУС.py) fails if that proof ever builds without classical axioms, or if the first three stop being axiom-free.

Where: lean/ZParamSound.lean, ZParamSound.gamma_delta_sound_three.

Continued (6 September 2026): the same fourth rule in the other direction — in completeness, not soundness — needs no axioms. See section XVI.

---

VII. "The X" when there is no X

Directly about legal descriptions: "the person who signed the contract", "the instrument of the crime", "the authorized representative". The first five entries are checked on sample descriptions in the five-individual test domain; the repair after them is proved for any domain.

In the test domain, a description with a unique bearer refers.

If exactly one object satisfies the description, "the X" points to it, and its existence is established.

Proved: in the test domain, a sample description satisfied by exactly one individual denotes it, and its existence is T.

Where: lean/ZDesc.lean, ZDesc.iota_unique_denotes.

With no bearer, the reference is marked.

"The X" when there is no X does not become false: it becomes an unverified reference.

Proved: in the test domain, a sample description satisfied by nobody yields a marked reference, whose existence is Z.

Where: lean/ZDesc.lean, ZDesc.iota_empty_marked.

With several bearers, existence is not established either.

Uniqueness is not earned, so the description does not refer. "The X" when there are two X's is not an addressing error but an unmet condition of uniqueness.

Proved: in the test domain, a sample description satisfied by two individuals yields a reference whose existence is Z.

Where: lean/ZDesc.lean, ZDesc.iota_multiple_marked.

On a name with no object, excluded middle falls.

P(τ) ∨ ¬P(τ) gives F, not T. Here ZTL departs from supervaluational free logic, which makes this "super-true": ZTL marks the gap instead of papering over it.

Proved: for the sample description with no bearer, P(τ) ∨ ¬P(τ) is F.

Where: lean/ZDesc.lean, ZDesc.lem_fails_nondenoting.

"True of everyone" does not carry over to a name with no object.

The classical move — from "this holds for everyone" conclude "so it holds for this one" — does not work on a name with no object: the premise is earned, the conclusion stays unverified, and the arrow refuses. The practical reading: a general rule does not extend by itself to "the authorized representative" until it is shown that such a representative exists.

Proved: in the test domain, for one predicate, ∀x φ(x) → φ(t) is F for the non-denoting t; for a verified t the same schema is T.

Where: lean/ZFreeUI.lean, ZFreeUI.classical_ui_fails; on a name with an object, ZFreeUI.classical_ui_holds_grounded.

The repair does not patch the inference — it does not issue the permission.

Add an existence requirement to the premise, and the transfer becomes lawful. But it works not because the inference improved, but because for a name with no object the premise itself is never T: existence there is unverified. The permission is not issued, rather than issued and then revoked.

Proved: in the test domain, wherever ∀x φ(x) ∧ E!t is T, φ(t) is T; for the non-denoting t that premise is not T; for a verified t it is T, so the rule licenses something.

Where: lean/ZFreeUI.lean, ZFreeUI.free_ui_valid; the premise, ZFreeUI.free_ui_premise_undesignated; not vacuous, ZFreeUI.free_ui_not_vacuous.

The repair is not about five individuals — it holds in any domain.

The repair above was first proved by enumeration over five individuals and one predicate. It is now proved for any type with decidable equality, any marking (who is unverified), any predicate and any finite range of the quantifier. The practical reading: the repair is not a property of the example. It holds in any register of persons, any catalog of things, any database, because it rests on one thing: the existence of a name with no object is not earned, and a conjunction with it is not T. Only the repair is generalized; the failures above stay examples.

Proved: for any such domain, marking, predicate and finite range containing t: if ∀x φ(x) ∧ E!t is T, then φ(t) is T; on a marked term the premise is never T; on a verified term inside an earned universal it is T. Separately: with an empty range the premise is still not T on a marked term, so an empty range is no loophole.

Where: lean/ZFreeUIGeneric.lean, ZFreeUIGeneric.free_ui_valid_generic, ZFreeUIGeneric.premise_undesignated_generic, ZFreeUIGeneric.not_vacuous_generic; the empty range, ZFreeUIGeneric.empty_range_still_refuses.

The honest boundary of this generality. What stays finite is the range of the quantifier, not the domain. A strict "for all" has to be computed, and computing over an unsurveyable range is exactly the survey this logic refuses to count as an act. The failure of the classical transfer does not generalize and should not: it is a counterexample, and in a domain without a single mark the logic is classical and the transfer is valid there. A counterexample belongs in a witness, not in a general theorem.

A mark is not removed by applying functions — in any number of steps.

Run an unverified value through any chain of functions, even a hundred links long: in the model of the file, the output is an unverified value. The pedigree grows; the mark does not come off. In this model, applying a function to a marked element keeps the mark by definition; the theorem extends that to chains of any length.

In the model, an unmarked element appears only when a verified value is put in its place — an act of verification, not an application. In security terms this is "declassification only by proof".

Proved: any chain of functions on numbers applied to a marked element yields a marked element; a verified value is a different, unmarked element.

Where: lean/ZTaint.lean, ZTaint.no_laundering; the contrast, ZTaint.sanitizer_is_substitution.

The count is earned in exactly two cases.

How many objects are in a set where some are verified and some are marked? The answer is an interval. It shrinks to a point only when there are no marks at all, or when there is exactly one mark and no verified object.

Hence: one mark with no verified object beside it is exactly one thing, and the count is earned there although identity is not (which thing it is, is unknown). And two marks are not two things: they may be two, or one named twice.

Proved: the lower and upper bounds of the count coincide exactly when there are no marks, or there is one mark and the verified core is empty.

Where: lean/ZTaint.lean, ZTaint.card_earned_iff. The four examples from the paper became consequences, not samples.

Two witnessed clicks: in this model the count of clicks is a hereditary T, the count of things is not.

A companion to the previous entry, on one example. A detector clicks twice. Each click is witnessed; nothing witnessed whether one thing caused both (one identity atom, dirty). "There were two clicks" is T and survives every verification. "Two different things" and "one thing" are each left open: later data could settle either. Not even "one thing or two" survives every verification — it is F as written, by the fall of excluded middle on the unwitnessed identity (section III); it is T in every completion, so the judge would call it EARNED IF STABLE. In this model, verifying the identity atom as "not the same" makes "two things" a hereditary T.

Proved: in this one example (two click atoms T, the identity atom Z): "two clicks" is T under every refinement; "two things" and "one thing" are each neither T under every refinement nor F under every refinement; "one or two things" is not T under every refinement; with the identity atom verified as "not the same", "two things" is T under every refinement.

Where: lean/ZQuasi.lean, ZQuasi.occurrences_earned, ZQuasi.two_objects_open, ZQuasi.one_object_open, ZQuasi.one_or_two_not_earned, ZQuasi.count_follows_identity.

---

VII-bis. When two pieces of evidence disagree

Combining evidence means intersecting, not averaging.

Each source says within which limits the value lies. Combining is the intersection of the limits, and what remains is exactly what both allow. Checking a single value is the same operation, with a second source made of one number. Hence a consequence worth knowing: the act of checking can itself reveal a contradiction — if the checked value lies outside what was already known.

Proved: when the combination of two intervals exists, its members are exactly the values both allow; checking a value v that the evidence allows gives exactly [v, v]; checking a value above the evidence gives an empty combination.

Where: lean/ZCombine.lean, ZCombine.meet_is_intersection, ZCombine.verify_is_meet, ZCombine.verify_can_conflict.

An empty intersection is an earned "no", not noise.

If the limits of two sources do not overlap, no value satisfies both. If each source claims the value lies within its limits, at least one of them is wrong — whatever the value turns out to be.

Proved: if the combination is empty, no value lies in both intervals.

Where: lean/ZCombine.lean, ZCombine.meet_none_is_earned.

Applied to Zadeh's paradox (1984).

Two doctors, three diagnoses. Each gives a tumor one percent and disagrees with the colleague about everything else. Dempster's rule intersects, discards what intersected into emptiness (9,999 parts out of 10,000), and renormalizes the rest. In the file, renormalizing is written as discarding the conflicting weight, since the thresholds do not need the division. One part remains, all of it on the tumor. Result: "tumor, with certainty", from two one-percent opinions.

This is computed inside ZTL: by their rule, and by the threshold theorem of section IV-bis about their theory.

The ZTL reading keeps the conflict instead. The weight then stays on the empty event, and such an assignment is not proper, so the threshold theorem does not apply to it: it gives no verdict, and the conflict weight is there to see. Interpretation: that is the refusal — not "don't know" in place of an answer, but "the two of you contradict each other".

Proved: after Dempster's rule the verdict on "tumor" is T; the discarded conflict weighs 9,999; the assignment that keeps the conflict is not proper.

Where: lean/ZCombine.lean, ZCombine.zadeh_two_readings.

---

VIII. Hume's gap

The models here are minimal: a type of acts (with at least one act), a fact predicate, and, in a normed model, an "ought" predicate. No field connects facts to norms.

Facts are preserved.

Adding norms to a descriptive model this way changes no descriptive fact.

Proved: in the extension of a descriptive model by any "ought" predicate, the facts are exactly those of the model.

Where: lean/Hume_Guillotine.lean, HumeGuillotine.facts_preserved.

"Ought" does not follow from "is".

For any descriptive model there are two normed models over the same acts, in one of which some act ought to be done and in the other none. So neither "some act ought to be done" nor "no act ought to be done" follows from the descriptions.

Proved: for every descriptive model there is a normed model over the same acts where some act ought to be done, and one where no act ought to be done.

Where: lean/Hume_Guillotine.lean, HumeGuillotine.ought_underdetermined.

The bridge works — and it is necessary.

Add a normative premise and the "ought" is derived. Remove it and the same facts live with the opposite norm. Without the bridge there is no inference; with it there is.

Proved: with the premise "whatever has the fact ought to be done", the "ought" follows by modus ponens; without it, a descriptive model has a normed extension where everything ought to be done and one where nothing ought to be.

Where: lean/Hume_Guillotine.lean, HumeGuillotine.bridge_delivers, HumeGuillotine.bridge_necessary.

---

IX. Cogito

Thinking is preserved; the bearer is not.

The model: events, which of them are thinkings, and one witnessed thinking. For any such model there is an extension where the witnessed thinking belongs to someone, and an extension where it belongs to no one — with identical facts about thinking, the witnessed event included. This is Lichtenberg's world: "es denkt" (it thinks), and nobody is home. So "I" does not follow from "thinking occurs", in either direction. What does follow, with no bridge, is that something occurs ("ergo est"); "ergo sum" needs the bridge "all thinking has a bearer".

Proved: for every model of thinking there is an extension with an owned thinking and one where nothing is owned; thinking facts survive extension by any ownership predicate; the witnessed occurrence exists; with the bridge, the witnessed thinking is owned, and without it, extensions with everything owned and with nothing owned both exist.

Where: lean/Cogito_Conservativity.lean, CogitoConservativity.bearer_underdetermined; nearby CogitoConservativity.thinking_preserved, CogitoConservativity.occurrence_exists, CogitoConservativity.bridge_delivers, CogitoConservativity.bridge_necessary.

---

X. Plato

The Third Man: in one formalization, the four premises are inconsistent, in three lines.

In a Vlastos-style formalization — one over many, self-predication, non-identity, uniqueness — the premises together give a contradiction: the Form is a bearer, hence its own Form, which non-identity forbids. Not an infinite regress but immediate inconsistency. The file also shows that each of the last two premises carries it: drop non-identity and a model exists (a Form that is its own Form); drop uniqueness and a model exists (an endless tower of Forms).

Proved: no structure satisfies the four premises together.

Where: lean/Plato_Equality.lean, Plato.third_man.

Under non-identity, the chain of Forms never reaches a ground.

If nothing is its own Form, the chain "Form of x, Form of that Form, …" never stops at a Form that is its own Form. (A cycle is not excluded by this theorem.)

Proved: if f x ≠ x for every x, then each step of the chain x, f x, f (f x), … differs from the next.

Where: lean/Plato_Equality.lean, Plato.no_grounded_regress.

Exactness is zero deviation.

"Being exactly F" is "deviating from F by zero", not a separate kind of being.

Proved: for a distance that is zero exactly on equal things, equality is approximation at tolerance zero; the standard is definable from deviation data alone.

Where: lean/Plato_Equality.lean, Plato.exact_is_approx_zero, Plato.standard_from_deviation.

---

X-bis. Ignorance is not a number

Ignorance does not turn into a number by itself.

You were told only one thing: a quantity lies somewhere within its limits. You are asked: "is it in the lower quarter?" A Bayesian with a uniform prior answers with one number. A Bayesian with a uniform prior on the square of the same quantity — the same ignorance, relabeled — answers with another. Both numbers are computed, and they differ.

The ZTL answer in both cases is the same: don't know. And not by accident: the verdict does not change under any strictly increasing relabeling of the quantity, not only under the squaring of the example. The number moves; the verdict stays.

Proved: in the file's example the two priors give 2/5 and 2/17; whenever the threshold c satisfies lo < c ≤ hi (so the verdict is Z), it stays Z under every strictly increasing relabeling.

Where: lean/ZIgnorance.lean, ZIgnorance.bertrand_two_numbers, ZIgnorance.verdict_reparam_invariant.

Ellsberg's urn — why a refusal is not a judgment.

Two urns: one verified fifty-fifty, the other of unknown composition. Question: "is it no worse than fifty-fifty?" For the first urn the answer is "yes". For the second the answer is "no" — and the point is why.

Not because the second urn is judged worse. Because the claim is not forced: it is neither proved nor refuted, and the denial of the unforced is F. This is refusal by default.

Interpretation, not a theorem: a chooser who follows the verdicts takes the verified urn, and the "irrationality" of people in Ellsberg's experiment can be read as reading a mark, which a point prior has nowhere to put.

Proved: "no worse than fifty-fifty" is T for the verified urn and F for the unknown one, whose underlying atom is Z.

Where: lean/ZIgnorance.lean, ZIgnorance.ellsberg, ZIgnorance.unknown_not_earned.

---

XI. Time, epochs, expiry

Sound and hereditary are defined in section IV. An expiry returns a verified atom to Z (its epoch ended).

A hereditary verdict survives further verification.

A hereditary verdict survives any further verification step — both its value and its grade. Checks may go on; the conclusion does not change. (An expiry is not a verification step; see the next entry.)

Proved: verifying a still-dirty atom leaves a hereditary verdict's value unchanged and keeps it hereditary; a marking with no marks left is hereditary.

Where: lean/ZTime.lean, ZTime.hereditary_absorbing, ZTime.grounded_hereditary.

Heredity does not protect against a change of epoch.

A bare verified fact is hereditary under every verification — and is destroyed by one expiry. So surviving a change of epoch is not implied by heredity. Interpretation: the epoch boundary therefore needs its own treatment and cannot be left to the verification guarantee.

Proved: one example — a formula and a marking where the verdict is hereditary but does not survive an expiry.

Where: lean/EpochBoundary.lean, EpochBoundary.epochs_matter.

The grades are distinct, and are entered in order.

Verification moves in one direction, and on an example the grades do not collapse into each other.

Proved: verifying a dirty atom is a refinement — it never overwrites a verified value; on a three-atom example, the all-dirty state is neither sound nor hereditary, one verification makes it sound but not hereditary, and a second makes it hereditary.

Where: lean/ZTime.lean, ZTime.Witness.strict_ladder, ZTime.verify_refines.

Clock ticks never undo a hereditary verdict; an expiry or a revocation can, and neither is a verification.

Model "the window has closed" as a ground d that a scheduler keeps dirty while the window is open and verifies when the clock passes its end — an ordinary verification step. That the scheduler does so is its contract, not a theorem. Under that contract: while d is dirty, an action guarded by "d and …" is not T, whatever the rest says. Once d is verified, every further verification keeps its value; an expiry or a revocation can reopen it. A hereditary verdict — a permit or a refusal — keeps its value under any sequence of verification steps. If a hereditary verdict does change, the new state is not a verification of the old one: some verified ground was taken back. One expiry is enough to do that (see also the next entry).

Proved: if d is Z, then d ∧ ψ is not T, for every ψ; after d is verified to T or F, every refinement of that state keeps d's value; a hereditary verdict keeps its value under every sequence of steps each of which verifies a still-dirty atom; if a hereditary verdict has a different value in some state, that state does not refine the original; and one example — a bare verified atom is hereditary, and expiring it changes its value.

Where: lean/ZClock.lean, ZClock.open_window_blocks, ZClock.closed_window_stays, ZClock.permit_survives_clock, ZClock.only_revocation_takes_back, ZClock.revocation_breaks_hereditary.

The honest size, from the file: these are short consequences of ZTime's definitions. They say nothing about clock accuracy, or about whether a natural-language instruction was formalized correctly. They extend the entries ZTime.hereditary_absorbing and EpochBoundary.epochs_matter above from one step to a sequence.

A hereditary T needs re-checking only when one of its own grounds expires.

When grounds carry expiry dates, a T that is hereditary now does not stay so by itself: its ground may expire. But it stays hereditary for as long as the grounds it actually mentions are unchanged, whatever happens to other grounds. For an engineer: re-check a conclusion on the expiry of its own grounds, not on every change in the system.

Proved: for formulas built from ¬, ∧, ∨, → (the file's language): if the state at a later time agrees with the earlier state on every atom that occurs in the conclusion, a conclusion that was T and hereditary is still T and hereditary; one example where a ground is T and hereditary at time 0 and is not at time 1, after its expiry.

Where: lean/ZLegion.lean, ZLegion.earned_persists_if_no_expiry, ZLegion.earned_not_persistent.

---

XI-bis. From nothing, nothing

From nothing, nothing.

In classical logic truth can be minted from form: there are axioms from which something is derived resting on nothing. For a calculus whose every rule requires a premise, that cannot happen, and this is proved in general form.

Two halves, and separately they mean little.

First: ZTL has tautologies. "Not-q implies not-q" is T under every valuation, dirty ones included — because the negation of a dirty value is a firm F, and a construction built on negations is not dragged down.

Second: from an empty set of premises nothing is derived — not only by these twelve rules, but by any system of rules each of which requires at least one premise.

Together: there is a statement, T under every valuation, that no such calculus produces from nothing. In such a calculus that truth has to be brought in, as a verified premise.

Proved: ¬q → ¬q is T under every valuation, and no rule system whose every rule has at least one premise derives it from the empty set.

Where: lean/ZNoAxiom.lean, ZNoAxiom.transport_not_creation.

What is premise and what is conclusion here: that all twelve rules that survive in ZTL require some premise is a fact about ZTL's rule set, measured separately. What is proved is that this fact suffices, for all rule sets at once. The second half holds for any calculus without premise-free rules, classical or not.

---

XII. What stands on a ground

What is grounded does not depend on the order of computation.

In the cautious register's fixed-point construction, a coordinate grounded in the least fixed point carries the same classical value in every fixed point. So "grounded" is a property of the system, not of the order in which it was computed.

Proved: for the lazy jump of a system, the least fixed point exists and lies below every fixed point (Knaster–Tarski), and a coordinate it grounds has the same value in every fixed point of the same length.

Where: lean/ZGround.lean, V.grounded_absolute; nearby V.kt_fixed, V.kt_least.

Russell's set, computed: eight facts grounded, one left open.

Russell's paradox gets not a shrug but a computed classification. In a nine-fact membership system with Russell's set R, eight facts ground to T or F, and R ∈ R stays Z.

Proved: in the file's nine-fact Russell system, the least fixed point gives T or F on eight facts and Z on "R ∈ R".

Where: lean/ZExped.lean, V.russell_grounded, V.russell_verdicts.

---

XIII. Disclosure and withholding

Directly about selective disclosure in law and compliance.

There is a syntactic class of claims where withholding one ground is provably harmless.

If the withheld ground enters only "positively" — not under a negation, not in the "if" part, not in an exclusive "or" — then the verdict coincides with checking both possible values of the withheld ground. This is a sufficient condition, not the only case where withholding is harmless.

Proved: for one withheld atom that occurs only in such positions, the verdict is T exactly when it is T with the atom set to T and with the atom set to F.

Where: lean/ContextClosure.lean, V.closure_coincides.

Outside that class they need not coincide, and here is the witness.

¬¬b with b withheld: the verdict as written is T, and the completion b = F refutes it.

Proved: there is a withheld atom outside the class where the verdict is T and a completion is not T.

Where: lean/ContextClosure.lean, V.outside_fragment_fails.

No test that looks only at the form of the claim can be exact.

The same formula with the same withheld ground is safe under one disclosure and unsafe under another. So the form of the claim alone cannot decide it — you have to look at what was disclosed.

Proved: one witness — ¬(a ∧ b) with b withheld: with a disclosed as F the T survives every completion; with a disclosed as T, a completion defeats it.

Where: lean/ContextClosure.lean, V.no_syntactic_characterisation.

The verdict as written can lose a truth only where the same dirty ground is mentioned twice.

If a dirty ground occurs once, no answer that both its values agree on can be lost. Reading: this is why p → p, p ↔ p, p ∨ ¬p fall — they read p twice, and the tables treat the two reads as unrelated. For a lawyer: a document that mentions the same unverified witness twice is the only place where the verdict loses a conclusion that both values of the witness would support. (In the judge program, the IF STABLE dispositions exist for such claims: p → p is F as written and EARNED IF STABLE, see the judge. That is a property of the program, not a theorem here.)

Proved: if a dirty atom occurs at most once and both of its values give the same T or F, the verdict with the atom dirty is that same value.

Where: lean/Linear.lean, V.linear_no_loss; the label half, lean/LabelExact.lean, V.label_exact_linear.

Measured before it was proved: 280,118 claims in a bounded set, no loss at a single occurrence; unearned T's at a single occurrence: 16,586 — so giving away does not need multiplicity, and losing does.

The second half of the same: on a claim where every dirty ground occurs once, the receipt also names nothing extra (section I). The other axis — negation, along which come unearned T's — is in section II. So at single occurrence the verdict loses no conclusion, and its receipt sends you down no empty trails; it can still give away a T.

Normal form protects and costs, and both halves are proved.

On a formula in negation normal form, no T verdict with one withheld ground can be overturned by a value of that ground. And normal form does not recover honest verdicts that every completion confirms.

Proved: on a formula in negation normal form, a T with one withheld atom stays T for every value of that atom; and one witness, b ∨ ¬b, is in negation normal form, T under both completions, and not T as written.

Where: lean/ContextClosure.lean, V.normal_form_sound, V.normal_form_incomplete.

---

XIV. Relying is not the same as proving

The question came from outside, from people who assemble large proofs from pieces: the kernel certifies that a proof fits the statement. But who certifies that the statement may be relied upon — for this consequence, with this authority, in this epoch? And can the conditions of reliance simply be written into the list of premises?

The cases below are small models built by hand in the file: one formula standing for "the proof is valid", and a bundle of grounds standing for warrant, authority and epoch.

Proved does not yet mean you may rely on it.

There is a state of the case in which the proof is accepted and reliance is refused. Three cases are computed by the kernel — no warrant from the source, insufficient authority, a changed epoch — and in each the proof itself stands as it stood, while the reliance verdict does not. The fourth, the control: everything in place — reliance granted.

Proved: in each of the three cases the proof formula is T and reliance is refused; in the epoch case one and the same proof is T in both epochs while reliance is granted in the first and refused in the second; in the control case reliance is granted.

Where: lean/RelianceBridge.lean, RelianceBridge.proved_does_not_imply_eligible; the cases, RelianceBridge.case2_missing_warrant, RelianceBridge.case3_weak_authority, RelianceBridge.case4_epoch_change; the control, RelianceBridge.case1_authorized.

The reliance bundle is not a list of premises governed by weakening and contraction.

An ordinary list of premises tolerates two things: add a superfluous one and nothing changes (weakening); write one twice and it is the same as once (contraction). On the reliance side both fail. Weakening: p is T; add to it q ∨ ¬q over a dirty q — a classical tautology that "costs nothing" — and the verdict is refused. Contraction: one dirty ground relied on twice is not the same as once. Order does not matter: of the three rules that make a list a set, one survives.

Proved: the bundle connective is commutative and not idempotent; [p] gives T while [p, q ∨ ¬q] gives F with q dirty; with p dirty, the bundle [p] gives Z while [p, p] gives F.

Where: lean/RelianceBridge.lean, RelianceBridge.weakening_fails_reliance, RelianceBridge.contraction_fails_reliance, RelianceBridge.same_grounds_two_verdicts, RelianceBridge.bundle_commutative; together, RelianceBridge.neither_weakening_nor_contraction, RelianceBridge.reliance_is_multiset_not_set.

Where the layer adds nothing — stated just as precisely, and against ourselves.

On fully verified ground the verdict is classical, formula for formula, and the layer creates no new law. With a ground used once, no answer both its values agree on is lost (section XIII). The contraction failure above is shown with a ground used twice; at single occurrence the layer can still give away a T (section II).

Proved: with no mark anywhere the verdict is the classical one; every ZTL tautology is a classical one; at a single occurrence nothing both values agree on is lost.

Where: lean/RelianceBridge.lean, RelianceBridge.inert_when_all_verified, RelianceBridge.no_new_laws; lean/Linear.lean, V.linear_no_loss.

The honest ceiling, written into the file itself. What is proved is only that the reliance bundle is not identical to an ordinary hypothesis context with weakening and contraction. It is not proved that a second context is needed: that is one candidate, and the design is open. That weakening and contraction can fail is old and not ours: Girard's linear logic (1987), relevance logics, substructural logics generally. What is put forward for testing is narrow: that institutional conditions of reliance — warrant, admission, authority, epoch — fall into this resource-sensitive territory. And nothing here says whether a formal statement faithfully renders its source: that is a separate burden, and it is not lifted.

---

XV. Three foreign languages, one atom

The paper names six engineering traditions that "reinvented" this logic without knowing it. Each of the six now has its algebraic core mapped by a theorem (the cores, not the whole traditions). Three of them — about numbers, databases and contamination — speak to a person directly.

IEEE floating point: the ordered predicates are ZTL's "earned T" test, and != is where the two differ.

In floating-point arithmetic a NaN compares "unordered" with everything, itself included. The five ordered predicates — <, ==, >, <=, >= — are exactly the test "is T earned" on a ZTL atom: their "true" is ZTL's earned "yes", and their "false" merges ZTL's F with Z. The predicate != differs: IEEE asserts NaN != NaN — true. In ZTL ¬(x = x) on a mark gives F: ZTL does not assert that the unknown is unequal to itself. Their Boolean layer is already collapsed inside the predicate: != is the complement of == on all four relations, unordered included.

Proved: < is the "earned T" test of the atom x < y (and likewise for the other ordered predicates); on a mark, IEEE's x != y is true while ZTL's ¬(x = y) is F; IEEE's != is the complement of == on every relation; a NaN makes both < and >= false. Rounding, infinities and signed zero are not modeled.

Where: lean/ZNaN.lean, ZNaN.pLT_signT and its neighbors; the divergence, ZNaN.pNE_not_negation_on_mark; the collapse, ZNaN.pNE_compl; NaN false in both polarities, ZNaN.both_polarities_false.

In the arithmetic, × breaks the correspondence at one cell.

Contamination by + and − maps exactly: the mark flows the way NaN flows. But 0 × NaN = NaN for IEEE, while 0 · mark = 0 in ZTL — zero is forced under every reading of the mark, and on this cell the correspondence breaks.

Proved: the embedding commutes with + and −; 0 × NaN = NaN in IEEE and 0 · mark = 0 in ZTL, so it does not commute with × on that cell.

Where: lean/ZNaN.lean, ZNaN.emb_add, ZNaN.emb_sub; the cell, ZNaN.zero_times_mark, ZNaN.emb_mul_not_hom.

SQL has two doors with opposite defaults.

SQL's NOT, AND, OR over NULL are the cautious register, cell for cell (NOT NOT UNKNOWN stays UNKNOWN, as cautious ¬¬Z = Z; the decisive ¬¬Z = T is not that). SQL's = lands on the same ZTL equality atom as IEEE's ==. At the boundary SQL keeps two doors: WHERE lets a row through only on TRUE, CHECK on "not FALSE", so the unknown passes a constraint but not a filter. WHERE drops both x < NULL and x >= NULL; CHECK passes both. At the WHERE door SQL and the ZTL verdict agree on every condition in negation normal form; at the CHECK door they part already on TRUE AND NULL — for ZTL the constraint fails, for SQL it passes.

Proved: SQL's NOT, AND, OR are the strong Kleene connectives, and not the decisive ones; SQL's = and ZTL's equality atom coincide; WHERE drops both polarities against NULL and CHECK passes both; at WHERE the two agree on every negation-normal condition; at CHECK they part on TRUE AND NULL.

Where: lean/ZNull.lean, ZNull.toV_not, ZNull.toV_and, ZNull.toV_or, ZNull.not_the_greedy_register, ZNull.eq_atom; the doors, ZNull.where_both_polarities, ZNull.check_both_polarities; agreement and departure, ZNull.where_agrees_nnf, ZNull.check_departs_on_conjunction.

And two equalities against one.

In SQL NULL = NULL is UNKNOWN, while NULL IS NOT DISTINCT FROM NULL is TRUE: two equalities that coincide away from NULL and part exactly on it. ZTL has one: mark = mark gives Z.

Proved: the two SQL equalities give UNKNOWN and TRUE on two NULLs, ZTL's equality gives Z on two marks; on non-null values the two SQL equalities coincide.

Where: lean/ZNull.lean, ZNull.two_equalities, ZNull.equalities_agree_off_null.

When a contaminated value may be trusted again — three answers.

Denning's lattice (1976): the class of a result is the join of the classes of its operands, and it never goes down. Perl (taint mode): down by convention — extracting with a regular expression clears the bit, although the payload is the same as the tainted input's, a flow the lattice forbids. ZTL: no chain of pointwise functions applied to a mark lowers its class. All three spread contamination the same way — Denning's join — and the check at a sink is, in ZTL, the "earned T" test of the atom "verified".

Proved: the join never lowers a high class; Perl's capture lowers the class while keeping the payload; in ZTL any chain of functions on numbers applied to a mark stays high; Perl's operations, ZTL's pointwise functions, + and − all propagate by the join; the flow check into a low sink is the "earned T" test of "verified".

Where: lean/ZFlow.lean; never down, ZFlow.join_absorbs_H; by convention, ZFlow.perl_launders; ZTL, ZFlow.ztl_no_laundering; propagation, ZFlow.lvl_perlOp, ZFlow.lvl_taint, ZFlow.lvl_zadd, ZFlow.lvl_zsub; the sink, ZFlow.sink_signT.

And where ZTL is more precise than the lattice.

ZTL's multiplication returns a clean value from a contaminated operand at 0 · mark = 0, where the value is forced under every reading of the mark: the result holds no information about it, so there is nothing to declassify. With a nonzero factor the result stays contaminated. The lattice says "contaminated" at 0 · mark too: it tracks dependence in the notation, while ZTL earns independence in the value.

Proved: 0 · n = 0 for every integer; ZTL classes 0 · mark as clean; Denning's join classes it as contaminated; a nonzero value times a mark gets the join, i.e. stays contaminated.

Where: lean/ZFlow.lean, ZFlow.zero_forced, ZFlow.ztl_clears_forced, ZFlow.denning_overtaints_forced, ZFlow.lvl_zmul_nonzero.

---

XVI. When the proof search stops open

This section is about the branch search (a tableau) for formulas with quantifiers over an arbitrary domain, built and proved in Lean. It is not the judge, and "open" here is not the judge's OPEN disposition. Here is what the search guarantees in both directions: when it closes, and when it does not.

A closed run is a proof — unconditionally without the fourth rule, under its hypothesis with it.

If every branch closed, then every total model in which all premises are T gives T on the conclusion as well. Without the fourth quantifier rule the search uses only rules proved sound with no axioms; with it switched on, soundness holds for models satisfying that rule's classical step, which is taken as an explicit hypothesis rather than an axiom. The fallen bridge stays fallen in the machine: on ¬∀x P(x) ⊢ ∃x ¬P(x) the search stops without closing.

Proved: a closed run shows that every total model making each premise T makes the conclusion T (with the fourth rule, in models satisfying its hypothesis); a closed run leaves no branch with a model; on the fallen bridge the search reports "stuck".

Where: lean/ZParamEngine.lean, ZParamEngine.entails_of_closed, ZParamEngine.search_sound, ZParamEngine.run_fallen_bridge.

A new name for an unknown witness spoils nothing — if the name is new.

The rule "there exists such a one — call it c*" is lawful because assigning a name that occurs in no formula of the case changes no value. This is proved for the whole language, quantifiers included. And that the fresh name is really fresh is a theorem about the branch, not a proviso left to the caller.

Proved: reassigning a parameter that does not occur in a formula leaves every value of the formula unchanged; the name the search picks does not occur on the branch.

Where: lean/ZParamSyntax.lean, ZParamSyntax.holds_fresh; lean/ZParamEngine.lean, ZParamEngine.freshFor_fresh.

If the search with all four rules halts open, there is a countermodel with marks in it.

If the search with the fourth rule switched on halts "stuck" at some fuel, on premises and conclusion without free variables, there is a total model over the natural numbers in which every premise is T and the conclusion is not T. It is read straight off the branch: an atom marked T is T, one marked F is F, and an atom with only a weak sign on the branch, or none, is Z. A classical countermodel has no Z to give. Per the file, the fallen bridge is refuted this way, with P(c*) = Z.

Proved: for closed premises and conclusion, if the search with the fourth rule halts stuck, there is a total model over the natural numbers in which every premise is T and the conclusion is not T.

Where: lean/ZParamHintikka.lean, ZParamHintikka.stuck_refutes; the lemma itself, ZParamHintikka.countermodel_of_saturated; both directions together, ZParamHintikka.closed_or_stuck_decides.

The non-mirror cell is what this rests on.

The rule for "no" on a disjunction says: both disjuncts are "not yes". To read it backward, "both not yes" must give "the disjunction is no", and that holds because in ZTL Z ∨ Z = F. Argued in the file, not proved here: in strong Kleene logic Z ∨ Z = Z, and this weak-sign rule would be incomplete. What this logic is criticized for — tables that are not mirror images — is what carries the proof.

Proved: if neither disjunct is T, the disjunction is F; the other backward cells likewise.

Where: lean/ZParamHintikka.lean, ZParamHintikka.zor_weak; the other backward cells, ZParamHintikka.zimp_weak, ZParamHintikka.zand_weak_l, ZParamHintikka.zand_weak_r, ZParamHintikka.znot_weak.

One rule, two tiers.

The fourth quantifier rule — "not all are such, so name the one who is not" — needs a classical step for soundness (section VI): to name, you need a survey of the domain. In completeness it needs none: one named instance that is "not yes" is enough to refute "all", and no survey is needed. The axiom audit sees both sides: the completeness side is in the corpus with no axioms, and the classical soundness proof lies outside it and is checked by the script that fails if it ever builds without classical axioms.

Proved: every node of an open saturated branch is satisfied in the model read off the branch; for the case "F: for all" this uses only that a formula has one value.

Where: lean/ZParamHintikka.lean, ZParamHintikka.sat_saturated, the case "F: for all", via ZParamClosure.holds_det (lean/ZParamClosure.lean); the classical half, inventory/probes/delta2_step_classical.lean and the script inventory/ПАРАМЕТР-ЯРУС.py. With this rule the quantifier swap closes (ZParamEngine.run_swap_with_delta2), and the fallen bridge stays open even with it (ZParamEngine.run_fallen_bridge_with_delta2): "not yes" against "not no" is not a contradiction — both admit the mark.

And two defects the machine found before the proof.

Kernel runs that became theorems. Before 6 September 2026 the search on the invalid P ∨ Q ⊢ P burned fuel and never stopped: the branching rule kept firing while any successor was missing. And a valid sequent with a "generator" as the first premise did not close: new nodes went to the front and starved the old ones. Both were fixed. The lesson is worth writing down: the earlier runs (E48) checked only valid sequents, and the search had never been checked on invalid ones.

Proved: the invalid sequent is now reported open; the generator sequent closes with the generator first and last.

Where: lean/ZParamEngine.lean, ZParamEngine.run_or_elim_open, ZParamEngine.run_generator_first, ZParamEngine.run_generator_last.

The honest boundary. This is the finite half of completeness. The other half — "a valid sequent closes at some fuel" — remains an argument, not a theorem, and its parts are named: a fair strategy (now in place), König's lemma, and a total model over an infinite domain — the very survey of a domain that this logic refuses to count as an act. The input formulas must be closed.

---

XVII. Where "no" and "yes" come from

In classical logic "no" and "yes" are equals: negation just swaps one for the other. In ZTL's decisive register one cell, ¬Z = F, breaks that symmetry, and the tables acquire an order of birth. Everything here is said for pure doubt: every atom is Z, and no constant (no ready-made T or F) is allowed.

In one step, doubt gives only "no".

Any single connective applied to dirty atoms alone gives F — all six without exception. Neither "yes" nor new doubt can be had from doubt in one step.

Proved: ¬Z, Z ∧ Z, Z ∨ Z, Z → Z, Z ⊕ Z, Z ↔ Z are all F; with every atom Z, no single connective over atoms gives T.

Where: lean/ZOrigin.lean, ZOrigin.doubt_gives_F, ZOrigin.no_T_at_depth_one.

Under pure doubt, "yes" is born only through "no".

If a compound statement built on dirty atoms alone, with no constants, is T, then somewhere inside it there is a part that is F. Under pure doubt, truth is never made directly — only through a falsehood already made. For the person handling a case: from ignorance alone you cannot derive a single "yes" that does not rest on some "no".

Proved: with every atom Z and no constants, a formula whose value is T has a proper subformula whose value is F.

Where: lean/ZOrigin.lean, ZOrigin.T_through_F.

The first "yes" appears at the second step — for example ¬¬p.

"It is not true that p is not true" is T as written while p is dirty: ¬Z = F, and then ¬F = T. But this is a T about "not not-p", not about p itself — p stays dirty. It is the same cell that makes double-negation removal fail (section III).

Proved: with every atom Z, ¬p is F and ¬¬p is T.

Where: lean/ZOrigin.lean, ZOrigin.T_second.

Doubt is made by nothing — it is only given.

No compound statement takes the value Z in the decisive register: the mark lives only on atoms. Together with the entries above this gives the order under pure doubt: doubt (given) → "no" (the first thing that comes out of it) → "yes" (only through "no"). This is the Z, F, T part of the order of birth N, Z, F, T named in the paper (§4): doubt → free denial → earned affirmation. That part is now a theorem about the tables; N ("nothing", the solver's phase) lies outside the tables and outside the theorem.

Proved: with every atom Z, every formula that is not an atom is T or F, ¬p is F, and every T formula without constants has a proper subformula that is F.

Where: lean/ZTL.lean, V.evalF_classical; lean/ZOrigin.lean, ZOrigin.birth_order.

Measured before it was proved: formulas over one dirty atom — at the first step 0 of 6 are T; at the second step 84 of 246 are T, and all 84 go through an F subformula.

The honest boundary. Constants are excluded on purpose: ⊤ hands in a ready-made "yes" without deriving it, and with it "yes only through no" would be false for an empty reason. The theorem is about the values of formulas, not about whether the atoms are verified.

---

XVIII. Local facts do not compose by themselves

Close to section XIV: facts that are each in order do not, by that alone, license the conclusion that joins them. In this section a hole is a ground that is dirty now and that no future act can verify; a reachable future is one that verifies only grounds some act can still check; and settled means T as written and hereditary. The formulas of these files are built from ¬, ∧, ∨, → only.

No promotion without a composition witness.

Several facts may each be settled in their own context, while the conclusion that joins them rests on a hole. If, however the checkable grounds come out, some values of the holes make the conclusion false, then the conclusion is settled (T and hereditary) in no reachable future. Read the other way: a conclusion that ever becomes settled has a witness — an outcome of the checkable grounds under which it holds whatever the holes are. For an investigator: two reports that are each sound do not support the story that connects them if the connection rests on a question nobody can now ask.

Proved: for every formula built from ¬, ∧, ∨, →, every state of checking and every set of checkable atoms: if for every classical outcome consistent with what is already checked there is an assignment, differing from it only on holes, that makes the formula classically false, then in no reachable future is the formula T and hereditary.

Where: lean/ZComposition.lean, ZComposition.no_promotion_without_witness; the corollary for a whole bundle of claims, ZComposition.economy.

The witness is necessary, not sufficient.

h ∨ ¬h over a hole h is classically true whatever h is — it has a witness — and yet it is F in every reachable future. ZTL does not promote even a classical tautology across a hole, for the reason in section XIII: two reads of one dirty ground are not tied together. So the theorem above is a ceiling, not a test.

Proved: h ∨ ¬h is classically true for every value of h; with nothing checkable and every atom dirty, it is F in every reachable future.

Where: lean/ZComposition.lean, ZComposition.witness_not_sufficient.

Agents who each hold their own fact settled have not thereby settled the link between them.

Each agent keeps its own state of checking, and the states are merged ground by ground. A ground that no agent checked stays dirty in the merge — the merge invents nothing. So if the link between agent A's fact and agent B's fact was checked by nobody and cannot be re-checked, the joined conclusion is settled in no reachable future, however firmly each agent holds its own fact. A boundary of the model: two agents who disagree on a ground merge to Z, but the merge of three or more depends on their order and can hide a disagreement (merge [T, F, T] is T, merge [F, T, T] is Z — checked by evaluation, not a theorem).

Proved: in the merged state, an atom that is Z for every agent is Z; for any merged state, a conclusion without a composition witness is not T and hereditary in any reachable future; one example — X is T and hereditary for agent A, Y for agent B, and "X and Y and link", with the link checked by nobody and not re-checkable, is T and hereditary in no reachable future of the merge.

Where: lean/ZLegion.lean, ZLegion.merge_invents_nothing, ZLegion.distributed_no_promotion, ZLegion.local_facts_global_link.

In a tree of 2-of-3 votes, a lie needs at least 2^d of the 3^d seats — and 2^d suffice for a coalition that chooses its seats.

Some accountability schemes decide a fact by triples of triples: 3^d seats, each triple decides 2-of-3, an undecided triple says nothing, and the results are grouped in threes again. An empty seat never helps a lie: to make the top verdict false, at least 2^d seats must lie, and fewer can never do it. The same bound holds for the truth. And 2^d lying seats are enough when the liars choose where they sit: at depth 4, 16 of 81 seats — about 20% — carry the verdict over 65 honest ones. The file's reading, not formalized: on its own, such a tree is weaker than a flat majority against an adversary who picks the seats; its protection must come from elsewhere (seats drawn at random for each fact), and that is measured by simulation, not proved.

Proved: a tree of depth d gives F only if at least 2^d leaves are F, and T only if at least 2^d leaves are T; with fewer than 2^d F leaves it never gives F; for every d there is a tree with exactly 2^d F leaves and every other leaf T that gives F; at depth 4: 16 F leaves, 65 T leaves, verdict F. The triple's table is the hereditary grade of the majority formula over the three voices: T exactly when the formula is T under every refinement, F exactly when it is F under every refinement.

Where: lean/ZMajority.lean, ZMajority.lie_needs, ZMajority.truth_needs, ZMajority.few_lies_safe, ZMajority.lie_suffices, ZMajority.depth4; the triple, ZMajority.triple_T_iff_earned, ZMajority.triple_F_iff_refuted.

---

XIX. Agrippa: what a chain of reasons can give

The model: every statement is either settled by a ground (it asks for nothing further) or rests on one other statement, or on its negation. A reading of a statement is an assignment of true/false that respects every reason met along its chain. The number of readings sorts the cases. In the last entries a ground is either an act (a decidable claim, computed from its content; in the file, an equation between two numbers) or a posit (its value is set by a base — an axiom, any chosen assumption).

Only a ground gives one answer. On a finite base there is no regress; a circle has either no reading or two; and a dogma is a circle.

Agrippa's trilemma says a justification ends in an infinite regress, a circle, or an arbitrary stop. On a base of n statements the chain of reasons repeats within n steps, so a regress of distinct reasons needs infinitely many statements. A chain that reaches a ground has exactly one reading. A loop with an odd number of negations has no reading at all (the liar). A loop in which every return is even has two readings that disagree — and "p because p" is such a loop, so the arbitrary stop is the same case as the circle. The converse closes it: on a finite base, a statement has exactly one reading only if its chain reaches a ground.

Interpretation, not a theorem: the author reads one reading as knowledge, two as a value held on credit (it holds while the chosen premise holds), none as a claim that asserts nothing.

Proved: on a base of n statements, closed under reasons, the chain from any of them repeats within n steps; if the chain reaches a ground, a reading exists and all readings agree on the statement; a loop with odd parity admits no reading; a loop whose every return is even admits two readings that disagree on the statement; "p because p", the circle a := b, b := a and the circle a := ¬b, b := ¬a each have two disagreeing readings; on a closed finite base, a statement has exactly one reading value if and only if its chain reaches a ground. One example on an infinite base: the chain in which each statement rests on the next also has two disagreeing readings.

Where: lean/Agrippa.lean, Agrippa.no_regress, Agrippa.forced_one, Agrippa.odd_zero, Agrippa.even_two, Agrippa.dogma_two, Agrippa.circle_two, Agrippa.twoneg_two, Agrippa.knowledge_iff_ground; the infinite chain, Agrippa.regress_two. The same three cases in ZTL's own terms — every admissible future gives one verdict, two admissible futures give opposite verdicts, no admissible future exists — are lean/AgrippaZ.lean, AgrippaZ.forced_futures_agree, AgrippaZ.two_readings_futures_split, AgrippaZ.paradox_no_future (by the file's own account, a translation of the three theorems above).

What rests on an act is the same under every base; what rests on a posit has a rival base.

If a statement's chain ends in an act, every reading under every base gives it the same value: no choice of axioms can change it. If it ends in a posit, there are two bases under which it reads with opposite values: the rival base is always available.

Proved: chain reaches an act ⇒ any two readings, under any two bases, agree on the statement; chain reaches a posit ⇒ there are two bases and readings under them that disagree on the statement.

Where: lean/Agrippa.lean, Agrippa.act_absolute, Agrippa.posit_relative.

The limits, as the file states them: the posit half is close to definitional once posits are free parameters. Which real statement is an act and which a posit is decided outside these theorems. That an act yields a truth value rather than merely happening is a philosophical claim (Sellars' "myth of the given" is the standing objection), not a theorem here.

With "and", "or", "not": reasons with no loop and no posit give one value under every base — and a dogma among the reasons does not by itself spoil a value.

Real reasons are joined: "x because a and b", "x because a or b". On a finite base, a statement whose reasons contain no loop and no posit has a reading under every base, and one value under all of them. So acts alone suffice for a forced value. The converse is not claimed: "a dogma anywhere among the reasons spoils the value" is false. x := (0 = 0) ∨ d, with d the dogma "d because d", has one value under every reading and every base; with a false act in place of 0 = 0, the dogma decides and there are two readings again. Nor is "contains a loop or a posit" an exact mark of what fails: by the definition of a reading, x := d ∨ ¬d also has one value, with no act at all (this follows directly from the definition and is not stated as a theorem in the file).

Proved: on a closed finite base, a statement with no posit and no loop among its reasons has a reading under every base, and all readings under all bases agree on it; for x := (0 = 0) ∨ d the same holds; for the same shape with a false act, two readings disagree.

Where: lean/AgrippaNet.lean, AgrippaNet.knows_unless_loop_or_posit, AgrippaNet.act_or_dogma, AgrippaNet.false_act_or_dogma_two.

If the operational meaning of every axiom already follows operationally, posits add no operational consequence.

Put posits (a cardinal, choice, any formal assumption) beside operational statements in one language, and replace each posit by an operational formula giving its meaning — its descent. The hypothesis: the descent of every axiom of the combined theory follows from the operational theory. Under it, every operational statement that follows from the combined theory already follows from the operational one. If some descent does not follow, the theorem says nothing — which posit is harmless is asked one posit at a time. And "true however the posit is set" is not what a posit gives: "A or not A" is T with A set to T and with A set to F, and is still not a ZTL consequence of nothing, because the state where A is unsettled counts.

Proved: consequence here is ZTL's (every valuation with values T, F or Z that makes the premises T makes the conclusion T); if the descent of each axiom of the combined theory is a consequence of the operational theory, every formula with only operational atoms that is a consequence of the combined theory is a consequence of the operational theory; A ∨ ¬A is T when every atom is T and when every atom is F, and is not a consequence of the empty theory.

Where: lean/ZDescent.lean, V.conservative, V.every_base_is_not_knowledge.

---

XX. The surprise examination

The teacher announces: next week there is exactly one exam, and on its morning you will not know it is today. The class reasons backward and concludes there can be no exam; midweek it is surprised. The model uses ZTL's own clock, whose only tick is a verification. On the morning of day d, the days before d are verified "no exam", the rest are dirty. To know, in the file's definition, is to hold a hereditary T: T as written, and no further verification changes it. The refinements range over every value of the unverified days, including weeks with two exams. The model's formula for the announcement is only "exactly one exam this week"; the surprise clause is not part of it.

On no morning does the class know (hold as a hereditary T) that the exam is today — and nothing it knows singles today out.

This holds for every day, the last one included. Whatever the class does know that morning is equally true in the week where the exam is that day and in the week with no exam at all.

Proved: for every week length and every day d, on the morning of d "the exam is on day d" is not known; every formula known on the morning of d is T both in the week whose only exam is on day d and in the week with no exam.

Where: lean/Surprise.lean, Surprise.today_unknown, Surprise.surprise_guaranteed.

"Exactly one exam" is not known (as a hereditary T) before the week is over; the class's elimination is valid, in a separate classical model, only given the full announcement.

On no morning before the exam is "exactly one exam" known, and after the exam it becomes known only once every remaining day has been verified. The class's elimination step is checked in a separate classical model, not linked to the clock by a theorem: if the possible exam days are exactly the days after which a possible day remains — the condition for knowing the whole announcement, surprise clause included — then no day is possible. The teacher keeps the promise: for every exam day, "exactly one exam" is known once the week is over, and on that day's morning the class did not know the exam was that day. And the class's Monday conclusion, "no exam this week", is T as written but not hereditary — the exam day's verification overturns it: a T on credit. (On the last morning, "if exactly one exam, then today" is T as written, but only because its antecedent is not T that morning.)

Proved: in a classical model, a set of possible days in which a day is possible exactly when a later possible day remains is empty; on no morning before the exam is "exactly one exam" known; after an exam on day e, it is known at the morning of day d exactly when d is at least the week length; for every exam day e of the week, it is known at the end of the week and "the exam is on day e" is not known on the morning of e; on Monday, "no exam" is T as written and not hereditary; on the last morning, the conditional above is T as written.

Where: lean/Surprise.lean, Surprise.classical_elimination, Surprise.ann_never_known_before_exam, Surprise.ann_known_iff_week_over, Surprise.teacher_keeps_promise, Surprise.no_exam_on_credit, Surprise.last_step_conditional.

Not ours, as the file says: "the class cannot know the announcement in advance" is Quine's resolution (1953), and the liar reading for ideal knowers (Surprise.liar_when_exam_today) is Shaw's and Fitch's. What is added is that both are theorems of ZTL's existing time layer, for every week length and every formula.

---

XXI. What the judge is, in other terms

In this section "the judge" is the Lean model of its six dispositions (lean/ZSpeaks.lean). That the judge program computes the same dispositions is not proved here.

Where a guess about the dirty grounds would be right, the judge's "yes" is right too; on a single dirty ground, every guess commits and the judge does not.

A common shortcut fills in unverified grounds with a guess — all false, all true, or one at a time — and then reasons classically. Take as the standard of a right "yes" the cautious T: true under every reading of every occurrence. For any one guess and any claim: if the guess answers that claim right, so does the judge's grant (EARNED or EARNED IF STABLE). On a single dirty p, every guess grants p or grants ¬p; the judge grants neither. Stated against the judge: its grant is not always right by this standard. ¬(p ∧ ¬p) on a dirty p is granted (EARNED IF STABLE) while its cautious value is Z — and there every guess grants it too.

Proved: the judge's grant (EARNED or EARNED IF STABLE) holds exactly when the claim is T in every completion; for any completion, if it grants the claim exactly when the cautious value is T, then the judge's grant holds exactly when the cautious value is T; on a dirty p, the grant holds for neither p nor ¬p; whatever value a guess gives p, it grants p or ¬p, and neither has cautious value T; ¬(p ∧ ¬p) on a dirty p is EARNED IF STABLE and its cautious value is not T.

Where: lean/ZSpeaks.lean, V.Speak.grant_iff_enum, V.Speak.grant_right_where_substitution_right, V.Speak.grant_strict, V.Speak.lnc_if_stable; lean/ZDirty.lean, V.strict_any.

The judge's dispositions are themselves ZTL statements.

For any claim, each of the six dispositions — EARNED, EARNED IF STABLE, ON CREDIT, OPEN, REFUTED IF STABLE, REFUTED — is the T value of some ZTL formula built only from the claim's own atoms. The cautious register cannot do this even for "p is established". Interpretation, not a theorem: the judge is then not an oracle standing above the logic; what it says about a claim can be said in the logic. Per the file, not proved: the formula can be exponentially long (3^k leaves for k atoms); this is about what the language can say, not about cost.

Proved: for every formula, each of the six dispositions is, at every valuation, the T value of a ZTL formula whose atoms occur in the original; the six cover every case (that they exclude each other is not part of this theorem); every two-valued function of the values of a finite list of atoms is the value of a ZTL formula; no strong Kleene formula gives "x is established" on the valuations where every atom is x.

Where: lean/ZSpeaks.lean, V.Speak.judge_speaks_ztl, V.Speak.dispositions_partition; lean/ZComplete.lean, V.Cpl.ztl_expressively_complete; lean/ZDirty.lean, V.kleene_cannot_say_established.

ZTL is classical logic about what has been established.

Replace every atom p by two classical statements: "p is established true" and "p is established false". Every ZTL claim translates into a classical formula about these statements, and the claim is T in ZTL exactly when its translation is classically true. Interpretation, not a theorem: a T as written is a classical truth about the state of the evidence, not a guess about the world.

Proved: for every valuation and every formula, the ZTL value is T if and only if the translation is classically true when "n is established true" is read as "the value of n is T" and "n is established false" as "the value of n is F".

Where: lean/ZEvidence.lean, V.ztl_is_evidence_logic; the exactness of the translation, V.tr_exact.

In what it can express, ZTL is a known logic in another basis.

Stated against ourselves. Bochvar's external logic B^e — weak Kleene ¬, ∧, ∨ plus operators "is false", "is undefined", "is true", and the constants (Bonzio and Pra Baldi, 2025) — contains ZTL: a translation sends each ZTL formula to a B^e formula with the same value at every valuation, so consequence is the same on both sides. Conversely, every B^e formula that never takes the middle value has, at every valuation, the value of some ZTL formula. So, up to bare atoms (which can take the middle value in both), ZTL's compound formulas compute exactly the B^e functions that never take the middle value. Interpretation: whatever is new in ZTL is not in what it can express; it is in the reading — the registers, the receipts, the judge.

Proved: the translation preserves the value of every formula at every valuation; a set of premises entails a formula in ZTL if and only if their translations entail its translation in B^e (designated value T); every B^e formula that never takes the middle value agrees at every valuation with some ZTL formula.

Where: lean/ZBochvar.lean, V.Boch.zeta_exact, V.Boch.zeta_consequence, V.Boch.external_is_ztl.

---

XXII. For the engineer relying on the judge

A single linear pass never lets through a "yes" that a later verification could overturn.

At runtime you need an answer, not a search over every possible world. Evaluate the claim once in the cautious register and pass it only on T. Every pass stays T under any later verification. An expiry or a revocation is not a verification and is not covered (section XI). The cost is one step per node of the formula, the same however many grounds are dirty. With the previous pass cached node by node, re-checking after one ground changes recomputes only the nodes that mention it and gives exactly the result of a full pass. The price is stated too: the gate is incomplete. ¬(a ∧ ¬a) with nothing verified stays T under every verification (the judge: EARNED IF STABLE), yet the gate does not pass it. Such cases go to a hold, never to a false pass. Deciding exactly whether a T survives every verification is coNP-hard: tautology checking reduces to it (ZHeredTaut.hereditary_iff_taut); so no exact linear gate is expected unless P = NP.

Proved: whatever the gate passes is T under every refinement; the cost, counted as one unit per formula node, equals the formula's size for every valuation; ¬(a ∧ ¬a) with every atom dirty is T under every refinement and is not passed; after a change of one atom, the incremental re-check from the cached pass gives exactly the full re-evaluation, and the number of nodes it recomputes is exactly the number that mention that atom (the test of whether a subformula mentions it is not counted).

Where: lean/ZRuntimeGate.lean, ZRuntimeGate.gate_sound, ZRuntimeGate.gateC_steps, ZRuntimeGate.gate_incomplete, ZRuntimeGate.reval_correct, ZRuntimeGate.reval_cost, ZRuntimeGate.gate_after_change. Wall-clock latency is a measurement, not part of these theorems.

For a numeric bound, the search can be anyone's; the check is proved.

When the stand claims "this quantity stays below c everywhere in the box", the search for evidence runs anywhere and brings a certificate: a tree that splits the box into pieces, each piece closed either by an interval reading or by a monotonicity reading checked at one corner. The kernel takes no search budget; it only checks. In general form: if the readings are sound and the quantity depends only on the listed variables, an accepted certificate shows the bound at every point of the box. For expressions built from + − × /, natural powers, exp, ln, sqrt, log10, sin, cos, tan and atan, the readings are proved in Lean, and no premise is left: at every rational point of the box, the value is at most c to within every precision.

Proved: given sound readings (an interval reading encloses the value on a piece; a derivative read with a sign makes the value monotone on it) and a value that depends only on the listed quantities, an accepted certificate shows f(p) ≤ c at every point p of the box; for the grammar above, over VR's operational reals, at every point of the box with rational coordinates, for every precision ε the value's approximants are eventually below c + ε.

Where: lean/ZCertify.lean, ZCertify.certificate_sound; premise-free for the grammar, lean/ZSlopeSqrt.lean, ZSlopeSqrt.certificate_sound.

What is not proved: that the Python checker computes exactly the readings modeled in Lean. The rule and the readings are proved; their implementation is tested.

A lower bound from duality: a bad multiplier gives a weak bound, never a false one.

"No cheaper mix exists" (a feed formula) should be checkable, not taken on a solver's word. For a mix that meets every requirement and any non-negative multipliers, a lower bound on cost − Σ y·h is a lower bound on the cost. The multipliers can come from anywhere; a poor choice gives a weak bound, not a false one. The lower bound the kernel computes term by term is proved to be one, given that the expression equals its affine form with coefficients in the read intervals. In the other direction (Farkas): if a combination Σ y·h is bounded above by a negative number, then not all the multipliers and requirement remainders are non-negative — with non-negative multipliers, some requirement is not met. That upper bound is a premise here, not computed by a proved rule. This is weak duality, old mathematics; the theorems are stated over any ordered ring given by its laws, and mixes and uncertain data are the reading, not part of the statement.

Proved: over an ordered ring given by its laws: if every pair of multiplier and requirement remainder is non-negative and L ≤ cost − Σ y·h, then L ≤ cost; with the kernel's term-by-term box minimum, the only premise left is that the expression equals its affine form with every term checked; if Σ y·h ≤ M and M is not non-negative, then not every multiplier and remainder is non-negative.

Where: lean/ZLP.lean, ZLP.lower_bound_sound, ZLP.lower_bound_sound_box, ZLP.infeasible_sound.

---

What is not on this page, and why

Mechanics: congruences, lemmas used inside proofs, the connective tables, bridges between representations, tableau certificates, quantifier laws on a two-element domain, algebraic properties of clones, the internals of the branch search (substitution, rotation, decidability of closure, soundness of each single step — E43 to E48). These work, but they say nothing to a person.

The quantum results (Contextuality.mermin_square_no_valuation, Contextuality.ghz_no_valuation, QuantumWitness.*) are left out on purpose: they are real, but their human reading needs a conversation of its own, not a line.

The extension of 2026-10-30 left out the numeric machinery added since September (the certificate rules beyond the representatives in section XXII, and the real-number functions behind them), single-operator completeness (ZClone.lean) and the run-level quantum files (Hardy.lean, KochenSpecker.lean, ZFrauchiger.lean, for the reason above); see what is proved.

The readings were checked against the Lean statements on 2026-10-30. Remaining gaps are named in the entries and in the honest-boundary notes.