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