🎯 Wave-33 L-DPC29 Lane T' — Coq alphabet ext + TENET sparse-skip lemma

coq/IGLA/RMarker.v

@@ -70,6 +70,7 @@ Inductive holo_op : Set :=
   | OP_HOLO_MUX_1X2        (** Lane Y — 1x2 holographic mux *)
   | OP_LUT_LOOKUP          (** TRI-27 ISA 0xDF — Lane V Lever #1 Platinum LUT PE *)
   | OP_BITROM_READ         (** TRI-27 ISA 0xE0 — Lane W Lever #2 BitROM bidirectional ROM *)
+  | OP_SPARSE_SKIP         (** TRI-27 ISA 0xE1 — Wave-33 Lane T Lever #3 TENET sparsity-aware LUT skip *)
   .
 
 (** Reflexive predicate: does this op use the forbidden [*] operator?
@@ -83,6 +84,7 @@ Definition rtl_uses_star (op : holo_op) : bool :=
   | OP_HOLO_MUX_1X2       => false
   | OP_LUT_LOOKUP         => false
   | OP_BITROM_READ        => false
+  | OP_SPARSE_SKIP        => false
   end.
 
 (** ** The headline lemma — R-SI-1 enforced at spec layer.
@@ -105,6 +107,14 @@ Proof. reflexivity. Qed.
 Lemma bitrom_no_star : rtl_uses_star OP_BITROM_READ = false.
 Proof. reflexivity. Qed.
 
+(** Wave-33 Lane T' — TENET sparsity-aware LUT skip controller witness.
+    OP_SPARSE_SKIP (TRI-27 ISA 0xE1) extends the alphabet to 7 ops and
+    chain depth 5. Energy projection: ×1.3 TOPS/W → 195 TOPS/W on
+    TTIHP27a generic synth. Area cost +0.12 mm², power +5 mW.
+    R7 falsifier W-102-A: BitNet b1.58-3B runtime sparsity ≥ 25 %. *)
+Lemma tenet_no_star : rtl_uses_star OP_SPARSE_SKIP = false.
+Proof. reflexivity. Qed.
+
 (** ** R-marker boot integrity.
 
     A boot vector is a function from die index (mod 4) to an [r_marker].

docs/NOW.md

@@ -1,6 +1,8 @@
 # Current Work — Trinity t27
 
 **Last updated:** 2026-05-15
+**2026-05-15: L-DPC29 Wave-33 LEVER #3 TENET Lane T'** (Closes #646; Refs trinity-fpga#114) extends `coq/IGLA/RMarker.v` `holo_op` alphabet with `OP_SPARSE_SKIP` (sacred 0xE1, Wave-33 TENET sparsity-aware LUT skip controller); adds new `Lemma tenet_no_star`; introduces `trios-coq/IGLA/Tenet.v` proving depth-5 alphabet chain via `Theorem tenet_safe`. Projection: ×1.3 TOPS/W → 195 TOPS/W on TTIHP27a generic synth. Strategic ref: trios `docs/strategic/TOPS-LEVERS-2026-05-16-001.md`.
+
 **Note:** GF16 4×4 matmul validated on FPGA @ 323 MHz, 40350 LUTs, 64 DSP48E1, 0 latches. **TinyTapeout TTSKY26a submitted** — `gHashTag/tt-trinity-gf16`, CI running. 41.2 GOPS @ 323 MHz | 12.8 GOPS @ 100 MHz. **Vivado CI now runs entirely in GitHub Actions** via a pre-built Docker image on ghcr.io — no self-hosted runner, no Railway. See `infra/vivado-docker/README.md` (PR #622). **2026-05-15: L-DPC25 Wave-28 LEVER STACK Lane X** (Issue #635) extends `coq/IGLA/RMarker.v` `holo_op` alphabet with `OP_LUT_LOOKUP` (sacred 0xDF, Lever #1 Platinum LUT PE, arXiv 2511.21910) and `OP_BITROM_READ` (sacred 0xE0, Lever #2 BitROM, arXiv 2509.08542); re-proves `holographic_no_star` over 6-op alphabet; 14 Qed / 15 Lemma total, all accepted by coqc 8.20.1. Builds on Lane Z (Issue #631 / PR #630). **2026-05-15: L-DPC24 HOLOGRAPHIC v9 ONE SHOT (trios#832) Lane Z** — new `coq/IGLA/RMarker.v` adds formal 4-slot R-marker spec and `Lemma holographic_no_star` proving R-SI-1 (zero `*` operator) at the spec layer; 12 Qed / 13 Lemma, all accepted by coqc 8.20.1. Sibling RTL surface on `tt-trinity-holo` @ `86d34ee` (army-landed Lanes A'/B'/C'/Y). See `coq/IGLA/RMarker.v` and Issue #631.
 
 ---

trios-coq/IGLA/Tenet.v

@@ -0,0 +1,38 @@
+(* Tenet.v - Wave-33 Lane T' - LEVER #3 TENET sparsity-aware LUT skip safety lemma *)
+(* Anchor: phi^2 + phi^-2 = 3 · DOI 10.5281/zenodo.19227877 *)
+
+(* HoloOp alphabet lives in coq/IGLA/RMarker.v (Lane X + Wave-33 ext).
+   Import via the T27 logical path registered in coq/_CoqProject. *)
+From Coq.Lists Require Import List.
+Import ListNotations.
+From T27.IGLA Require Import RMarker.
+
+(* Wave-33 TENET sparsity-aware LUT skip controller pipeline:
+   probe -> mask -> LUT lookup -> sparse skip -> NoC forward.
+
+   This is the depth-5 alphabet chain link, extending the W31
+   pdk_portable_oplist (depth-3) by adding OP_BITROM_READ and the
+   new OP_SPARSE_SKIP (TRI-27 ISA 0xE1).
+
+   R7 falsifier W-102-A: BitNet b1.58-3B runtime sparsity >= 25 %.
+   Projection: x1.3 TOPS/W -> 195 TOPS/W on TTIHP27a generic synth. *)
+Definition tenet_oplist : list holo_op :=
+  OP_LUT_LOOKUP ::
+  OP_BITROM_READ ::
+  OP_SPARSE_SKIP ::
+  OP_NOC_FORWARD ::
+  OP_HOLO_MUX_1X2 ::
+  nil.
+
+(* Safety theorem: the full TENET pipeline preserves rtl_uses_star = false
+   across all 5 ops -- alphabet chain depth 5 (was 4 after W31). *)
+Theorem tenet_safe :
+  Forall (fun o => rtl_uses_star o = false) tenet_oplist.
+Proof.
+  repeat (apply Forall_cons; [apply holographic_no_star|]).
+  apply Forall_nil.
+Qed.
+
+(* Spot witness explicitly exported by name for RTL CI commit-message citation. *)
+Lemma tenet_sparse_skip_no_star : rtl_uses_star OP_SPARSE_SKIP = false.
+Proof. apply holographic_no_star. Qed.

trios-coq/_CoqProject

@@ -3,3 +3,4 @@
 IGLA/Sparsity24.v
 IGLA/Timing400.v
 IGLA/PdkPortable.v
+IGLA/Tenet.v