Formalization coverage — Logical Resolution v0.2
PASS: 13 local library modules, 112 theorem declarations, 74 definitions, 2 abbreviations, 3 structures and 5 inductive syntaxes. All 196 explicit named declarations were axiom-audited. The five new modules add 39 theorems, 20 definitions, one abbreviation, one structure, and three inductive syntaxes. No claim of 39 historically new results.
All 23 expected-outcome tasks passed. Every library file was compiled with warnings-as-errors. Only Classical.choice, Quot.sound and propext occur. No additional project axiom, sorryAx, or Lean.ofReduceBool appears. Two positive controls pass; six false/placeholder controls reject. Accepted source hashes were unchanged. The eight inherited library files match their frozen original bytes.
Lean: Lean (version 4.34.0-rc2, x86_64-unknown-linux-gnu, commit 6a10ac8c22beadecabdbb0919c2b50214762f91d, Release)
Mathlib: aeb72f1e9981b6d35b426b16dca7759be3e7ba06. This is a cold LOCAL build using the pinned upstream
compiled cache, not a rebuild of Mathlib or the entire embedded history.
| New module | Checked content |
|---|---|
| RelationalSyntax | Exact old-language inclusion; binary state relations; surjective quantified transport; relation descent iff fiber invariance; actual behavioral quotient preservation |
| RelationalBackForth | Atomic relation-sensitive agreement, both witness directions, reflexivity/symmetry, finite-rank and all-rank soundness |
| StandardTranslation | Actual FirstOrder.Language/model, source-to-Mathlib syntax, arbitrary free/bound assignment correctness, old-language bridge, quantifier rank and IsQF correctness, standard transport |
| StandardContracts | Fully composed actual quotient and finite-rank back-and-forth theorems for standard Realize |
| QuantifierWitness | Three actual vertices and one edge; all parameter-free standard QF formulas agree on single-vertex assignments; a rank-one formula distinguishes; no QF replacement in the same model; old quotient cannot retain the relation |
Boundaries
The translation is a one-sorted relationalization on the state carrier, with primitive predicates interpreting observations in a fixed external value type. It is not a native many-sorted backend. The translated fragment excludes state equality even though the target syntax supports it. Generic preservation therefore does not assert full first-order elementarity. The three-vertex QF theorem is explicitly stronger within that particular parameter-free model and does include standard equality atoms.
Back-and-forth is a sufficient preservation condition, not a proved completeness or strategy-discovery theorem. Atomic tests allow arbitrary finite operation words. The Python executable and interpretation of prose are not kernel-verified. No compactness, saturation, QE algorithm, imaginaries theorem, performance advantage, independent referee result, or novelty verdict is claimed.