feat(models): decode IEEE-754 bit patterns as exact dyadic rationals (MD-13, #118)

[afflom]

Closes #118

Summary

Implements plan item L3.5 of #106 (IEEE-754 bit patterns as exact dyadic rationals, capability ID MD-13):

1. Specification & Register (R1, RP-07):
   • Registers capability MD-13 in model/ids.toml, SPEC.md §17.12 (Rule 15), and SPEC.md §31 (382 total required capability IDs).
2. BDD & Conformance (R3):
   • Adds @MD-13 @build scenario to features/suites/models.feature and conformance_md_13 in crates/conformance/src/cases/models.rs and crates/conformance/tests/conformance.rs.
3. IEEE-754 Dyadic Rational Decoding & Scale-Ratio Derivation (examples/models):
   • Adds Dyadic ((sign, mantissa, exponent) representing $(-1)^{\text{sign}} \cdot \text{mantissa} \cdot 2^{\text{exponent}}$), dyadicTriple, DyadicMatches, byteToInt, decodeBinary32, decodeBinary64, decodeBinary32Bytes, decodeBinary64Bytes, dyadicMul, dyadicRoundShift, dyadicRatioRound, scaleRatioRound32, and scaleMultipliersRound32 in examples/models/src/Recognizer.lex.tex, plus deriveScaleMultiplier and deriveChannelMultipliers in examples/models/src/Main.lex.tex.
   • Proves 36 theorems in Models.Recognizer and 4 theorems in Models.Main by decide{} under pinned Lean and leanchecker, covering binary32 and binary64 positive/negative zero, minimum/maximum subnormal, minimum/maximum normal, unit scale (1/255), little-endian byte-slice decoding from the committed banner artifact, non-finite/out-of-range rejection (+Inf, -Inf, NaN, negative/overflow widths), tie-to-even dyadic rounding, and exact $\operatorname{round}(a \cdot b / c \cdot 2^{32})$ scale-ratio and channel-multiplier batch derivations.
4. Independent Differential & Planted-Defect Verification (VERIFICATION.md, conformance_md_13):
   • Checks all corpus vectors and 40 seeded binary32, binary64, and round(a * b / c * 2^32) theorems against an independent u128 rational oracle under Lean, and verifies that planted mutations to the normal exponent offset (-150 $\to$ -149), the tie-to-even rounding rule, and a skewed oracle expectation are each accepted by check and refused by verify with LLV7002.

Verification

• just model-write
• cargo xtask validate (382 IDs, 80 codes)
• cargo xtask check-golden
• LEXLEAN_ONLY_EXAMPLE=models cargo xtask verify-examples (161 normalized verification records)
• cargo test -p repo-conformance --test bdd
• cargo test -p repo-conformance --test conformance conformance_md_02 -- --exact
• cargo test -p repo-conformance --test conformance conformance_md_13 -- --exact
• cargo fmt --check & cargo clippy --workspace --all-targets -- -D warnings

[afflom]

Heads-up on the register count, not a review. This PR's base is 96b382df (register 381) and it adds MD-13 (382). Main is now d58c4ef9: #130 merged and added PX-13, so main is 382 and this PR reads as 383 once main is merged in.

The count is written in four places (README.md "All N registered conformance IDs", SPEC.md "Total required capability IDs", crates/conformance/src/cases/repository.rs table.len(), xtask/src/spec_links.rs). Both PRs changed each of them from 381 to 382, so a merge of main reads as clean and is wrong by one: set all four to 383 by hand and run cargo xtask validate-model --write, validate-spec-links, conformance_rp_07 and conformance_rp_11 before pushing. (Same trap I hit merging #101.)

Separately: this PR changes examples/models, whose verification record #144 and #146 (hh) also regenerate; whichever of the three lands later regenerates it again on the combined tree.

---

Generated by Claude Code

[afflom]

Maintainer triage (the author session has ended; I carry this PR). State at 18:05Z: closes #118, which is milestone v0.5, so it is outside the v0.4 release path. The branch is dirty against main (80331cb4) and its CI is from 02:32Z on a base before #130, #144, #152 and #156. Plan: it is not abandoned; it waits for the v0.4 PRs that move the language-1.2 identity to land (#158 first, then #146), because anything regenerated before them would be regenerated again. Then: merge main, regenerate the records once, run the full gate, review against #118's acceptance, and merge on a green head with the maintainer review recorded here. If you are the author's session and still running, say so here and take it.

---

Generated by Claude Code

[afflom]

Train status for #150 (the hand-written part now lives on train/dyadic @ f329834, ported onto current main 243f0c7; this branch is no longer updated).

Issue #118 Definition of Done: "A corpus derivation computes round(a·b/c·2^32) from three float32 patterns exactly and agrees with an independent exact computation."

Item	Command / test	Result
Corpus derivation from three float32 patterns	scaleRatioRound32, deriveScaleMultiplier, deriveChannelMultipliers; theorems scale_ratio_*, scale_multipliers_channel_batch (Models.Recognizer), corpus_scale_* (Models.Main) closed by decide{}	cargo test -p repo-conformance --test conformance conformance_md_13 -- --exact: ok (772 s, pinned Lean 4.32.1)
Agrees with an independent exact computation	u128 rational oracle in models.rs (shares no algorithm with the iterative bit-stepper); 9 fixed ratio vectors and 16 seeded triples	same test: ok
binary32 zero / ±0 / min and max subnormal / min and max normal	binary32_* theorems	proved by decide; oracle vectors agree
binary64 same set	gap found: only +0 and min subnormal were proved. Added binary64_neg_zero, binary64_max_subnormal, binary64_min_normal	proved; oracle vectors added; test ok
Little-endian slicing of the committed banner artifact	binary32_banner_*, binary64_banner_*	proved by decide
Non-finite and out-of-width rejection	binary32_rejects_*, binary64_rejects_*, scale_ratio_rejects_*	proved by decide
Tie-to-even	dyadic_round_shift_*tie*, scale_ratio_tie_*	proved by decide
Planted defects (exponent offset, tie rule, skewed oracle)	planted inside conformance_md_13, recorded in VERIFICATION.md	check accepts, verify refuses with LLV7002; test ok
R3 order, R1/R5 gates	cargo xtask validate-spec-links, validate-model	404 rows bijective; model, audits clean
fmt / clippy	cargo fmt --check, cargo clippy -p repo-conformance --all-targets -- -D warnings	clean

Theorem count is now 39 in Models.Recognizer + 4 in Models.Main = 43.

Not run: just vv as a whole, check-golden, the bdd suite, cargo deny, and a separate lexlean verify on a scratch copy of the whole examples/models project (the conformance test does its own Lean verification of a copy). No generated outputs are committed; the regenerated records are for the integration branch.

---

Generated by Claude Code

[afflom]

Maintainer status: the content of this PR (MD-13, the dyadic decoding and the u128 oracle in conformance_md_13) is on the v0.4 train, #167, re-applied there so that it meets the byte-literal, widening and certificate changes in one regeneration (e30230ab3, f329834e6 on claude/v0.4-train). #167 closes #118. Because the train could not take this branch's head as an ancestor without a tree-changing merge, this PR will be closed by hand when #167 merges, with the pointer above; its commits are credited in the train's history.

---

Generated by Claude Code

[humuhumu33]

Content review of #150 as it lands on #167 (merge 6375f32, train head e24a7ff).

The decoding and the scale ratio are correct. binary32: subnormal exponent -149, normal biased-150 with the implicit 2^23. binary64: -1074 and biased-1075 with the implicit 2^52. Signed zero keeps its sign, and the 255/2047 exponents are refused. Byte order is little-endian. round(ab/c2^32) is exact with ties to even and symmetric in sign, and for every finite binary32 triple the shift (at most 389) stays under the 512 fuel. I checked every committed vector and about 60,000 random binary32 triples, ties included, against exact fractions: all agree. The u128 oracle cannot overflow (product below 2^48, shift below 80) and has no binary64 ratio. #118's acceptance is met.

1. dyadicRoundShift (examples/models/src/Recognizer.lex.tex:356) drops iterate_until's fixed-point flag. For exponent + shift > 512 it returns mantissa * 2^512 without a signal (the binary64 max normal at shift 0 gives 2^564), and its sticky round-up branch is never run. Return Option and refuse when the flag is false, as dyadicRatioRound does, or remove dyadicRoundShift and dyadicMul, which no derivation uses.
2. decodeBinary64 (:300) accepts both the signed and the unsigned 64-bit form. No theorem, oracle vector or seeded case reaches the unsigned branch, and out-of-range binary64 input (< -2^63, >= 2^64) has no rejection theorem. SPEC.md:3524 rule 15 should state each width's accepted range. Please add theorems: 13832806255468478464 decodes to (1, 6755399441055744, -52); 9223372036854775808 to (1, 0, -1074); -9223372036854775809 and 18446744073709551616 to none.
3. CHANGELOG.md:55 says 43 theorems (39 + 4). The train adds 43 to Models.Recognizer and 4 to Models.Main, 47 in all. CHANGELOG.md:50 (and :66) say the register is 404 rows; the train is at 413.
4. VERIFICATION.md:5238 records "..." for the skewed-oracle refusal. Please paste the real LLV7002 line for seeded_ratio_15.
5. Nit: the k < 0 branch of dyadicRatioRound has only an even-quotient tie (scale_multipliers_channel_batch), so a round-half-down mutation there survives. scaleRatioRound32 1065353219 1065353216 1149239296 = some 4194306 covers it. The seeded ratios span only shifts of about [-16, 16] with normal operands, and the Bytes decoders have no past-the-end theorem.
6. Nit: the fixed oracle tables in crates/conformance/src/cases/models.rs:3425, :3451 and :3486 are hand copies of the theorem literals; reading them from the module data would make the corpus-vs-oracle check real.
7. Nit: rule 15 is normative text for corpus code in examples/models, and it does not state the little-endian byte order. byteToInt (:279) duplicates to_int (SM-32, same train). *_neg_one_half decodes -1.5.

The register agrees at 413 in all four places on e24a7ff. conformance_md_13 passed in that head's rest leg; the RP-08/11/12 failures there come from other members.

This is a comment review; formal approval will be given on #167's final head once both vv legs are green.

[afflom]

Landed through the v0.4 train, #167, merged to main as 193cd2148: MD-13 (IEEE-754 bit patterns as exact dyadic rationals) is in the register, the scenario, the named test, the model reader, and the regenerated language-1.2 records on the combined identity. #118 is closed by that merge. This branch's own head (da31f6bc4) predates certificates A and B as data and the identity moves of #68 and #151, so it is not merged itself; the content is in 7053b2185..f5748851c of the train. Closing. hh's remaining text points on this member are tracked in #182.

---

Generated by Claude Code