The negative pole of lean-keep. lean-keep's tower_safe
proves the permitted side of "who gates the gate": a tower that swaps
gates — policies checked at admission time by one fixed kernel — is safe
along every reachable trace, with no gate's soundness assumed en route.
Its companion note LOEB.md argues in prose where
that stops: doing the same to the checker is blocked by Löb's theorem.
This artifact proves the blocked side, so both rows of LOEB.md's closing
table are now theorems:
| trust discipline | status | theorem |
|---|---|---|
| mediate: particular certificates, checked at admission, forever | safe, derived | Keep.tower_safe (lean-keep) |
| delegate: schema-trust in a successor's unseen proofs | inconsistent | LoebObstacle.checker_swap_collapse (here) |
Abstract layer — any provability predicate satisfying the
Hilbert–Bernays–Löb derivability conditions plus diagonalization
(Foundation's Provability/HBL classes):
| theorem | statement |
|---|---|
instance_trust_free |
trust in a particular proved sentence is trivially provable — the permitted half of the asymmetry (proved with the Löb machinery explicitly omitted) |
selftrust_collapse |
the internalized soundness schema □σ → σ (for all σ) is inconsistency, via Löb at the single instance σ := ⊥ |
checker_swap_collapse |
the tiling step: internally believing a successor at-least-as-strong (□σ → Cσ) and trusting it in the abstract (Cσ → σ) is inconsistency — where C is an arbitrary formula family carrying no assumptions: the obstruction lives entirely in the predecessor's beliefs |
trust_forces_descent |
the "telomere" of Tiling Agents, as a theorem: a consistent system that schema-trusts a successor has a sentence for which it cannot prove its own strength carries over |
consistent_unreflective |
contrapositive in witness form: every consistent system fails some concrete reflection instance |
Arithmetic layer — the same statements (*_arith) where □ is the
standard arithmetized provability predicate of a real theory: any
Δ₁-axiomatized T with 𝗜𝚺₁ ⪯ T, via Foundation's
Theory.standardProvability, whose derivability conditions are proved
from arithmetized proof theory, not assumed.
All sorry-free; axioms exactly [propext, Classical.choice, Quot.sound]
(the Mathlib baseline), machine-pinned per theorem in Audit.lean. The
pins also guard against Foundation's two declared axioms for concrete
Δ₁-instances (its Examples.lean) ever entering the dependency cone —
this artifact stays parametric and does not import them.
- The collapse factors through σ := ⊥ — it is Gödel II in tiling clothes. That is the point being made precise (the "trust decision over an open-ended future" is already fatal at one sentence), not a new incompleteness result.
- No concrete theory (PA, IΣ₁ itself) is named: Foundation's concrete
Δ₁-definability instances are currently declared axioms upstream, so the
statements here quantify over
[T.Δ₁] [𝗜𝚺₁ ⪯ T]instead. - The bridge to lean-keep — that the gate tower's certificates contain no
provability predicate and so offer Löb nothing to grab — is an
observation about lean-keep's formalization (its
Soundis a statement about a Bool-valued filter), not a theorem of this artifact.
Built on Foundation
(FormalizedFormalLogic), pinned by commit in lakefile.lean (Foundation
has no release tags); Lean toolchain v4.29.0 to match. Foundation brings
Mathlib.
lake update # fetch pinned deps
lake exe cache get # Mathlib olean cache
lake build # builds the Foundation cone (~30 min first time) + this
References: Löb 1955; Yudkowsky & Herreshoff, Tiling Agents for
Self-Modifying AI, and the Löbian Obstacle (2013); lean-keep/LOEB.md
for the systems reading and the Feferman/Beklemishev context.