Constructive Repair

Komorebi Constructive Repair Audit — v0.1.0

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.

It is not a new foundation, not a modification of the existing Komorebi Python library, and not a Lean-verified release.

Run

Python 3.10+; main experiment requires no third-party packages.

python run_audit.py
python -m unittest -v test_repair_core

The first command writes:

• audit_trace.txt — 258+ lines of exact intermediate calculations and negative controls
• case_records.jsonl — one machine-readable record for each of 3,307 individual cases
• audit_summary.json — assertion counts, category counts, known limitations

Optional independent cross-check with SymPy 1.14:

python -m pip install sympy==1.14.0
python crosscheck_sympy.py

Then run sha256sum -c SHA256SUMS.txt to check the packaged evidence (do this before rerunning the scripts, as reruns rewrite outputs).

Read first

1. TECHNICAL_AUDIT.md: detailed theorems, ordinary proofs, scope analysis, test results, all significant negative controls.
2. audit_trace.txt: short exact computation log and human-readable intermediate values.
3. case_records.jsonl: complete deterministic per-case evidence for reproducing or auditing the sampled computations.
4. DEVELOPMENT_HISTORY.md: stages and changes from initial to strengthened audit.
5. FORMALIZATION_TARGETS.md: suggested Lean contracts and what has not been compiled.

Main status

• Restricted free-linear augmentation theorem: ordinary proof, tested.
• Finite admissible-menu optimization: exhaustively certified within input menu, tested by independent coefficient enumeration.
• Invariant preservation, information-losing transport, nonlinear obstructions: negative controls passed.
• Genuine Euler and cyclotomic trace regression tests: exact arithmetic passed in tested ranges.
• Global arithmetic representation / universal repair synthesis: not proven.
• Lean kernel compilation: not attempted; toolchain absent.

File roles

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.

No floats, optimization heuristics masquerading as proofs, or unsupported existence claims are used in the exact solver.