Skip to content

VR and ZTL

VR and ZTL (Zero-Trust Logic) are connected in two directions, and both connections are in code:

  • VR reads its own objects through ZTL's values;
  • ZTL builds part of its analysis on VR's numbers.

Each Lean object named below was opened on 2026-10-30 and its statement read; the wording here was then checked against the statements by a separate reader. VRCycle was at commit 87d2e79 (its guard re-run that day: all checked declarations on the empty list) and ZTL at 5028e75.

VR → ZTL: VR Part II

The paper is VR Part II: Raising VR onto Zero-Trust Logic (10.5281/zenodo.21326038). Its Lean half is VR/ZTL/, inside the guarded VR library, so every object below is on the empty axiom list.

The value kernel, vendored (VR/ZTL/Kernel.lean). ZTL's values T, F, Z and its connectives are copied verbatim from lean/ZTL.lean of inventor1975/ZTL at commit 3c5ff34 (2026-07-12). Only the subset VR needs is copied. A connective returns T only if T is forced under every classical reading of Z; this is the rule. The kernel is a pinned copy, not a dependency: nothing in Lean ties VRCycle.ZTL.V to ZTL's own V. On 2026-10-30 its definitions (subs, lift1, lift2) were compared by hand with ZTL's current ones and were still identical.

Identity atoms are ZTL atoms (VR/ZTL/Atoms.lean). In VR's set universe, identity is a witnessed bisimulation. EqVerdict x y turns that into a ZTL verdict with three cases:

  • earned T carries the bisimulation itself;
  • earned F carries a refutation;
  • unexamined has the value Z. zero_trust_start states this, and the proof is rfl.

Soundness holds by construction: sound_T and sound_F return the witness the verdict carries. Further results:

  • The rules refl, symm and composeT build new witnesses from old ones.
  • On the operational naturals every identity atom gets decided (vnVerdict_ne_Z, vnVerdict_T_iff).
  • The Quine atom: Ω ≈ Ω is earned by refl (as for every set), while Ω is not well-founded (quine_orthogonality) — being ungrounded does not block an earned identity.
  • For propositional formulas over the six connectives, given that every atom is decided (T with its fact or F with its refutation), the vendored kernel's value is T exactly when the formula is classically true, and never Z (earned_register_classical).

Choice sequences (VR/ZTL/Stages.lean). A growing binary sequence is the continuum's Branch. A node (a finite segment that has already been performed) forces a property when every branch through it has the property (Forces). Forces is stated with Lean's own booleans; no theorem relates it to ZTL's values. Part II reads the stages as ZTL's "lazy register" — that reading is an analogy, and Lean proves separate facts, some about Forces, some about the table:

  • forces_mono: a verdict forced at a node stays forced at every extension. A verdict earned at a stage survives every later choice.
  • identity_forced_at_root: at the root, every branch has α 0 → α 0; separately, identity_greedy_abstains: ZTL's table gives Z → Z = F.
  • ladder_overclaims: the table gives ¬¬Z = T; separately, atom_not_forced_at_root: the root does not force α 0 = true (a longer node, such as [true], does).
  • stage_eq_super: for a property of the first H bits, forcing at a node equals quantifying over all completions to length H.
  • eq_never_forced: no node forces "all branches through it are equal".
  • apart_earned: one disagreeing bit earns apartness.

The survival criterion (VR/ZTL/Survival.lean, ledger ZTL_SURVIVAL.md). It is a bookkeeping convention adopted by the author on 2026-07-12: a proof whose measured axiom footprint contains no Classical.choice is called surviving the move onto ZTL. It is not a Lean theorem; the argument that such proofs are chains of rules ZTL keeps rests on a measured Python battery (14 of 14 rules), not on Lean. Since the whole VR library is now on the empty list, every VR proof meets it, so it no longer discriminates inside VR. What Lean checks are the spot-checks, which rebuild flagship results as verdicts that carry certificates:

  • extVerdict: strong extensionality yields earned identity;
  • afaVerdict: two decorations of one graph have earned identity at every vertex;
  • MemVerdict and memCongrVerdict: membership as a carried verdict, transported along earned identity;
  • apart_earned in Stages.lean.

The ledger itself warns that the audit bounds the given proof, never the theorem. Its counts were measured on 2026-07-12 (405 audited public objects), before the September 2026 move of the whole VR library to the empty list.

ZTL → VR: VR's numbers inside ZTL

Since 2026-10-10, part of ZTL's analysis uses VR's operational numbers directly. lean/ZSlope.lean and lean/ZExp.lean import VR.Numbers.RealsOp; about 45 further analysis modules depend on them. The logic core (the tables, the laws, the judge's theorems) does not use VR.

  • ZSlope proves the derivative-sign rule of ZTL's certificate checker, for expressions built from +, − and × over constants and quantities, over VR's rationals (QExpr) by slopes (exp is added in ZSlopeExp). It does not use the mean value theorem (slope_sound, certificate_sound_E).
  • ZExp defines exp on VR's operational reals, with an explicit Cauchy modulus (rexp, rexpR). Its rational brackets are proved sound (bracket_sound).
  • Among the modules built on these two: ZSlopeExp, ZRecip, ZExp2, ZTaylor2, ZIntegralR.

The numbers are read from VRCycle, not copied. In lean/lakefile.toml the library VRNumbers builds only the import closure of the numbers. That closure is seven VR modules, from VR.Arithmetic to VR.Numbers.RealsOp, with no Mathlib. The CI workflow (.github/workflows/lean.yml) checks out inventor1975/VRCycle at the pinned commit de72f58 (the seven number modules are identical there and at 87d2e79). When it counts ZTL's axiom-free theorems, it leaves VR's own #print axioms lines out.

The boundary: VR does not reason in ZTL

VR's papers say that VR generates no logic of its own. VR. A Formal System (v1.1.1) says the logic VR reasons with is metatheoretic, borrowed from the ambient framework. In practice, Lean checks VR's proofs in Lean's type theory, using none of Lean's three axioms. Inside VR, ZTL's values are a data type (VRCycle.ZTL.V), and verdicts about VR's objects are built from them. The reasoning about those verdicts is still Lean's.

Part II states the thesis "VR always stood on ZTL". It is a reading of the survival convention above, not a theorem: VR's proofs avoid Classical.choice. It does not say that VR's theorems are derived inside ZTL's calculus. The comments in VR/ZTL/Kernel.lean and VR/ZTL.lean said "ZTL never depends on VR" until 2026-10-30, when they were corrected (VRCycle 2bc5cee): the vendored kernel is still a one-way copy, but since 2026-10-10 ZTL reads VR's numbers.

The other direction works the same way. ZTL uses VR's definitions and theorems as code, not as a logic. For ZTL's own results, see Useful theorems.