Edition README
Logical Resolution
README.md
1 # Komorebi Logical Resolution v0.2
2
3 **Standard first-order translation, relational quotient contracts, and quantifier-sensitive resolution.**
4
5 This is a continuation of Logical Resolution v0.1, not a new p-adic block or a
6 replacement for Representation Calculus v0.4. The frozen v0.1 ZIP is in `history/`.
7 Its eight current Lean modules are reused byte-for-byte and rebuilt. Five new
8 modules complete the standard-syntax bridge and add a relational layer.
9
10 Start with `THEOREM_NOTE.md`, then `FORMALIZATION_COVERAGE.md` and `RESULTS.md`.
11 The accepted universal claims are the actual Lean declarations. Python examples
12 and finite counts are separate implementation audits. No novelty or independent
13 referee verdict is asserted.
14
15 ## Reproduce
16
17 Python 3.11+ and the standard library suffice for the finite audit:
18
19 ```sh
20 python tools/verify_integrity.py
21 python tools/audit_python.py
22 ```
23
24 Distribution integrity must be checked BEFORE rerunning audits, which intentionally
25 replace current execution records. Prefer an extracted working copy.
26
27 For the complete strict Lean audit, provide the preserved runtime root containing
28 `toolchain/bin/lean` and `workspace/.lake/packages/mathlib` at the pins below:
29
30 ```sh
31 python tools/run_checked.py --runtime /path/to/Komorebi_Portable_Lean_4.34.0-rc2
32 python tools/validate_manifest.py LEAN_MANIFEST.json --root .
33 python tools/validate_manifest.py PYTHON_MANIFEST.json --root .
34 ```
35
36 The wrapper cold-builds all 13 local modules, checks every named declaration's
37 axioms, and executes positive and expected-negative controls. It uses cached
38 pinned Mathlib dependencies, NOT a cold build of Mathlib. The multi-gigabyte
39 runtime/cache is deliberately not bundled.
40
41 Lean: `leanprover/lean4:v4.34.0-rc2`, commit
42 `6a10ac8c22beadecabdbb0919c2b50214762f91d`.
43 Mathlib: `aeb72f1e9981b6d35b426b16dca7759be3e7ba06`.
44 Source hashes and attribution: `source_records/MATHLIB_INPUT.json` and
45 `EXTERNAL_INPUTS.md`.
46
47 ## Main results
48
49 * Constructive translation to actual Mathlib `FirstOrder.Language` formulas,
50 with satisfaction and quantifier-rank preservation at every arity/nesting.
51 * A binary relation descends through an encoding iff it is constant on both fibers.
52 Surjective operation/observation transports preserving AND reflecting the added
53 relations preserve every translated formula, including nested quantifiers.
54 * Finite-rank two-sided witness matching implies truth agreement up to that rank.
55 * A three-vertex example agrees on all parameter-free one-variable standard
56 quantifier-free formulas but is separated by `exists y, R(x,y)`. This query has
57 no parameter-free quantifier-free replacement even within that one model.
58
59 The translated source fragment excludes state equality. The target library has
60 state equality, but our preservation theorem does not cover arbitrary formulas
61 using it. The special three-vertex quantifier-free counterexample DOES quantify
62 over all standard quantifier-free formulas, including state equality.
63
64 See `CONTINUE_HERE.md` for the next bounded target and exact remaining limitations.