perf(lean): lower byte literals through explicit typed octets

[afflom]

Scope

Use explicit UInt8.ofNat literals in generated byte arrays without changing source-language semantics, kernel replay, axiom policy, or time limits. Refresh compiler semantic versions and genuinely regenerated build/verification records.

Evidence

Independent review completed. Hosted writer run 37157920780 on c3ba388 succeeded for the complete Atlas, all twelve other examples, and compiler verification. Reviewed artifact contains 500 normalized records; all 355 process results and 710 output hashes validated. The final commit imports only the generated compiler verification namespace refresh; all 469 example records were already identical.

Focused SM-19, compiler tests, model/spec validation, Clippy and source golden checks passed before the hosted writer. Full normative CI and host matrix remain required; this draft does not claim release acceptance.

[afflom]

Independent evidence review: run 37157920780 completed on exact c3ba388. Its 500 normalized records cover the complete Atlas (267), twelve other examples (202), and compiler (31). All 355 process results succeeded and all 710 stdout/stderr hashes recomputed correctly; the Atlas inventory includes all 66 modules for elaboration and replay. Final 98f1c1a imports the exact generated compiler subtree, removing stale namespace filenames. Full normative CI has now been dispatched on the final branch; this writer evidence is not full acceptance.

[afflom]

Current-main integration is not yet accepted. The original exact head c32a77d passed full CI run 37171674234, but main subsequently gained reasoning artifacts without their compiler implementation (see issue #31, comment 5980988926). Merging current main reproduces LLT4001 in ReasoningOracle before compiler golden generation; no declaration tags were renamed and no reasoning artifacts were deleted. The reviewed closed-octet sharing/hygiene follow-up is committed separately as ff92e75, with full CI 37207135528 running (all four supported non-Lean host jobs passed). Its newer-main port is independently source-reviewed and is being checked separately. Kept this PR draft until the current integration and complete required evidence are correct.

[afflom]

Closing as superseded by #68, at the maintainer's direction. This was the first iteration of the typed-octet lowering of byte literals (backend/semantic.rs, the language/semantics-1.x.toml backend identities, and the regenerated outputs); #68 carries the explicit rooted UInt8 lowering with literal-local sharing on a base that includes the reasoning artifacts this branch predates (it was reproducing LLT4001 in ReasoningOracle on merge, per the comment above).

The branch perf/typed-byte-main is left in place. Nothing from it is merged.

---

Generated by Claude Code