feat(model): the model's facts over its parameter values (MN-07)

[afflom]

Item M4 of the completion plan #3, the part decided over parameter values; refs #6. Stacked on #17; retarget to main when #17 merges.

What Mnist.Facts proves. Each fact is computed from the content-addressed parameter artifacts and proved by decide; 23 theorems in all:

Fact	Value
Requantization multipliers of conv1, conv2 and fc (34)	all positive
fc multipliers (10)	pairwise distinct
conv1: least bias + 255·(negative taps), greatest bias + 255·(positive taps)	−205015, 210788
conv2: the same	−1477999, 878711
Stored-order tap pairs per channel (a zero added to an odd count) that can saturate an int16 sum of u8×s8 products	conv1 28 of 104, conv2 113 of 1600
Pairing each channel's smallest tap with its largest	no pair can saturate (conv1 whole; conv2 one theorem per channel)

Not proved here, and said so (README, #6):

• that these bounds hold for every input;
• that positive multipliers make requantization monotone;
• that the 3×3 pool never reads conv2's last two rows and columns.

Those are statements over all inputs, and they need UOR-Foundation/LexLean#117. Its probe found Int order propositions, the runtime's comparison/negation/quotient in the linear_arithmetic lowering, and a split on if missing. The eighth fact (a positive dequantization scale) needs the ONNX file, #15.

Consequences in the repository.

• Facts is an entrypoint, so the bundle's source identity covers it. MN-01 now counts twelve modules.
• The request pins the new identities, and the bundle was rebuilt with lexlean production build at the pinned 54f2ec41 and Lean 4.32.1 (result 8370f724). The package's crate is byte-identical: the module is outside the root's closure.

R3.

• Register row, scenario and test come first (c2661d7), then the module, the bundle and the docs.
• conformance_mn_07 verifies the module and reads all 23 theorems from the attestation as checked within their axiom policies.
• Planting a wrong value (210789 for 210788) makes Lean reject the module and the test fail; recorded in docs/evidence/planted-defects.md.

Checked locally with Rust 1.97.0 (1.97.1 is not downloadable in this session):

• lexlean production verify-artifact dist: bindings verified.
• xtask check-model, cargo fmt --check and cargo clippy --workspace --all-targets -D warnings pass.
• cargo test --workspace: all seven of MN-01 to MN-07 pass.

🤖 Generated with Claude Code

https://claude.ai/code/session_013Eo1UJoRXDrVSdkPw8UC35

---

Generated by Claude Code