# Ckd — proof obligations (E8 / Blaster checklist)

Status of every obligation in `lean/Ckd/Ckd/`. The scaffold builds under
`leanprover/lean4:v4.31.0` (`lake build` succeeds). **6 of 7 obligations are now proved**
in core Lean 4 (no Mathlib); the only remaining `sorry` is the circuit seam, which is the
Blaster/E8 target (see note below).

Authoritative relation: `proto/circuit/ckd/RELATION.md` (REQ-CKD-VR-01).
Definitions live in `Ckd/Spec.lean` and carry **no** `sorry`. Supporting arithmetic lemmas
live in `Ckd/Lemmas.lean` (core Lean 4 only). Every proved theorem was checked with
`#print axioms` to depend only on `propext, Classical.choice, Quot.sound` (no `sorryAx`,
no `native_decide`).

Regenerate the remaining list with: `grep -rn "sorry" lean/Ckd/Ckd/`
(ignoring the two doc-comment mentions in `Spec.lean` and `Sufficiency.lean`).

## Sufficiency conditions — `Ckd/Sufficiency.lean`  (all PROVED)

| # | Theorem | Condition | REQ | Status |
|---|---------|-----------|-----|--------|
| 1 | `mode_byte_significant`     | S-01 — hardened vs soft tag distinctness (`msgZHard ≠ msgZSoft`) | REQ-CKD-S-01 | proved |
| 2 | `adder_exact`              | S-02 — adder exactness: `kL_child = kL_par + 8·trunc28(Z)` (no slack, no dropped carry) | REQ-CKD-S-02 | proved |
| 3 | `single_canonical_vector`  | S-03 — single canonical `kL` vector: `natToLE32` round-trips with `leToNat` mod 2^256 | REQ-CKD-S-03 | proved |
| 4 | `bit255_invariant`         | S-04 — bit 255 = 0 on every derived `kL` (`kL_child < 2^255`); requires `WellFormed master` | REQ-CKD-S-04 | proved |
| 5 | `no_mod_L_alias`           | S-05 — no mod-L slack: child `kL` is the exact integer, not the `+L` alias | REQ-CKD-S-05 | proved |
| 6 | `clamp_complete`           | S-06 — Icarus clamp completeness: `icarusClamp` output satisfies `clamped` | REQ-CKD-S-06 | proved |

**Note (S-01/S-03/S-06):** (completeness proved; circuit-level rejection deferred to Seam — see PROOF-REPORT.md "Completeness vs rejection").

## Seam obligation — `Ckd/Seam.lean`  (DEFERRED-BLOCKED)

| # | Theorem | Condition | REQ | Status |
|---|---------|-----------|-----|--------|
| 7 | `circuit_models_relation` | Seam — `circuit_constraints ⊨ Rckd` over the canonical `kL` vector the gadget emits | REQ-CKD-VR-03 | **deferred-blocked** |

**Why the seam is deferred-blocked (Phase 4 spike NO-GO, 2026-06-27).**
`Seam.lean` models the R1CS witness, its constraint system (`circuitConstraints`),
and the projection (`witnessRelation`) as **opaque**. With opaque constraints there
are only two ways to close the goal: (a) introduce an axiom that is morally
`circuitConstraints w → Rckd …` — an axiom equal to the conclusion, which is not a
proof; or (b) replace the opaque constraint model with the gadget's concrete R1CS
constraint system and extract `Rckd` from it.

Path (b) is the Blaster/E8 import, and Phase 4 determined it is currently out of
reach. The deployed gnark circuit contains **2,774,043 R1CS constraints** of which
**>99% are HMAC-SHA512 and Ed25519 fixed-base scalar-mult gadgets** — exactly the
primitives that `Spec.lean` declares `opaque hmacSha512` / `compressBase` and
explicitly does not formalize. Bridging the gnark SHA-512 + Ed25519 R1CS gadgets
to those opaque functions requires either (i) a multi-month core-Lean formalization
of SHA-512/Ed25519 R1CS soundness (out of scope; contradicts the deliberate
opaque-primitive decision) or (ii) a hand-asserted abstraction whose fidelity to
the real ~2.77M-constraint circuit cannot be certified without a gnark→Lean
extraction tool that does not exist. Neither path meets the plan GO criterion.

The arithmetic sub-layer (no-mod-L adder, canonical decomposition, clamp,
bit-255 pin) is already proved `sorry`-free in core Lean (`Sufficiency.lean` +
`Lemmas.lean`, Phase 1-2). The seam's residual is exactly and only the hash/curve
bridge. The seam therefore remains deferred-blocked as the E8/Blaster target.

Spike report: `docs/superpowers/spikes/2026-06-27-seam-a-r1cs-feasibility.md`

What Blaster must provide: a faithful encoding of the gadget's R1CS constraints
(booleanity of the `kL` bits, the no-mod-L byte/carry adder, the SHA-512 and
Ed25519 compress gadgets sound w.r.t. `hmacSha512`/`compressBase`) such that any
satisfying assignment projects, over the single canonical `kL` vector
(REQ-CKD-S-03), to a `deriveChain` of a well-formed clamped master.

## Coverage

- **REQ-CKD-VR-02** — `lean/Ckd/` compiles under its pinned `lean-toolchain`, defines `Rckd`,
  and the six sufficiency conditions are now **proved** (rows 1–6).
- **REQ-CKD-VR-03** — `Seam.lean` states `circuit_constraints ⊨ Rckd` (row 7); proof
  deferred-blocked per the Phase 4 spike NO-GO (opaque HMAC-SHA512 + Ed25519 R1CS soundness,
  ~2.77M constraints; see spike report above).

Proved: **6 / 7**. Remaining: **1** (seam, deferred-blocked).