Komorebi Model-Theory Normalization v0.10
Verified scalar binary backend; end-to-end discovery bit-cost lowering remains open.
Start with NORMALIZED_CORE.md and FORMALIZATION_COVERAGE.md. The new implementation contains ripple addition/subtraction, shift-and-add multiplication, restoring positive-divisor division, signed Euclidean adjustment and modular reduction. Its actual evaluators have proved operand-length-dependent gate/cell counters.
Nine Lean modules and 27 concrete examples pass a fresh cold build. The independent Python port reproduces all 203 predecessor discovery outputs and their canonical bases, while retaining 295,173 original arithmetic events. Those complete port runs are finite tests, not a universal Lean lowering theorem.
Reproduce
First verify distribution bytes:
python tools/verify_integrity.py
python tools/validate_manifest.py LEAN_MANIFEST.json --root .
python tools/validate_manifest.py PYTHON_MANIFEST.json --root .
Then use a fresh working directory and the exact pinned runtime root:
python checks/run_audit.py lean-init --runtime /path/to/Komorebi_Portable_Lean_4.34.0-rc2 --work /tmp/komorebi-bits-check
python checks/run_audit.py lean-step --work /tmp/komorebi-bits-check --limit 5
Repeat lean-step until all 17 tasks complete. It refuses changed inputs and writes PASS only after every planned expected outcome succeeds. The upstream Mathlib cache is reused, not rebuilt. Runtime/cache files are not bundled.
python checks/run_audit.py python
The last commands intentionally rewrite current execution records. Run integrity checks BEFORE them in a fresh copy. The Python audit requires only the Python standard library and the included unchanged baseline modules.
The predecessor ZIP is preserved verbatim under history/. Selected baseline data are duplicated only to make the current audit self-contained. No fonts are bundled.