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

CONFORMANCE.md

@@ -307,6 +307,7 @@ the error registry does not sanction (R5, `ERRORS.md`).
 | `MD-10` | `build` | Model declarations are part of the semantic identity, so changing an artifact byte with its declared digest, a descriptor, a claim, or a check changes the semantic ID, and language-1.2 snapshots carry, schema-valid, every elaborated declaration, generated obligation, cross-check, and required check. |
 | `MD-11` | `build` | Model constructs have production dispositions under which artifacts, realizations, models, validators, and checked applications are realized through their elaborations while contracts and evidence are erased, the realization table covers every new runtime construct, and production roots applying an artifact-backed model, directly and through its checks, are eligible and extract the same closure through Lean. |
 | `MD-12` | `build` | The committed models example verifies nontrivial deterministic stateful, rule, statistical, artifact-backed neural, and composite models with every claim kernel-checked, and planting a contract and realization mismatch in it is refused by verification. |
+| `MD-13` | `build` | IEEE-754 binary32 and binary64 bit patterns decode in LexLean to exact dyadic rationals (sign, integer mantissa, exponent) for zero, subnormal, and normal values while rejecting non-finite and out-of-range patterns, and the models corpus derives round(a * b / c * 2^32) from three binary32 patterns by exact integer arithmetic that agrees with an independent exact rational computation under Lean and refuses a planted rounding or exponent mutation. |
 
 ## oracle
 

README.md

