Edition README
Representation Calculus
README.md
1 # Komorebi Representation Calculus v0.4
2
3 Torsion-safe optimality for certificate-derived representations over Z/(p^r).
4 This is the representation-calculus branch, not p-adic Block 16.
5
6 ## Read first
7
8 - `FORMAL_NOTE.md`: exact contract, proof and nonlinear-encoding boundary.
9 - `FORMALIZATION_COVERAGE.md`: universal and instance-level proof scope.
10 - `RESULTS.md`: retained completed execution results, not intended targets.
11 - `DEVELOPMENT_FAILURES.md`: failed drafts, interrupted runs and their replacements.
12 - `EXTERNAL_INPUTS.md`: pinned upstream and reused project proofs.
13
14 A certified encoding with t nonzero principal-ideal factors needs exactly t
15 residue coordinates when the initial encoding is linear and every initial state
16 and future word must be handled. The lower bound even permits nonlinear target
17 operations/observations. A checked example shows that permitting a nonlinear
18 initial encoding changes the answer. This is not an arbitrary-program memory bound.
19
20 ## Source layout
21
22 `formalization/MatrixLinearBridge.lean`, `FinRingCompatibility.lean`, and
23 `MatrixPrimeMinimality.lean` prove the generic adapter. `MinimumBatch*.lean`
24 instantiates it on all 202 frozen matrix certificates. `CertifiedMinima.lean`
25 imports the batches. `TorsionEncodingBoundary.lean` proves the exact hypothesis
26 boundary. `LargeLinearMinimum.lean` reuses the general bound for the previous large
27 example. `examples/FreshMinimum.lean` is a fresh end-to-end exporter example.
28
29 The original v0.3 ZIP is preserved under `history/`. Its 213 Lean files have only
30 module/public-import header changes in the current tree; mathematical bodies and
31 literal data are unchanged. Three generator-bound modules from p-adic Block 15
32 are copied unchanged under `formalization/KomorebiPadic/` and rebuilt here. This
33 is not a new verification of the entire p-adic project.
34
35 ## Reproduction
36
37 Check the distribution before any audit, because rerunning an audit intentionally
38 replaces current execution records:
39
40 ```sh
41 python tools/verify_integrity.py
42 python tools/validate_manifest.py COMPUTATION_MANIFEST.json --root .
43 python tools/validate_manifest.py LEAN_MANIFEST.json --root .
44 python tools/run_python.py
45 ```
46
47 The Python code uses the standard library. It rediscovers and checks the frozen
48 certificates, verifies emitted source contents, and exhausts the small torsion
49 boundary example. Python/exporter/checker correctness is not proved in Lean.
50
51 For Lean, use the saved portable runtime or an equivalent installation with:
52
53 - Lean 4.34.0-rc2, commit `6a10ac8c22beadecabdbb0919c2b50214762f91d`;
54 - Mathlib commit `aeb72f1e9981b6d35b426b16dca7759be3e7ba06` and its dependencies.
55
56 The audit expects `<runtime>/toolchain/bin/lean` and the matching dependencies
57 under `<runtime>/workspace/.lake/packages/`. Runtime/cache bytes are not bundled.
58 Run from this directory, with a new empty build directory outside the release:
59
60 ```sh
61 python tools/audit_lean.py --runtime /path/to/portable-runtime --build /tmp/repr04-cold --batch 25 --timeout 120
62 python tools/audit_lean.py --runtime /path/to/portable-runtime --build /tmp/repr04-cold --batch 25 --timeout 120 --resume
63 ```
64
65 Repeat the resume command until the result says PASS. An IN_PROGRESS record or a
66 timeout is not verification. Resumption refuses changed accepted source hashes.
67 Use `--batch 1000` for one enclosing invocation. The runner cold-builds local
68 modules and reuses the pinned upstream compiled cache; it does not rebuild Mathlib.
69
70 The inherited v0.3 scripts `verify_lean.py`, `replay_selected_lean.py`, and
71 `normalize_lean_manifest.py` are historical tools, NOT the v0.4 audit entry point.
72
73 ## Export a newly discovered certificate
74
75 ```sh
76 python tools/export_minimum_lean.py source.json certificate.json --namespace MyCase --output MyCase.lean
77 ```
78
79 The exporter runs the unchanged independent checker and writes untrusted Lean
80 source. Compile that source against the current compiled modules to accept its
81 all-state/all-word optimum. A successful export message is not a successful proof.
82
83 ## Trust boundaries
84
85 The formal theorem concerns literal matrices under a declared all-state contract.
86 The JSON parser, proposer/discoverer, Smith engine and exporter are not verified
87 executables. No trained search policy, independently held-out scientific discovery,
88 comparative speedup, independent referee review or historical-novelty claim is made.