Logical Resolution

Download original file

Read the formatted document

1 # Exact formalization coverage — Logical Resolution v0.1
2 
3 ## Completed execution
4 
5 PASS: eight library modules, 73 named theorem declarations, 54 definitions, one
6 abbreviation, two structures, and two inductive syntaxes. All 132 explicit named
7 declarations are axiom-audited. Six new modules contribute 50 theorem declarations,
8 37 definitions, and two inductive syntaxes. These counts include routine lemmas,
9 not 50 claims of historical novelty.
10 
11 Only `propext`, `Classical.choice`, and `Quot.sound` occur. No custom project axiom,
12 `sorryAx`, or `Lean.ofReduceBool` occurs in accepted dependencies. All library files
13 pass warnings-as-errors. A positive control accepts; two false-claim controls and
14 a placeholder control reject. All accepted input hashes are unchanged.
15 
16 Toolchain: Lean 4.34.0-rc2, commit
17 `6a10ac8c22beadecabdbb0919c2b50214762f91d`, with matching Std. No Mathlib import is used.
18 
19 | Module | Exact checked scope |
20 |---|---|
21 | RepresentationCore (inherited unchanged) | Unary deterministic system, all-word equivalence, exact transport and actual quotient |
22 | FiniteCertificates (inherited unchanged) | Finite horizons, distinguishing words, sufficient tests and finite local transport checks |
23 | ObservationSyntax | Well-scoped value terms and formulas, binder semantics, exact quantified preservation under SURJECTIVE transport, actual quotient preservation |
24 | LogicalHorizon | Full behavior iff observational qf-type agreement iff observational formula agreement; finite word-depth characterization at every quantifier rank; distinguishing atomic formulas |
25 | SemanticBoundaries | Actual state-equality/cardinality counterexamples, failure of nonsurjective quantified preservation, qf preservation without surjectivity, no uniform QE across a two-model example |
26 | StreamBoundary | Actual infinite stream dynamics; behavior equals stream identity; no uniform finite horizon; no single finite observational formula defines full behavior |
27 | FiniteDefinability | Pair-atom schema, finite code equality formula, exact depth/rank, certified all-word definability under the local closure contract |
28 | ConcreteLogical | Explicit 8-state/4-state example, verified quotient, all-formula transport, finite formula defining complete behavior |
29 
30 ## Crucial boundaries
31 
32 The language has STATE quantifiers and VALUE equality, not state equality. Its
33 fixed value sort includes literals for all values. These restrictions are part
34 of every scope claim. The depth/rank collapse is within a fixed structure and
35 this fragment, not uniform quantifier elimination or a theorem about full logical
36 types. The stream nondefinability theorem excludes this fragment only.
37 
38 The custom syntax has not been embedded into Mathlib's standard first-order
39 syntax. No compactness, elimination of imaginaries, saturation, ultraproduct,
40 forcing, arbitrary relational-profile, or historical novelty theorem is claimed.
41 Python evaluation and discovery, the parser interface, and the textual exposition
42 are not kernel-verified programs. Semantic proof audit is self-review.
43 
44 Only TWO semantic predecessor modules were reused and rebuilt. The frozen parent
45 archive is included for provenance, not claimed to have been entirely rechecked.

Back to source controls