# 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:

```bash
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

```bash
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.