[humuhumu33]

#276 member 1 (SL-09): hexadecimal and decimal in the standard library (LexLeanStd.Numeral) — draft

Rebuild of the closed draft #281 (head e7f942c7) onto release/v0.4 = a1b925dc (register 458), renumbered to SL-09 per my derivation comment on #276 (SL-08 is taken on release/v0.5 by #126 stage-2; SL-09 is the first number free on both lines).

Hand-written part and its local gates only — no record sweep (the stdlib records, goldens, coverage/closure and the committed tests/production-export/stdlib/packages/** for the five new roots are the landing wave's; a red just vv before that sweep is expected and this draft states exactly which assertion moves).

What changed vs #281:

• SL-08 → SL-09 at every site; register row, §31 row, scenario all re-derived against 458, not 443 (count mirrors: 458→459, README, spec-links, repository case).
• README capability row claims discrete `SL-01`, … `SL-05`, `SL-09` — the line's SL series has gaps (06–08 are v0.5-only), and RP-11 recomputes any a..b range against the register, which a gapped range would fail.
• Locks rewritten by the built lexlean lock (the draft carried pre-Buffer values; the entrypoint digest moved when #92 BS-06: LexLeanBoot.RustPrint, the Rust printer as language-1.2 source (draft: register row and failing test) #253 landed).
• Entrypoints sorted (config.rs: sorted unique; the draft inserted Numeral out of order).
• The draft's \title was kept as Natural number addition: every title word must be a concept of the project's glossary (lexlean.std.nat) and "Hexadecimal" is not one (LLL1004) — which is why all four stdlib modules, Text, Sha256 and Buffer included, carry the same title by necessity.

Delivered (6 commits): register row + §31 prose/row + scenario + count mirrors → fail-first case wired (R3, panic evidence below) → module + entrypoint + differential + roots.json → locks → CONFORMANCE.md via just model-write → title/lock correction.

Local gates on a1b925dc + this branch:

• cargo fmt --all -- --check: clean
• cargo xtask validate-model: validate-model: documents current, 459 ids, 86 codes, meta-gate and audits clean (R1)
• cargo xtask validate-spec-links: validate-spec-links: 459 table rows bijective with the register (RP-07)
• R3 fail-first (stub body at 2e081fe00): SL-09 is not implemented: the LexLeanStd.Numeral module and its differential land next — test result: FAILED. 0 passed; 1 failed; 458 filtered out.
• conformance_sl_09 at 623d3285: project check and build pass; the eligibility report matches the five roots and their exact effects; all five evaluator differentials (600 runs each) pass; both reader round trips pass; the five rendered rust-std packages build under the pinned rustc; the case then stops red at the committed-exports step — stdlib/decimal is no package of the committed exports (stack_bounds.rs:349). The five certified packages are what the landing wave regenerates; this draft deliberately does not write them. The armed hexValue plant and the export comparison sit behind that step, so they did not run locally; CI (Linux x86-64 with the pinned Lean) reaches them.
• cargo xtask check-test-inventory: clean (rc 0).
• Not run here: just bdd (whole-suite meta-gate — attempted twice, the shared WSL VM was recycled mid-run by host load both times; CI runs it), just vv (owner's wave), the record sweep.

Known-red until the wave: the case's stack-bounds/committed-export step — packages/rust-std/{decimal,hex_nat,parse_decimal,hex,parse_hex}/** are not committed on release/v0.4 and this PR deliberately does not write them.

Bootstrap private copies (CalculusCheck/RustValidate/AxiomOutput/PrimitiveScan/Buffer decimal printers; CalculusCheck/RustPrint/TokenAudit/PrimitiveScan/Sha256 hex digits) are untouched — they migrate to this member by the module owners after it lands.

Refs #276 (member 1 of 4; members 2–4 take SL-10/SL-11/SL-12).