Edition README
AddMul Arithmetic Reconstruction
README.md
1 # Komorebi Additive/Multiplicative Arithmetic Observation — Block 03
2
3 Continuation of the preceding two additive–multiplicative reconstruction research blocks.
4
5 ## Contents
6
7 - `RESEARCH_NOTE.md`: theorem statements, self-contained mathematical proofs, exact claim boundaries, restart instructions.
8 - `proofs/FiniteObservation.lean`: algebraic three-sample filter, sharp lower bound and exact witness.
9 - `proofs/FilterBudget.lean`: generic finite annihilator L∞ error theorem over arbitrary lengths.
10 - `proofs/WittCarryExample.lean`: complete finite `F_3 → Z/9` Teichmüller carry example and nonsplitting proof.
11 - `proofs/Block03Negative.lean`: intentionally false statement to test compiler rejection.
12 - `tests/test_block03.py`: exact modular repetitions, sharp minimax, polyphase interpolation, Witt lift and carry-cocycle tests.
13 - `tests/test_recurrence_grammar.py`: general finite recurrence annihilator and escape-mode negative control.
14 - `tests/plot_block03.py`: deterministic mathematical figures.
15 - `evidence/`: machine-readable results, stdout logs, compiler audit and manifest.
16 - `figures/`: two explanatory mathematical graphics.
17
18 ## Run exact tests
19
20 ```bash
21 python3 tests/test_block03.py
22 python3 tests/test_recurrence_grammar.py
23 python3 tests/plot_block03.py
24 ```
25
26 ## Reproduce Lean checks
27
28 Use the separately supplied, pinned **Komorebi Portable Lean 4.34.0-rc2** kit and its `run.sh` entrypoint:
29
30 ```bash
31 bash /path/to/Komorebi_Portable_Lean_4.34.0-rc2/run.sh check proofs/FiniteObservation.lean
32 bash /path/to/Komorebi_Portable_Lean_4.34.0-rc2/run.sh check proofs/FilterBudget.lean
33 bash /path/to/Komorebi_Portable_Lean_4.34.0-rc2/run.sh check proofs/WittCarryExample.lean
34 ```
35
36 The intentionally false file must **fail** compilation. The archive includes exact `#print axioms` audit outputs; no `sorry`, `admit`, or added axioms are used in the positive Lean source.
37
38 ## Scope
39
40 This package **does not** contain or prove a global abc height estimate, IUT reconstruction, or a new global arithmetic height mechanism. It distinguishes finite conditional statements and fully checked examples from broader open research goals.