[afflom]

Requested by Alex · project thread

Implements #127 (L5.2 of #106) as decided in D7 (#110): κ-addressing is a workspace source package in this repository beside stdlib/, outside language/ and schemas/ (no compiler-semantics ID moves), gate-held, with uor-addr as the oracle. The labels take the form D3 (#108) handles consume.

What it adds

kappa/ (module prefix LexLeanKappa, source package std = stdlib), two modules, five production roots (rust-std, effects allocation, overflow):

Module	Roots	Oracle
Label	kappaLabel (sha256: + hex SHA-256, 71 bytes), isLabel, handleWire kind canonical = kind@label	uor_addr::json::address, the 12 committed JSON fixtures, the 5 committed .kappa-label files
Json	canonicalJson, jsonLabel	uor_addr::json::canonicalize / address

Register (R3 order: rows, scenarios, failing cases, implementation — one commit each)

KA-01 package, roots, no identity move; KA-02 label, D3 handle, fixtures; KA-03 canonical JSON differential. New prefix KA (suite kappa-addressing): SL-09..SL-12 are already taken by the open member stack (#326/#328/#363), so a new prefix avoids a collision on forward merge. Register 475 -> 478; README row KA-01..KA-03, "All 478 registered conformance IDs".

Choices the issue left open

• Location/prefix: kappa/ workspace member, prefix KA (above).
• Scope: sha256 axis, the JSON realization, the D3 handle. GGUF, ONNX, the other four hash axes and E-series composition are not written. So [0.5.0] κ-addressing in LexLean, validated against uor-addr #127's "every committed fixture yields the same label" holds for the 12 JSON fixtures; for the 5 GGUF/ONNX .kappa-label files only the label form (isLabel) is checked. [0.5.0] κ-addressing in LexLean, validated against uor-addr #127 should stay open for those forms.
• D3 handle wire form: kind@label, kind = [a-z0-9-]+, else refused (Option). handleOf returns the Handle {kind, label} structure.
• NFC: no UCD tables in LexLean, so NFC is computed only for ASCII, Latin-1 and the combining marks U+0300–0303, 0308, 030A, 0327 after a letter that composes with them (53 composites, each checked against Python unicodedata); any other non-ASCII scalar is refused with no output rather than guessed. Numbers: integers only (fraction, exponent, -0 refused). Fails closed.
• Duplicate member names: refused. uor-addr 0.2.0 keeps both; its unreleased main (953fb68) refuses. The corpus treats this as a design divergence, not a disagreement.
• No theorems: a reflexivity theorem on kappaLabel of a literal is refused by the kernel (LLV7002); the label is held by the differential, not a proof.
• Oracle dependency: uor-addr =0.2.0 (default features off, std) in repo-conformance only. Its graph adds arrayref (BSD-2-Clause), added to deny.toml's allow list with the reason; I could not run cargo deny here (not installed), the licences were read from the crate manifests.
• The 5 .kappa-label files are vendored under tests/kappa/ from uor-addr v0.2.0 (no authority row; they are oracle data used for the label form only).

#363 (canonical JSON writer)

#363 is open, draft, and based on member2-order, not release/v0.5, so nothing here depends on it. Json writes (and reads) its own canonical form because uor-addr's differs from §21.7 (NFC; no final LF). If #363 lands, escapeString there could replace Json.quoted.

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

• conformance_ka_01/02/03 pass (370 s together); plants observed failing (VERIFICATION.md): source package dropped; sha512: prefix (23/23 runs); uppercase hex in isLabel (7/127); handleWire label for kind (7/15); reversed key order (3/120); raw newline (1/120); dropped combining mark (6/120).
• KA-03 corpus: 120 evaluator runs (78 refused, 42 accepted), 600 under rustc.
• lexlean verify of kappa accepts with exact axiom policies; kappa/expected/ holds 23 build oracles and 105 verification records (written for the new project only).
• cargo fmt --check, clippy --workspace --all-targets --all-features -D warnings, validate-model (478 ids), validate-spec-links (478 rows), check-golden, check-fixtures (309), check-reproducibility, cargo test -p repo-conformance --test bdd, conformance_rp_*, conformance_pk_05, conformance_ex_*: pass. conformance_ex_09 failed once under heavy host load alongside other work and passed alone (567 s).
• Not run: just vv whole, check-test-inventory (disk full), cargo deny.

---

Generated by Claude Code