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