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