README.md
Constructive Repair
README.md
1 # Komorebi Constructive Repair Audit — v0.1.0
2
3 This is a **standalone experimental test harness** for a proposed constructive-repair refinement of Realization Calculus (particularly Paper III), with arithmetic and representation-theoretic regression examples from Paper IX and Paper XI.
4
5 It is **not** a new foundation, not a modification of the existing Komorebi Python library, and not a Lean-verified release.
6
7 ## Run
8
9 Python 3.10+; main experiment requires **no third-party packages**.
10
11 ```bash
12 python run_audit.py
13 python -m unittest -v test_repair_core
14 ```
15
16 The first command writes:
17
18 - `audit_trace.txt` — 258+ lines of exact intermediate calculations and negative controls
19 - `case_records.jsonl` — one machine-readable record for each of 3,307 individual cases
20 - `audit_summary.json` — assertion counts, category counts, known limitations
21
22 Optional independent cross-check with SymPy 1.14:
23
24 ```bash
25 python -m pip install sympy==1.14.0
26 python crosscheck_sympy.py
27 ```
28
29 Then run `sha256sum -c SHA256SUMS.txt` to check the packaged evidence (do this before rerunning the scripts, as reruns rewrite outputs).
30
31 ## Read first
32
33 1. `TECHNICAL_AUDIT.md`: detailed theorems, ordinary proofs, scope analysis, test results, all significant negative controls.
34 2. `audit_trace.txt`: short exact computation log and human-readable intermediate values.
35 3. `case_records.jsonl`: complete deterministic per-case evidence for reproducing or auditing the sampled computations.
36 4. `DEVELOPMENT_HISTORY.md`: stages and changes from initial to strengthened audit.
37 5. `FORMALIZATION_TARGETS.md`: suggested Lean contracts and what has **not** been compiled.
38
39 ## Main status
40
41 - Restricted free-linear augmentation theorem: ordinary proof, tested.
42 - Finite admissible-menu optimization: exhaustively certified within input menu, tested by independent coefficient enumeration.
43 - Invariant preservation, information-losing transport, nonlinear obstructions: negative controls passed.
44 - Genuine Euler and cyclotomic trace regression tests: exact arithmetic passed in tested ranges.
45 - Global arithmetic representation / universal repair synthesis: **not proven**.
46 - Lean kernel compilation: **not attempted; toolchain absent**.
47
48 ## File roles
49
50 `repair_core.py` is the finite exact-arithmetic solver, `run_audit.py` orchestrates primary experiments, `extra_audit.py` runs additional domain-linked tests, `test_repair_core.py` provides 20 regression unit tests, and `crosscheck_sympy.py` independently verifies ranks and coefficients using SymPy.
51
52 No floats, optimization heuristics masquerading as proofs, or unsupported existence claims are used in the exact solver.