Edition README
Constructive Repair
README.md
1 # Constructive Repair in Realization Calculus — 1.0.0rc3
2
3 **Komorebi P. · Standalone release candidate · 19 October 2026**
4
5 An exact rational repair component with independently checkable certificates and Lean proofs. This candidate retains the frozen mathematics and Python algorithms, adds source-bound release checks, and packages the complete current sources and evidence without recursively embedding old release archives. Its release-tested configuration is Linux x86_64 with CPython 3.13.5. It is not a claim that all of Operation Komorebi is at version 1.0.
6
7 The component handles freely chosen rational augmentations, weighted candidate menus, and proof-carrying branch search. Its original equations, costs, admissibility rules, and coefficient ring remain fixed throughout certification.
8
9 ## Start with the standalone Python wheel
10
11 From this source archive, install the included wheel without network access or runtime dependencies:
12
13 ```bash
14 python -m pip install --no-index --no-deps dist/komorebi_constructive_repair-1.0.0rc3-py3-none-any.whl
15 komorebi-repair doctor
16 komorebi-repair solve examples/branch_corpus/Branch018_input.json --output /tmp/repair-example
17 komorebi-repair check examples/branch_corpus/Branch018_input.json /tmp/repair-example/certificate.json --output /tmp/repair-recheck
18 ```
19
20 Each output directory must be new. The commands preserve original inputs, certificates, traces, and final receipts. They do not publish anything. The Python wheel has no third-party runtime dependencies. The source archive, rather than the wheel alone, carries the Lean projects and monograph.
21
22 Python checking returns `PYTHON_CERTIFICATE_VALID`, **never** a kernel-checked status. The certificate's `kind` distinguishes an optimal repair from a scoped no-repair result. Malformed data, an invalid certificate, or exhausted work budgets return `UNRESOLVED`. A rejected certificate is not an impossibility theorem.
23
24 ## Public Python API
25
26 ```python
27 from komorebi_repair import ExactMatrix, menu_problem, solve, verify
28
29 D = ExactMatrix.of([[1], [0], [0]])
30 E = ExactMatrix.of([[0, 0], [1, 0], [1, 1]])
31 R = ExactMatrix.of([[0], [1], [0]])
32 original = menu_problem(D, E, R, costs=[1, 1])
33 result = solve(original)
34 assert result.status == "PYTHON_CERTIFICATE_VALID", result.error
35 assert result.certificate["cost"] == 2
36 assert verify(original, result.certificate).status == "PYTHON_CERTIFICATE_VALID"
37 assert result.kernel_checked is False
38 ```
39
40 `fractions.Fraction` supplies fractional entries. Floating-point matrix entries are rejected rather than approximated. For free minimum-dimensional repair use `free_problem(D, R)`. `load(path)` loads a strictly parsed problem. See `docs/PUBLIC_API.md` for the 1.0 candidate compatibility contract.
41
42 ## Obtain a Lean-checked result
43
44 Use the source archive and the existing complete, pinned Linux x86_64 offline kit:
45
46 ```bash
47 python scripts/certify_branch.py examples/branch_corpus/Branch018_input.json \
48 --kit /path/to/Komorebi_Portable_Lean_4.34.0-rc2 \
49 --output /tmp/repair-kernel
50 ```
51
52 Supply `--certificate /path/to/certificate.json` to check a previously generated branch certificate instead of rerunning search. `certify_one.py` handles free repair, and `certify_menu.py` handles the small exhaustive reference menus.
53
54 These commands compile the actual original input and witnesses, check theorem axioms, replay modules through Lean's own kernel, and compare the Lean-evaluated input with the external original. The compiler and large Mathlib cache are not duplicated in this release. A complete pinned kit is required; this is not a download/install script.
55
56 ## Mathematical scope
57
58 For free repair, the least added dimension equals the span dimension of the residual classes in the original cokernel. The rational implementation constructs explicit matrices and certifies that dimension using exact identities.
59
60 For a weighted finite menu, a returned repair is checked in the original target. A proof tree accounts for every potentially cheaper admissible alternative. Rejection concerns only the directions and admissibility rules in the supplied problem. Search and certificate size can still be exponential.
61
62 The 51 proof modules and 526 named theorem declarations from v0.5.0 are unchanged. This candidate does not increase the theorem count. The fresh formal receipt is `evidence/verification/current/verification.json`. Counts measure coverage, not novelty.
63
64 ## Read and reproduce
65
66 - `monograph/Constructive_Repair.pdf` and `.tex`: complete monograph with a consolidated current release contract.
67 - `docs/RELEASE_READINESS.md`: completed gates and remaining conditions before final 1.0.
68 - `docs/THREAT_MODEL.md`: exact trust boundary and resource assumptions.
69 - `evidence/rc3/acceptance_run/release_tests.log`: current API, parser, CLI and portability regressions.
70 - `evidence/rc3/acceptance_run/platform_acceptance/`: clean installed-wheel test receipt and logs.
71 - `docs/PLATFORM_SUPPORT.md`: explicit tested/untested configurations and local acceptance commands.
72 - `evidence/release_coordinate_audit.json`: new exact coordinate-invariance comparisons.
73 - `DEVELOPMENT_HISTORY.md`: retained failures, changes, and next restart point.
74
75 ```bash
76 PYTHONPATH=python python -m unittest discover -s tests -v
77 (cd python && python -m unittest test_certificates test_rational_menu test_branch_menu)
78 python scripts/verify_release.py --kit /path/to/PINNED_KIT --output /tmp/fresh-full-verification
79 python scripts/check_manifest.py
80 ```
81
82 A fresh full Lean verification must use a new output directory and may take several minutes. The optional `scripts/audit_release_api.py` needs SymPy; the production API and CLI do not.
83
84 ## Offline platform acceptance
85
86 ```bash
87 python scripts/platform_acceptance.py --output /tmp/komorebi-platform-check
88 ```
89
90 The output path must be new. The runner installs the bundled wheel into an isolated environment, exercises the installed API and command-line entry point, checks paths with spaces and Unicode, and records actual interpreter/platform details. It makes no network requests and does not label Python checks as Lean proofs. The same runner is provided for Windows/WSL evaluation, but neither platform was executed here.
91
92 The default text-encoding defect was reproduced with the POSIX C locale and Python UTF-8 mode disabled. Export now uses explicit UTF-8 for Lean source, documents and logs. That test is not a Windows simulation.
93
94 ## Check this exact release
95
96 ```bash
97 python scripts/release_gate.py
98 ```
99
100 The gate checks the extracted manifest, all historical proof snapshots, the current source against the formal-verification receipt, the wheel against the source and installed-acceptance receipt, and the PDF against its build receipt. It reports technical readiness separately from the outstanding license decision. A PASS is not a signature or an independent proof checker.
101
102 The package contains every active source, proof, example and retained log needed for its workflows. `provenance/` replaces nested predecessor ZIPs with 121 exact historical proof-source snapshots. See `docs/DISTRIBUTION.md` for what is retained and what is not recursively bundled. No historical whole-archive replay is implied.
103
104 ## What “release candidate” means
105
106 The mathematical and wire protocols are frozen for this component. The final public 1.0 tag still requires the author's explicit code and document licensing choices. Technical support is now defined by `docs/PLATFORM_SUPPORT.md`; untested Windows/WSL and interpreter combinations are not advertised as validated. No license grant has been invented. Do not describe the package as having a particular open-source license until that choice is made.
107
108 Direct integration into the main Komorebi Python library and the authoritative Paper III source tree remains a separate adapter task. That does not require changing the foundations or resolving Conjecture 66. No unrestricted integral, nonlinear, or native arithmetic repair is claimed.