15 Operational sets under ZTL verdicts (VR Part II)
15.1 Position
This chapter opens VR Part II: raising VR onto ZTL — Zero-Trust Logic, the curator’s three-symbol logic of “truth is never granted on credit” (Zenodo, DOI 10.5281/zenodo.21318982; the measured Python twin of this chapter is zopsets.py, expedition E21, in the ZTL repository). Step (а) of the programme: the witnessed identity of the operational set universe (Chapter 14) is a ZTL atom discipline. An identity atom \(x \approx y\) earns T by carrying a bisimulation, earns F by carrying a refutation (apartness at a finite separation stage), and is worth the input mark Z until examined. Nothing is translated between the two sides — the disciplines coincide; the Lean development makes the coincidence a set of kernel-checked theorems.
The ZTL value kernel is vendored into VR/ZTL/Kernel.lean with a commit pin (the dependency is one-way: ZTL never depends on VR). The kernel stands on the empty axiom list, as it does at home; the whole verdict layer of this chapter is likewise Axiom profile: []; after the 2026-07-12 tier pass of Chapter 14 (Iff-rw repaid with combinators) even the vn_inj route is axiom-free, so the ENTIRE module stands on the empty axiom list.
EqVerdict x y has three constructors: earnedT holding a bisimulation witness \(x \approx y\), earnedF holding a refutation, and unexamined; val sends them to T, F, Z. Soundness is not a theorem about the type — it is its shape: sound_T/sound_F extract the certificate from the value (Axiom profile: []). The zero-trust start is unexamined (zero_trust_start: its value is Z).
refl (the diagonal), symm (the converse, verdict-preserving) and composeT (composition of carried witnesses via Equiv.trans: two earned identities earn the third) — each Axiom profile: []. The ZTL inference rules alive on \(\approx \)-atoms are not table luck; each is backed by a certificate constructor.
On the operational naturals every identity atom decides: vnVerdict n m is never Z, and its value is T exactly when \(n = m\) (F earned through vn_inj). Identity on this register is totally earnable — the Lean twin of E21 §1. Both Axiom profile: [].
The Quine atom \(\Omega = \{ \Omega \} \) earns its identity (refl gives T) while \(\neg \mathrm{IsGrounded}\, \Omega \); and \(\Omega \) earns F against \(\varnothing \) — apartness across the grounded/ungrounded divide. The cycle that dooms a sentence (the liar: permanent quarantine, an lfp leftover) is harmless in a set (identity is gfp-shaped): AFA-as-theorem is the set-side mirror of quarantine-as-theorem. All Axiom profile: [].
If every atom of a formula carries a decided, truthful verdict, then the greedy ZTL value of every formula over the six connectives is decided and truthful: T exactly on the classically true formulas, Z nowhere. Over verified identity atoms the zero-trust connectives neither lie nor refuse. Proved by one structural induction with a per-connective Decided calculus; Axiom profile: [] (empty axiom list — no propext).
15.2 Choice sequences as the lazy register (step (б))
The measured twin is zchoice.py (E22). The objects are VR’s own: a Branch of the binary spread (Chapter 13) is the sequence-in-growth, its performed segment take is the LAZY register, and the stage court Forces — what the segment forces over every continuation — is where the greedy register’s verdicts are judged. The Branch layer inherits the Continuum’s own choice-free tier (Axiom profile: [propext(, Quot.sound)]); the kernel cells are Axiom profile: [].
Node \(s\) forces \(P\) when every branch through \(s\) satisfies \(P\). Axiom profile: [].
A verdict forced at a node is forced at every extension: earned-at-a-stage survives every future choice (E22 §3: 0 revocations vs 1371 greedy deaths). The Kripke persistence the greedy register refuses as a free axiom (E12) is native to the lazy one.
The identity law, fallen in the greedy court (zimp Z Z = F), is redeemed by the stage court (every branch satisfies it) — a law of logic, not of data; while the ¬¬ ladder verdict (znot (znot Z) = T) asserts an atom NO prefix forces (the all-false branch refutes it). Raw greedy verdicts are not assertions about the future; warranted ones are (E22 §1: 0 violations for the sound grade). All four cells Axiom profile: [].
For a property read off the horizon-\(H\) segment, forcing at node \(s\) is EXACTLY the universal quantifier over all finite completions of \(s\) to length \(H\) — the world-set of the global \(\square \) (E22 §2: measured totally, 49545 pairs, then kernel-checked here). Zero trust is assertability against a maximally ignorant future; a law narrows the worlds and strengthens the stage.
Equality of branches is never forced at a finite stage (below any node two explicit continuations diverge), while apartness is earned by one disagreeing reveal and, being an \(\exists \)-fact, persists. E6 recast per-stage: stream equality is Z-permanent, apartness earnable — constructive practice reproduced by the registers.
15.3 The survival ledger (step (в))
Criterion C2 (curator, 2026-07-12): a proof survives the move onto ZTL iff it stands below the classical floor — ZTL’s fallen laws are the laws of free truth, their Lean fingerprint is Classical.choice, and a constructive proof from earned premises is a chain of ZTL-alive rules (measured: E20 rules 14/14; E21 §3 constructors; E22 §1 warranty). The four-tier axiom ledger the cycle has kept from its first work is therefore the ZTL-survival audit — “VR always stood on ZTL,” literally. The full MEASURED ledger is ZTL_SURVIVAL.md (405 live-audited objects + flagship anchors): everything VR calls operational moves; what stays is exactly what was already flagged classical by design, by substrate, or by borrowed plumbing. The audit bounds proofs, never theorems (auditor, not separator).
Strong extensionality moves as a certificate constructor (extVerdict: from member-matching data the identity witness is built); AFA-as-theorem moves (afaVerdict: decorations carry earned identity at every vertex); membership becomes a carried verdict (MemVerdict — the membership twin of EqVerdict, closing step (а)’s gap: the vn register total and classical, earned \(\in \) transported along earned \(\approx \) by memCongrVerdict). All on the empty axiom list.
What is deliberately not formalised here: the warranty ladder over partially examined registers (sound \(\supset \) hereditary, the E21 find that revised ZTL’s E12) lives and is measured in the ZTL repository; its Lean twin belongs to the ZTL corpus, not to VR.