v0.3_README.md
Representation Calculus
v0.3_README.md
1 # Komorebi Representation Calculus v0.3
2
3 A symbolic certificate-to-Lean bridge for exact observable representations.
4
5 This release continues Representation Calculus v0.2, not p-adic Block 16. The
6 complete predecessor is preserved byte-for-byte under `history/`.
7
8 ## Main result
9
10 The generic matrix adapter proves that finite certificate equations imply
11 all-state, all-word behavior preservation and an exact observational quotient.
12 It constructs the actual encoded image, verifies its principal-multiple
13 coordinates, and injects that image into every competing sufficient state space.
14 All 202 frozen v0.2 certificates now have kernel-checked generated matrix proofs.
15 There is no source-state enumeration in this new exporter.
16
17 The synthetic eight-coordinate system modulo 65536 has a separate symbolic
18 bijection between its actual image and `Fin (2^30)`. Lean proves an exact
19 minimum of two residue coordinates for this example, even against arbitrary
20 nonlinear zero/one-coordinate encodings with the same all-word specification.
21
22 ## Read first
23
24 - `FORMAL_NOTE.md`: precise statements, proofs and semantic contracts.
25 - `FORMALIZATION_COVERAGE.md`: generic, generated, specialized and unfinished scopes.
26 - `RESULTS.md`: completed executions, counts and limits.
27 - `DEVELOPMENT_FAILURES.md`: failed attempts and evidence corrections.
28 - `CONTINUE_HERE.md`: the next missing theorem, without conflating it with completed work.
29
30 ## Reproduce
31
32 Python 3.11 or newer is sufficient. The reference scripts use only the standard
33 library. Lean is pinned by `lean-toolchain` to 4.34.0-rc2; only Lean/Std is needed.
34 No Mathlib source or cache is needed. Runtime binaries are not included.
35
36 Run integrity before audits, because audits replace current execution records:
37
38 ```bash
39 python tools/verify_integrity.py
40 python tools/validate_manifest.py LEAN_MANIFEST.json --root .
41 python tools/validate_manifest.py COMPUTATION_MANIFEST.json --root .
42 python tools/run_python.py
43 python tools/verify_lean.py --lean /absolute/path/to/lean
44 python tools/normalize_lean_manifest.py
45 python tools/validate_manifest.py LEAN_MANIFEST.json --root .
46 python tools/validate_manifest.py COMPUTATION_MANIFEST.json --root .
47 ```
48
49 In an environment with short per-call runtime limits, replace the Lean command by
50 an initial `--batch-size 20` call and subsequent identical calls with `--resume`.
51 Resume checks the complete accepted input-hash set and exact toolchain version.
52 Do not modify accepted sources between batches. A batch returning `IN_PROGRESS`
53 is not a completed audit. Completion also requires the axiom audit and controls.
54
55 `normalize_lean_manifest.py` corrects one metadata classification: the auditor's
56 JSON progress log is a log, not a declared scientific result. The raw manifest
57 and exact one-field correction are retained. This does not alter proof inputs,
58 compiler outcomes, or any output hash.
59
60 ## Export another matrix certificate
61
62 ```bash
63 python tools/export_symbolic_lean.py --help
64 ```
65
66 The exporter checks a certificate against a separately supplied expected source.
67 It emits literal matrices, shared observation-row proofs, and calls to the generic
68 adapter. Every initial state is admissible. The single-seed interface is rejected.
69 The original finite-state table exporter remains available, but is not used for
70 the 202 symbolic exports.
71
72 ## Boundaries
73
74 No Python discoverer, parser, Smith routine or exporter is a verified program.
75 Lean proves the theorem of the matrices actually present in each generated file;
76 independent literal-data extraction audits agreement with expected source JSON.
77 The universal numerical minimum free-coordinate count for arbitrary matrix
78 certificates remains a written chain-ring argument. The large fixture's exact
79 two-coordinate minimum is formally proved separately. No learned AI policy,
80 held-out structural discovery, speedup comparison, p-adic corpus update, external
81 refereeing or historical-priority conclusion is claimed.