@@ -137,7 +137,7 @@ just vv        # the complete normative acceptance gate (SPEC.md §9.2)
 just release   # vv, then the §30 release criterion; refused until 1.0.0
 ```
 
-All 382 registered conformance IDs are implemented and pass; `just vv` runs clean from a checkout with the pinned toolchain installed.
+All 383 registered conformance IDs are implemented and pass; `just vv` runs clean from a checkout with the pinned toolchain installed.
 
 The differential against the independent generator `lean4-prod` (SPEC.md §17.19, `OR-01`..`OR-08`) acquires it at its pinned commit: from the checkout `LEXLEAN_ORACLE_DIR` names, or by fetching the commit with `git` into the Cargo target directory (`LEXLEAN_ORACLE_CACHE` overrides), and builds it with the pinned Lean and Rust toolchains. It is validation evidence only and no input to any identity. An oracle that cannot be acquired, is not the pinned files, or fails is unavailable: that fails the gate on Linux x86-64 and is printed as `NOT VALIDATED` elsewhere, and is never reported as agreement.
 
@@ -170,7 +170,7 @@ Every row is validated by `just vv`; the IDs link the claim to its register row,
 | GNAF requests over the calculus: an optimizer-independent complete-system universe, a machine contract that accounts every action, scalar and Pareto orders without weighting, fail-closed validation, and kernel-checked answers and authority vectors | `GN-01`..`GN-08` | `build` |
 | GNAF certification: certificates that prove a global optimum, an argmin, or a complete Pareto frontier over the independent universe from a premise for every system, a library proving the checker sound, closed transformation schemas, local normality kept distinct from optimality, a bridge from a representation metric to execution cost, and honest non-global statuses | `GC-01`..`GC-11` | `build` |
 | Semantic preservation from the source to the calculus: a validated lowering of every production root, a kernel-checked certificate per root relating the lowered program to the source denotation with exact width predicates, a differential evaluator, a proof library that is LexLean source (native core modules migrated once from the Lean it replaces, its Lean generated by the compiler) pinned by exact axioms, certificate checking in verification, a declared Rust machine on which every rendering is evaluated, certificate B relating every rendering to its program, certificate E composing them end to end, boundary validators, and a rustc differential of the declared machine | `SP-01`..`SP-13` | `build` |
-| Language-1.2 models: content-addressed typed artifacts, contracts with sound validators, exact deterministic, rule, statistical, neural, and composite realizations, generated evidence obligations restated in Lean, checked runtime boundaries, and their identity, production, and verification | `MD-01`..`MD-12` | `build` |
+| Language-1.2 models: content-addressed typed artifacts, contracts with sound validators, exact deterministic, rule, statistical, neural, and composite realizations, generated evidence obligations restated in Lean, checked runtime boundaries, and their identity, production, and verification | `MD-01`..`MD-13` | `build` |
 | The differential validation oracle: `lean4-prod` pinned by commit and content hash as validation evidence only, a corpus of every production root and one probe per runtime construct, a comparison of acceptance, contract, behavior, and resources that never compares bytes, versioned tables of known differences and of constructs outside the overlap, planted discrepancies detected, failures that are unavailable rather than validated, and its isolation from every identity | `OR-01`..`OR-08` | `build` |
 | The production export contract: a stable, versioned `lexlean::api::production` façade and its CLI through which a consumer compiles production roots to certified Rust packages; closed requests refused before Lean on every root, target, pin, evidence, path, and package defect; results binding every output to the source, semantic, compiler-semantics, target, compiler-input, preservation, and certificate identities with unforgeable certification; deterministic, confined, offline bundles; source-free replay; versioned schemas; each output's effects and what `recursion` asks of the host | `PX-01`..`PX-13` | `build` |
 | Language-1.2 reasoning machines: logics, guarded inference rules, verifiers, and forward, search, and generate-and-verify reasoners elaborated to ordinary declarations, with exact obligations, fixed-template theorems over the axiom-free reasoning runtime, a closed runtime boundary, resource ledgers, and their production, calculus, and GNAF realization | `RS-01`..`RS-14` | `build` |

SPEC.md

@@ -3347,11 +3347,36 @@ member or value is an ordinary schema failure (`LLT4001`).
     checked applications are realized through their elaborations; contracts
     and evidence are erased (§17.13). Lean extraction of a root sees only
     elaborated definitions.
+15. **IEEE-754 bit patterns as exact dyadic rationals.** Because no floating-point
+    type exists in LexLean, IEEE-754 `binary32` (1 sign bit, 8-bit biased
+    exponent with bias 127, 23-bit trailing significand) and `binary64` (1 sign
+    bit, 11-bit biased exponent with bias 1023, 52-bit trailing significand)
+    parameter bit patterns enter exact integer derivations by decoding to exact
+    dyadic rationals `(sign, mantissa, exponent)` representing
+    $(-1)^{\text{sign}} \cdot \text{mantissa} \cdot 2^{\text{exponent}}$ over
+    `nat` and `int`:
+    - Out-of-width bit patterns and non-finite biased exponents (`255` for
+      `binary32`, `2047` for `binary64`, covering infinities and NaNs) decode
+      to `none`.
+    - Zero and subnormal patterns (`biased = 0`) decode to `mantissa = fraction`
+      and `exponent = -149` (`binary32`) or `exponent = -1074` (`binary64`).
+    - Normal patterns (`1 <= biased <= 254` for `binary32`, `1 <= biased <= 2046`
+      for `binary64`) decode to `mantissa = 2^23 + fraction` and
+      `exponent = biased - 150` (`binary32`) or `mantissa = 2^52 + fraction`
+      and `exponent = biased - 1075` (`binary64`).
+    - Fixed-point scale ratios $\operatorname{round}(a \cdot b / c \cdot 2^{32})$
+      from three `binary32` bit patterns decode $a$, $b$, and $c$ to exact
+      dyadic rationals, reject any `none` operand or a zero divisor
+      ($\text{mantissa}_c = 0$) as `none`, and compute the nearest integer
+      (ties to even) by exact integer Euclidean division and bit-stepping over
+      `iterate_until`, kernel-checked by `decide`.
 
 `examples/models` is the committed instance: a stateful deterministic
 session, a rule policy, a statistical triage and an artifact-backed neural
-recognizer, every composite form, checked boundaries at production roots,
-and every claim kind, all verified by pinned Lean.
+recognizer, IEEE-754 `binary32` and `binary64` dyadic rational decoding and
+exact `round(a * b / c * 2^32)` scale-ratio derivations, every composite
+form, checked boundaries at production roots, and every claim kind, all
+verified by pinned Lean.
 
 #### Reasoning machines (language 1.2)
 
@@ -9168,6 +9193,7 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte
 | `MD-10` | `models` | Model declarations are part of the semantic identity, so changing an artifact byte with its declared digest, a descriptor, a claim, or a check changes the semantic ID, and language-1.2 snapshots carry, schema-valid, every elaborated declaration, generated obligation, cross-check, and required check. | §17.12, §21.4 |
 | `MD-11` | `models` | Model constructs have production dispositions under which artifacts, realizations, models, validators, and checked applications are realized through their elaborations while contracts and evidence are erased, the realization table covers every new runtime construct, and production roots applying an artifact-backed model, directly and through its checks, are eligible and extract the same closure through Lean. | §17.13, §17.14, §22.10 |
 | `MD-12` | `models` | The committed models example verifies nontrivial deterministic stateful, rule, statistical, artifact-backed neural, and composite models with every claim kernel-checked, and planting a contract and realization mismatch in it is refused by verification. | §17.12, §28.6 |
+| `MD-13` | `models` | IEEE-754 binary32 and binary64 bit patterns decode in LexLean to exact dyadic rationals (sign, integer mantissa, exponent) for zero, subnormal, and normal values while rejecting non-finite and out-of-range patterns, and the models corpus derives round(a * b / c * 2^32) from three binary32 patterns by exact integer arithmetic that agrees with an independent exact rational computation under Lean and refuses a planted rounding or exponent mutation. | §17.12, §28.6 |
 | `RS-01` | `reasoning` | Language 1.2 logic, inference_rule, verifier, and reasoner declarations, the forward, search, and generate_and_verify strategies, the initial_invariant, terminates, observation_invariant, and answer_correct claims, and the reasoning_failure type belong to the closed lexlean/semantic-module/2 schema and its snapshot schema, are rejected under language 1.1 before either backend runs, and admit no member, strategy, or claim outside the closed schema, such as an opaque oracle, a prompt, an unregistered strategy, or an unregistered claim, which fail with LLT4001. | §17.12 |
 | `RS-02` | `reasoning` | A logic names a prior state relation and an optional invariant with a statement-exact preservation theorem and an optional ranking, each of exactly its state type, and an inference rule over a logic is a typed guard, conclusion, and optional binding with a candidate list whose soundness theorem states exactly that the guard implies the relation and whose progress theorem states exactly that the ranking decreases; logics, rules, verifiers, and reasoners may be generic, and a predicate of the wrong signature, an inexact theorem, a rule over another logic than its reasoner's, or a use with the wrong number of type arguments fails with LLT4010. | §17.12 |
 | `RS-03` | `reasoning` | A verifier links an executable Boolean check over a subject and a candidate to a prior proposition-valued specification by statement-exact soundness and optional completeness theorems that Lean restates against the fixed reasoning semantics; an inexact statement or a verifier whose subject or candidate type differs from its reasoner's fails with LLT4010, and a false soundness theorem is refused by verification with LLV7002. | §17.12, §22.6 |
@@ -9228,7 +9254,7 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte
 | `AU-11` | `authoring` | Malformed core notation fails closed and never panics: an unclosed delimiter, a keyword used as a name, a label that is not the number of its node, a reference to a node not yet written, a numeral with a redundant leading zero, a statement that defines no node, a nesting beyond the bound, and every single-token deletion and duplication of a committed module fail with a registered code at a position in the notation or link to a module that decodes. | §17.21.8 |
 | `AU-12` | `authoring` | A core module written with names for its statements and its variables reads to exactly the module its canonical notation reads to, and the canonical notation keeps the names of the binders and writes the numbers of the statements: a variable is written by the name of its binder exactly when no nearer binder has the name, a constant a binder in scope is named like is written as a string, a theorem added to the certification library by name reads to the committed module and is written as the committed bytes, and an unknown or repeated statement name and a variable given universe levels are refused with a position. | §17.21.8 |
 
-**Total required capability IDs:** 382.
+**Total required capability IDs:** 383.
 
 No row may be downgraded to `some-true` or `open`. Upstream Lean facts are ledger/authority rows, not substitutions for these build behaviors.
 

VERIFICATION.md

@@ -4747,6 +4747,59 @@ is false
 
 Removed: the copy was discarded; the committed example verifies.
 
+### IEEE-754 dyadic decoding and scale-ratio derivation can fail (Issue #118)
+
+`MD-13` was registered before its named test failed on the missing corpus
+declarations:
+
+```text
+thread 'conformance_md_13' (1417488) panicked at crates/conformance/src/cases/models.rs:3284:9:
+Models.Recognizer declares `Dyadic`
+test conformance_md_13 ... FAILED
+```
+
+Planted, one at a time in a focused copy of `examples/models/src/Recognizer.lex.tex`:
+
+- the normal `binary32` exponent offset `150` (`biased - 127 - 23`) replaced by
+  `149` in `decodeBinary32`, which still links cleanly (`lexlean check` exits
+  `0`) because the result remains an `Option Dyadic`:
+
+  ```text
+  error[LLV7002]: Lean rejected `Models.Recognizer` (error): Tactic `decide` proved that the proposition
+    DyadicMatches (decodeBinary32 8388608) 0 8388608 (-149)
+  is false
+  ```
+
+- the tie-to-even rounding branch
+  `(prim subtract q (prim negate (prim remainder q (2 : Int) (0 : Int) : Int) : Int) : Int)`
+  in `dyadicRatioRound` replaced by unconditional round-up
+  `(prim subtract q (-1 : Int) : Int)`, which still links cleanly and agrees on
+  every non-tie and odd-tie case, but rounds an exact tie with even quotient up
+  instead of keeping it even:
+
+  ```text
+  error[LLV7002]: Lean rejected `Models.Recognizer` (error): Tactic `decide` proved that the proposition
+    scaleRatioRound32 1065353219 1069547520 1140850688 = Option.some 12582916
+  is false
+  ```
+
+- a seeded scale-ratio expectation skewed by `+1` against the independent
+  `u128` rational oracle in `conformance_md_13`:
+
+  ```text
+  error[LLV7002]: Lean rejected `Models.Recognizer` (error): Tactic `decide` proved that the proposition
+    ...
+  is false
+  ```
+
+`conformance_md_13` plants all three mutations in `Recognizer.lex.tex`,
+asserting that `check` succeeds and `verify` fails with `LLV7002` on each, and
+verifies 40 seeded `binary32`, `binary64`, and `round(a * b / c * 2^32)`
+theorems against the independent exact rational oracle in addition to the
+committed `examples/models` corpus.
+
+Removed: the committed `examples/models` corpus is unchanged; `conformance_md_01`..`conformance_md_13` pass.
+
 ### reasoning rule priority order can fail
 
 Planted: the leaves of `E.select` were combined in reverse of the declared order (`leaves.into_iter().rev()` before `balanced` in `elaborate_forward`), so the last rule is tried first. Command: `cargo test -p repo-conformance --test conformance -- conformance_rs_05`. Expected: a forward reasoner that fires rules out of their declared priority order. The case reads the order the select term evaluates its guards in (a `match` scrutinee before its branches, a `let` value before its body), not document order, because canonical JSON orders object keys alphabetically.