RESULTS.md
Model-Theory Normalization
RESULTS.md
1 # Retained results — v0.10
2
3 ## Cold Lean audit
4
5 PASS: nine modules; 159 named declarations; 105 theorems (78 generic, 27 examples).
6 17 expected-outcome tasks completed. Sum of subprocess runtimes: 52.769184 seconds.
7 This is an execution receipt, not a comparative performance claim. All pinned
8 accepted source hashes were unchanged. The positive control accepted and six
9 invalid controls were rejected for their claims. Only standard axioms occurred.
10
11 ## Independent Python audit
12
13 PASS: 119,732 individual checks; 203 full discovery fixtures.
14 All values use exact integer/Boolean arithmetic. Random wide cases use seed
15 2026092110. Native integer arithmetic supplies independent scalar reference results.
16
17 | Check | Count |
18 |---|---:|
19 | `unsigned_add` | 8,192 |
20 | `adder_cost_length` | 8,192 |
21 | `subtractor_borrow_identity` | 8,192 |
22 | `subtractor_cost_length` | 8,192 |
23 | `unsigned_multiply` | 4,096 |
24 | `multiply_quadratic_budget` | 4,096 |
25 | `unsigned_divmod` | 7,936 |
26 | `division_quadratic_budget` | 7,936 |
27 | `signed_add` | 4,225 |
28 | `signed_add_budget` | 4,225 |
29 | `signed_multiply_budget` | 4,225 |
30 | `signed_subtract_budget` | 4,225 |
31 | `signed_subtract` | 4,225 |
32 | `signed_multiply` | 4,225 |
33 | `signed_euclidean_divmod` | 8,224 |
34 | `signed_division_budget` | 8,224 |
35 | `residue_multiply` | 4,900 |
36 | `residue_wide_product_budget` | 4,900 |
37 | `residue_add` | 4,900 |
38 | `residue_add_budget` | 4,900 |
39 | `wide_padded_multiply` | 160 |
40 | `wide_padded_divide` | 160 |
41 | `wide_signed_divide` | 160 |
42 | `zero_divisor_rejected` | 3 |
43 | `malformed_word_rejected` | 4 |
44 | `frozen_parent_result_count` | 203 |
45 | `bit_backend_discovery_answer` | 203 |
46 | `bit_backend_canonical_basis` | 203 |
47 | `same_arithmetic_opcode_counts` | 203 |
48 | `same_arithmetic_total` | 203 |
49
50 The declared exhaustive bounds are: unsigned pairs 0..63, unsigned division
51 dividends 0..255 and divisors 1..31, signed pairs -32..32, signed division
52 dividends -128..128 and divisors 1..32, every residue pair at moduli 1..24.
53 There are 160 separately seeded padded wide cases with widths drawn from
54 16,32,64,128,256. Finite tests do not replace generic Lean proofs.
55
56 ## Full discovery port results
57
58 All 203 ordered outputs and canonical bases equal the frozen originals. Every
59 per-opcode arithmetic-event count matches, totaling 295,173 events. The new
60 declared gate/cell total is 270,165,476. The maximum input magnitude width is
61 42 bits; padded output storage reaches 100 bits. These are different quantities.
62
63 | Fixture | Scalar events | Gate/cell units | Maximum operand width |
64 |---|---:|---:|---:|
65 | scrambled_128bit.source | 2,465 | 14,028,031 | 42 |
66 | descending_torsion.source | 696 | 1,045,360 | 25 |
67
68 The port deliberately re-encodes and decodes at scalar boundaries; conversion
69 volume is recorded but its cost is not included. Extraction/Option interface
70 charges are declared port conventions, not a whole-program Lean cost theorem.
71 The 203 examples are inherited synthetic regressions, not new held-out discoveries.
72
73 ## Lineage and replay
74
75 The frozen parent archive SHA and all 1,395 listed payload hashes were verified.
76 All 207 selected baseline payloads agree byte-for-byte with the parent. The
77 recursive ZIP font scan found no font files. No parent Lean or full Mathlib rebuild
78 is claimed. Final distribution and fresh-extraction results are in the separate
79 EXTRACTED_REPLAY.json and packaging report, rather than inferred from this note.