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