[afflom]

Closes #10.

This authors the missing U64 ULEB128 semantics in the repository LexLean graph: shortest encoding, a ten-byte prefix decoder that preserves the suffix, exact decoding, six typed failures with offsets, and an explicit error order. The public encoder rejects values above U64 maximum before encoding. The generated contract is a projection of the authorized source.

The computational implementation is stored in LexLean native-core source and reconstructed by the locked SDK. It has no handwritten Lean/Rust product input or compiler fallback. General kernel proofs establish both public round trips, exact size for every successful public encoding, one-to-ten-byte bounds, minimum base-128 representation length, prefix/suffix preservation, and bounded/reference encoder refinement. The six computational entry/helper roots have exact empty axiom sets; proof declarations record their exact standard Lean foundational axioms.

Validation:

• 236 independent literal kernel vectors cover 36 positive values, all width transitions/U64 maximum, truncation, overlong forms, every overflowing tenth-byte terminal payload, continuation overflow, invalid byte positions, trailing bytes, and encoder-domain rejection.
• Three source-owned mutations change the radix, byte allowance, and U64 maximum. Each fails at its exact owning kernel declaration and every restored control verifies successfully. Both mutation harnesses also reject conditional omission and early returns; these regressions failed before the audit fix and now pass.
• Registry, scenario, ledger, model, README, verification summary, and conformance projections are maintained together. The required just vv includes the executed mutations and the harness's own negative tests.
• Full local just vv passed with 94 identical canonical artifacts across two clean roots and nine rejected dependency/tool defects. The final full run also passed after strengthening the public size theorem, contract-schema checks, and conditional-omission audits. All five hosted checks passed at e402535cbec0da42f48bbdd3f2d3fff3be77840e: both native bootstrap jobs and both offline jobs plus projection generation.

Evidence procedure records the initial failing conformance test, proof scope, failure ownership, and retained receipts. This implements the codec primitive and its mathematical acceptance; it does not claim a complete archive parser, generated product CLI, or production compression release.

Stacked on #74. M0's separate SDK capability reconciliation (#72 / #5) remains unresolved, so this PR stays unmerged under the milestone merge prerequisite.

Downloaded offline evidence was independently checked against the published archive digests. Each architecture contains two complete no-network just vv runs with 94 identical canonical artifacts within the pair, nine dependency/tool negatives per run, and three setup negatives. All 36 mutation/restoration pairs have exact, duplicate-free source inventories, recomputed mutant hashes, matching log/generated-Lean hashes, owning kernel failures, and restored current build/attestation IDs. All 13 hosted generated projections also match the committed files exactly.

Platform	Evidence artifact	ZIP SHA-256
AMD64	11675798773	c4e503d5cb0f3ff476d48b1e23998415bded057f9e2debb15b7804ffbbbfdc48
ARM64	11676877032	15d68bfec351204547e975c6f9e09deb11a728da9793eccd19640350c582c4ea