[afflom]

Requested by Alex · project thread

Part of #127. Slice 2 after #368 (slice 1: KA-01..KA-03).

Scope of this slice

The remainder of #127 is: GGUF and ONNX model forms, the four other hash axes (blake3, sha3-256, keccak256, sha512), and E-series composition. Those do not fit one reviewable PR (the four axes need new 64-bit/Keccak/BLAKE3 primitives in LexLean, GGUF and ONNX are ~1.6 kLoC of parsers in the oracle). This PR does the coherent subset that rests on what slice 1 already has: the five categorical compositions of uor-addr on the sha256 axis.

Added

New module kappa/src/Compose.lex.tex (module prefix LexLeanKappa, same kappa project; no language/ or schemas/ file touched, so no compiler-semantics identity moves). Five production roots (rust-std, effects allocation, overflow), each the kappaLabel of the canonical form of uor-addr's operation, None for an operand isLabel does not accept:

Root	Canonical form hashed	Oracle
composeG2 a b	smaller label, then larger (commutative)	compose_g2_product
composeF4 x	sha256: + min(digest, nibble-wise complement)	compose_f4_quotient
composeE6 x	degree byte (05, 06 when first digest byte mod 9 = 8) + label	compose_e6_filtration
composeE7 x	sha256: + the four digest quarters sorted ascending (= lex-min of the 24 S4 orders)	compose_e7_augmentation
composeE8 x	the label	compose_e8_embedding

Register (R3, one commit each for the rows and the implementation): KA-04 (build, suite kappa-addressing); KA-01 is widened from two modules to three and now lists the five new roots. Register 478 -> 479; README row KA-01..KA-04, "All 479 registered conformance IDs". spec/src edited, SPEC.md / CONFORMANCE.md / model/ids.toml regenerated by cargo xtask validate-model --write.

KA-04 holds each root to uor_addr::composition::compose_* (uor-addr 0.2.0, already the oracle) on a seeded corpus (290 runs for G2 in both operand orders and self-pairs, 101 for the others): extremes, the degree-6 class of E6, a digest and its mirror, quarters in all 24 orders, plus refused operands (other axes, prefix case, short/long digest, upper case, non-hex, trailing newline, non-ASCII byte). It runs under the calculus evaluator and under rustc (rust-std package), reads the commutativity and mirror laws, and plants four defects (G2 order, F4 complement, E6 degree class, E7 quarter order) that the differential must detect: 88/290, 34/101, 11/101 and 81/101 runs disagree. The first run showed the oracle's composed label is exactly SHA-256 of that canonical form.

kappa/expected/ is regenerated for the kappa project only (29 build oracles, 164 verification records); kappa/lexlean.lock relocked. uor-atlas was not touched or run.

Left for #127 (not in this PR)

• GGUF and ONNX canonical forms (and with them the 5 committed .kappa-label fixtures, still only checked for label form via isLabel)
• the blake3, sha3-256, keccak256 and sha512 hash axes and the composition operations on them
• so [0.5.0] κ-addressing in LexLean, validated against uor-addr #127's acceptance sentence (every committed uor-addr fixture yields the same label) still holds only for the 12 JSON fixtures; [0.5.0] κ-addressing in LexLean, validated against uor-addr #127 stays open

Evidence (this host, Linux, Rust 1.97.1, Lean 4.32.1)

• lexlean verify of kappa: accepted, exact axiom policies per definition
• cargo fmt --check, clippy --workspace --all-targets --all-features -D warnings, validate-model (479 ids), validate-spec-links (479 rows), check-golden: pass
• conformance_ka_01..ka_04 (525 s together, run singly), cargo test -p repo-conformance --test bdd, conformance_rp_* (18), conformance_pk_05: pass
• Not run: just vv whole, check-fixtures, check-reproducibility, cargo deny, conformance_ex_*, uor-atlas examples

🤖 Generated with Claude Code

https://claude.ai/code/session_013Asa3QZQru5a9Beo3r4Rfa