FORMALIZATION_COVERAGE.md
Model-Theory Normalization
FORMALIZATION_COVERAGE.md
1 # Formalization coverage — v0.10
2
3 PASS: 9 new local Lean modules, 105 theorem declarations (78 generic and 27 concrete
4 kernel examples), 50 definitions, 2 abbreviations, 1 structure and 1 inductive type:
5 159 explicit named declarations audited. Generated constructors/fields compile but
6 are not counted again as named research declarations. 17 expected-outcome tasks
7 passed: 9 cold builds, one full axiom audit, one positive control and six rejections.
8 Only `propext`, `Classical.choice`, and `Quot.sound` appear. No custom project axiom,
9 `sorryAx` or `Lean.ofReduceBool` is accepted. Library warnings are errors.
10
11 | Module | Exact checked scope |
12 |---|---|
13 | BinaryWords | Word semantics, padding, full-adder/subtractor truth tables, ripple operations and length/value theorems |
14 | BinaryMulDiv | Actual shift-and-add multiplication and restoring long division, positive-divisor invariants and cost recurrences |
15 | BinarySigned | Sign/magnitude arithmetic, zero detection, Euclidean adjustment and safe divisor rejection |
16 | BinaryEncoding | Integer/word boundary conversion correctness and semantic scalar adapters; conversion costs excluded |
17 | BinaryCosted | Actual metered evaluators, erasure theorems, exact counts, modular multiplication and quadratic width budgets |
18 | BinaryPricing | Explicit unsigned request interpreter, trace semantics and conditional length/width cost bound |
19 | BinarySignedCost | Metered sign handling, zero scans, signed addition/multiplication/division and their cost bounds |
20 | BinaryBackend | Signed subtraction, modular addition, final scalar semantics and budgets |
21 | BinaryExamples | 27 finite direct kernel computations, including negative division, padding, carry, borrow and widened modular products |
22
23 The current Lean modules import pinned Mathlib directly. The predecessor archive
24 is preserved but its historical local Lean library is NOT recompiled by this block.
25 The selected Python baseline payloads are exact original bytes; their 203 source
26 profiles are re-executed independently and under the new port.
27
28 ## Boundaries
29
30 No universal theorem lowers the full discovery loop into these binary routines.
31 The 203 complete bit-backed discovery executions are PYTHON tests, not 203
32 kernel-checked whole-loop instances. Their scalar algorithms have generic Lean
33 counterparts; their parser/port/transcription is not verified extraction.
34
35 The cost theorem concerns a declared gate/cell model. It excludes input conversion,
36 allocation/indexing/queue work, compiled runtime, proof checking and bit-machine
37 implementation overhead. Primitive arithmetic correctness and priced scalar
38 recurrences do not alone close that missing implementation refinement.
39
40 The conditional unsigned trace theorem requires an explicit trace and explicit
41 operand-width/length bounds. The signed primitive theorems are separate; no
42 unproved universal trace-composition premise is silently discharged.
43
44 Lean 4.34.0-rc2, commit 6a10ac8c22beadecabdbb0919c2b50214762f91d.
45 Mathlib aeb72f1e9981b6d35b426b16dca7759be3e7ba06. Existing upstream cache reused,
46 not rebuilt. Interpretation and implementation review are self-review.