README.md
Komorebi Space
README.md
1 # Exact computational examples
2
3 These four programs accompany the monograph's examples of protected repair, regularization, approximation, and certificates. They use Python's standard library and exact rational arithmetic. Run the commands from the package root, keeping the files together in `examples/`.
4
5 | Program | Purpose | Command |
6 | --- | --- | --- |
7 | `protected_repair.py` | Solve a finite protected linear system or return an obstruction | `python3 examples/protected_repair.py --demo` |
8 | `budgeted_repair.py` | Compute a protected regularized correction and its budget certificate | `python3 examples/budgeted_repair.py` |
9 | `approximation_models.py` | Evaluate finite trajectory formulas, diagonal data, tail bounds, and a phase table | `python3 examples/approximation_models.py --depth 16 --steps 10` |
10 | `inexact_repair_certificate.py` | Certify a proposed correction without computing the optimizer | `python3 examples/inexact_repair_certificate.py` |
11
12 Each command writes JSON to standard output. Add `> result.json` to save a result. The supplied demonstration JSON files are reference outputs. The commands above generate fresh records.
13
14 Start with [WORKED_EXAMPLE.md](WORKED_EXAMPLE.md) for one complete route from a declared rational problem to a generated and verified certificate, its exact expected values, and the corresponding monograph and Lean statements.
15
16 ## Protected linear repair
17
18 The program solves
19
20 $$
21 Ay=0,\qquad Py=Px
22 $$
23
24 over the rational numbers. Here `A` describes the equations to satisfy, `P` describes the information to preserve, and `x` is the original candidate.
25
26 The demonstration covers a unique answer, a one-dimensional affine family, and an obstructed problem. For a custom problem, save an object such as the following as `problem.json`:
27
28 ```json
29 {"A": [[1, -1, 0]], "P": [[1, 0, 0], [0, 0, 1]], "x": [2, 0, 5]}
30 ```
31
32 Then run:
33
34 ```sh
35 python3 examples/protected_repair.py problem.json
36 ```
37
38 A feasible result contains a particular answer and a basis for all invisible exact changes, `ker A ∩ ker P`. The chosen particular answer is obtained by elimination and need not minimize a norm. An obstructed result contains row vectors satisfying
39
40 $$
41 \lambda A=\mu P,\qquad \lambda Ax=1.
42 $$
43
44 These equations exclude a protected exact answer. The command checks each returned certificate before succeeding. An obstructed input is a successfully classified mathematical problem and exits with code 0. Invalid input exits with code 2.
45
46 Matrix entries must be integers or exact rational strings such as `"1/2"`. Floats and Boolean values are rejected. Matrix row lengths must match the candidate dimension. Empty row families and zero-dimensional candidates are supported. The coefficient field is rational: a system that has a rational solution may have no integer solution.
47
48 ## Protected quadratic regularization
49
50 For fixed matrices `d` and `p`, datum `r`, and positive parameter `alpha`, the regularized solver minimizes
51
52 $$
53 \|da-r\|^2+\alpha\|a\|^2\quad\text{over }a\in\ker p.
54 $$
55
56 The candidate is `f - a`, so the protected value `p f` is preserved. By default the datum is `r = d f`. The optional `measured_residual` field supplies a different datum for the fitting objective. The output reports both that fit residual and the candidate's actual residual under the supplied model.
57
58 Use the included problem file:
59
60 ```sh
61 python3 examples/budgeted_repair.py --input examples/budgeted_problem.json
62 ```
63
64 Custom inputs have keys `d`, `p`, `f`, and `alpha`, with optional `measured_residual`. The candidate dimension and number of residual coordinates must be positive. A zero-dimensional protected kernel is supported. Entries use the same integer or rational-string format as the linear solver.
65
66 The program constructs a basis of the full protected kernel and retains its Gram matrix. It returns the unique regularized correction, exact preservation and normal-equation checks, objective value, and squared norms. Its budget certificate describes optimality at the norm of the returned correction. A unit dual witness is represented by its rational numerator and squared normalization factor, avoiding rounded square roots.
67
68 The default demonstration includes a protected coordinate, a nonorthogonal kernel basis, a fully protected candidate, a dual witness, and a diagonal tail enclosure.
69
70 ## Approximation models
71
72 ```sh
73 python3 examples/approximation_models.py --depth 16 --steps 10
74 ```
75
76 The output contains a polynomial-decay trajectory, a trajectory with alternating growth and decay, a diagonal finite-prefix model, and a two-bit phase table. `--depth` and `--steps` each accept integers from 1 through 4096 and default to 8.
77
78 The tail intervals evaluate analytic bounds proved in the monograph. Their finite evaluation does not establish an infinite convergence or nonexistence theorem by itself. The program evaluates these specific formulas and does not implement a general reconstruction method.
79
80 ## Inexact correction certificates
81
82 The certificate program evaluates a proposed correction using the actual protected kernel and its inherited Euclidean metric. It provides exact primal and dual values, a normal-residual certificate, and squared bounds on the distance to the regularized optimizer.
83
84 See [WORKED_EXAMPLE.md](WORKED_EXAMPLE.md) for the complete reader walkthrough and [INEXACT_CERTIFICATES.md](INEXACT_CERTIFICATES.md) for the full input contract and additional examples.
85
86 ## Interpretation
87
88 These are finite exact computations tied to declared mathematical inputs. The monograph supplies the relevant general proofs, and the accompanying Lean source formalizes its stated scope. The Python programs are not certified extractions from Lean. Their executions do not establish universal implementation correctness, floating-point accuracy, or an efficiency bound for large problems.
89
90 The publication's citation is in [CITATION.bib](../CITATION.bib), and its current reuse status is in [REUSE.md](../REUSE.md).