feat(rrc): 278-equation corpus — AVM sole output boundary, RRC classifier feeds it

Architecture:
  RRC.Corpus278  — raw features only (Python supplies, Lean owns gate)
  RRC.Emit       — alignment classifier; emitCorpus generic entry point
  AVMIsa.Emit    — sole output boundary; imports Corpus278, stamps bundle

Changes:
- RRC/Emit.lean: extend FixtureRow + RrcRow with 5 generator fields
    (operatorTokens, invariantsDeclared, boundaryConds, templateKey, templateParams)
  Add emitCorpus (schema, corpus) generic emitter; emitFixture is now a thin wrapper
  jRrcRow JSON serializer emits all generator fields
- RRC/Corpus278.lean: auto-generated 278-row FixtureRow list
  Source: archive/experimental-shim-probes/rrc_equation_classifier_receipt.json
  Python extracts raw features; all gating in Lean (alignment gate fires missingPrediction
  for all 278 rows currently — correct, no PIST labels present yet)
- AVMIsa/Emit.lean: import Corpus278; add §7 emitRrcCorpus278 — AVM canaries must
  pass for bundle receipt to be valid; stamped by AVM authority (avm.rrc_corpus278.bundle)
  §8 eval: corpus summary fires (278, 0, 278) — all held, 0 promoted, gate honest
- lakefile.toml: add Semantics.RRC.Corpus278 to Compiler blessed roots; update comment
- 4-Infrastructure/shim/build_corpus278.py: corpus builder script

Build: 3567 jobs, 0 errors (lake build)

Generated with [Devin](https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>

0-Core-Formalism/lean/Semantics/Semantics/AVMIsa/Emit.lean

@@ -13,6 +13,7 @@
 import Semantics.AVMIsa.Run
 import Semantics.ReceiptCore
 import Semantics.RRCLogogramProjection
+import Semantics.RRC.Corpus278
 
 namespace Semantics.AVMIsa.Emit
 
@@ -186,7 +187,46 @@ def emit : EmitResult :=
     json            := jsonBody }
 
 -- ─────────────────────────────────────────────────────────────────────────────
--- §7  Proof-of-life eval witnesses
+-- §7  RRC corpus stamping (278-equation corpus → AVM-stamped receipt bundle)
+--
+--     Architecture:
+--       Semantics.RRC.Corpus278  — raw features (Python-supplied, no decisions)
+--       Semantics.RRC.Emit       — alignment gate (Lean classifies)
+--       Semantics.AVMIsa.Emit    — AVM stamps final receipt + emits JSON (here)
+--
+--     The AVM is the sole output boundary.  RRC.Emit feeds it; AVMIsa.Emit
+--     stamps it.  Promotion remains not_promoted at this stage.
+-- ─────────────────────────────────────────────────────────────────────────────
+
+open Semantics.RRC.Emit in
+open Semantics.RRC.Corpus278 in
+/-- Stamp the 278-equation corpus: run the alignment gate (RRC.Emit), then
+    mint an AVM-authority receipt for the whole bundle, and emit JSON.
+
+    The AVM canary suite must pass for the bundle receipt to be valid.
+    Individual row receipts reflect alignment-gate pass/fail independently. -/
+def emitRrcCorpus278 : String :=
+  -- 1. Classify all 278 rows through the alignment gate
+  let classified := emitCorpus "rrc_corpus278_v1" corpus278
+  -- 2. Run AVM canaries — AVM must be live for the bundle to be valid
+  let avmOk      := canaryReceipts.all (·.valid)
+  -- 3. Mint AVM-authority bundle receipt
+  let bundleReceipt := leanBuildReceipt "avm.rrc_corpus278.bundle" avmOk
+  -- 4. Compute summary statistics
+  let total      := classified.totalRows
+  let passed     := classified.candidateRows
+  let held       := total - passed
+  -- 5. Emit JSON — AVM is the output boundary
+  s!"\{\"schema\":\"avm_rrc_corpus278_v1\"," ++
+  s!"\"claim_boundary\":\"admissibility-and-routing-pass-only;not-promoted\"," ++
+  s!"\"avm_canaries_passed\":{jsonBool avmOk}," ++
+  s!"\"bundle_receipt_valid\":{jsonBool bundleReceipt.valid}," ++
+  s!"\"summary\":\{\"total\":{total},\"passed_alignment\":{passed},\"held\":{held}," ++
+  s!"\"not_promoted\":{total}}}," ++
+  s!"\"rows\":{classified.json}}"
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- §8  Proof-of-life eval witnesses
 -- ─────────────────────────────────────────────────────────────────────────────
 
 -- Individual canary checks
@@ -197,7 +237,16 @@ def emit : EmitResult :=
 -- Receipt validity
 #eval canaryReceipts.map (fun r => (r.targetId, r.valid))
 
--- Full JSON bundle (the "rainbow raccoon compiler" output)
+-- Full canary JSON bundle (the "rainbow raccoon compiler" output)
 #eval emit.json
 
+-- 278-equation corpus: AVM stamps the bundle, RRC.Emit classifies rows
+-- (summary only — full JSON is ~200KB)
+open Semantics.RRC.Emit in
+open Semantics.RRC.Corpus278 in
+#eval
+  let r := emitCorpus "rrc_corpus278_v1" corpus278
+  (r.totalRows, r.candidateRows, r.totalRows - r.candidateRows)
+  -- expect: (278, <passed_alignment>, <held>)
+
 end Semantics.AVMIsa.Emit

0-Core-Formalism/lean/Semantics/Semantics/RRC/Emit.lean

@@ -72,6 +72,18 @@ inductive Promotion where
   - weakAxesCnt:      count of weak (missing) projection axes — proxy for receipt_density gap
   - pistProxyLabel:   PIST proxy classifier output (if any)
   - pistExactLabel:   PIST exact classifier output (if any)
+
+  Generator fields (for EN9wiki page generation):
+  - operatorTokens:   operator/domain tokens derived from route_hint and rrc_kind
+                      e.g. ["cognitive_load", "exponential_decay"]
+  - invariantsDeclared: declared invariant family from domain_type
+                      e.g. "LAYER_G_ENERGY" or "unknown"
+  - boundaryConds:    binding class / boundary condition family
+                      e.g. "thermodynamic_bind" or "unknown"
+  - templateKey:      which page-generator template applies
+                      e.g. "definition", "master_equation", "gate", "receipt", "hold"
+  - templateParams:   compact parameter string for deterministic rendering
+                      e.g. "route=cognitive_load;shape=CognitiveLoadField"
 -/
 structure FixtureRow where
   equationId        : String
@@ -82,6 +94,12 @@ structure FixtureRow where
   weakAxesCnt       : Nat
   pistProxyLabel    : Option String   -- None when PIST has no prediction
   pistExactLabel    : Option String
+  -- Generator fields
+  operatorTokens    : List String     -- domain/operator token list
+  invariantsDeclared : String         -- declared invariant family or "unknown"
+  boundaryConds     : String          -- binding class or "unknown"
+  templateKey       : String          -- page-generator template key
+  templateParams    : String          -- compact rendering parameter string
   deriving Repr
 
 -- ─────────────────────────────────────────────────────────────────────────────
@@ -155,6 +173,12 @@ structure RrcRow where
   promotion           : Promotion
   warnings            : List String
   receipt             : Receipt
+  -- Generator fields (passed through from FixtureRow)
+  operatorTokens      : List String
+  invariantsDeclared  : String
+  boundaryConds       : String
+  templateKey         : String
+  templateParams      : String
   deriving Repr
 
 def compileRow (row : FixtureRow) : RrcRow :=
@@ -171,7 +195,12 @@ def compileRow (row : FixtureRow) : RrcRow :=
     alignmentScore     := aScore
     promotion          := .notPromoted
     warnings           := warnings
-    receipt         := receipt }
+    receipt            := receipt
+    operatorTokens     := row.operatorTokens
+    invariantsDeclared := row.invariantsDeclared
+    boundaryConds      := row.boundaryConds
+    templateKey        := row.templateKey
+    templateParams     := row.templateParams }
 
 -- ─────────────────────────────────────────────────────────────────────────────
 -- §6  Fixture corpus — 6 canonical rows, one per RRCShape
@@ -194,7 +223,12 @@ def fixtureClf : FixtureRow :=
     rrcKind             := "cognitive_field_receipt"
     weakAxesCnt         := 7
     pistProxyLabel      := some "LogogramProjection"
-    pistExactLabel := some "LogogramProjection" }
+    pistExactLabel      := some "LogogramProjection"
+    operatorTokens      := ["cognitive_load", "exponential_decay", "threshold_reweighting"]
+    invariantsDeclared  := "unknown"
+    boundaryConds       := "unknown"
+    templateKey         := "definition"
+    templateParams      := "route=cognitive_load;shape=CognitiveLoadField" }
 
 /-- SignalShapedRouteCompiler — CANDIDATE, proxy=LogogramProjection (PIST mismatch) -/
 def fixtureSsrc : FixtureRow :=
@@ -205,7 +239,12 @@ def fixtureSsrc : FixtureRow :=
     rrcKind             := "compression_route_prior"
     weakAxesCnt         := 6
     pistProxyLabel      := some "LogogramProjection"
-    pistExactLabel := some "LogogramProjection" }
+    pistExactLabel      := some "LogogramProjection"
+    operatorTokens      := ["compression_route", "signal_shaped"]
+    invariantsDeclared  := "LAYER_A_COMPRESSION"
+    boundaryConds       := "geometric_bind"
+    templateKey         := "master_equation"
+    templateParams      := "route=compression_route;shape=SignalShapedRouteCompiler" }
 
 /-- LogogramProjection — HOLD, proxy=LogogramProjection (exact alignment) -/
 def fixtureLp : FixtureRow :=
@@ -216,7 +255,12 @@ def fixtureLp : FixtureRow :=
     rrcKind             := "logogram_projection"
     weakAxesCnt         := 9
     pistProxyLabel      := some "LogogramProjection"
-    pistExactLabel := some "LogogramProjection" }
+    pistExactLabel      := some "LogogramProjection"
+    operatorTokens      := ["logogram_projection"]
+    invariantsDeclared  := "unknown"
+    boundaryConds       := "unknown"
+    templateKey         := "receipt"
+    templateParams      := "route=logogram_projection;shape=LogogramProjection" }
 
 /-- ProjectableGeometryTopology — HOLD, no PIST prediction (missing) -/
 def fixturePgt : FixtureRow :=
@@ -227,7 +271,12 @@ def fixturePgt : FixtureRow :=
     rrcKind             := "geometry_topology_receipt"
     weakAxesCnt         := 8
     pistProxyLabel      := none
-    pistExactLabel := none }
+    pistExactLabel      := none
+    operatorTokens      := ["geometry_topology", "hubble_tension"]
+    invariantsDeclared  := "LAYER_C_TOPOLOGY"
+    boundaryConds       := "unknown"
+    templateKey         := "hold"
+    templateParams      := "route=geometry_topology;shape=ProjectableGeometryTopology" }
 
 /-- CadForceProbeReceipt — HOLD, no PIST prediction (missing) -/
 def fixtureCad : FixtureRow :=
@@ -238,7 +287,12 @@ def fixtureCad : FixtureRow :=
     rrcKind             := "cad_force_receipt"
     weakAxesCnt         := 8
     pistProxyLabel      := none
-    pistExactLabel := none }
+    pistExactLabel      := none
+    operatorTokens      := ["cad_force", "dag_equilibrium"]
+    invariantsDeclared  := "unknown"
+    boundaryConds       := "physical_bind"
+    templateKey         := "gate"
+    templateParams      := "route=cad_force;shape=CadForceProbeReceipt" }
 
 /-- HoldForUnlawfulOrUnderspecifiedShape — HOLD, no PIST prediction (missing) -/
 def fixtureHold : FixtureRow :=
@@ -249,7 +303,12 @@ def fixtureHold : FixtureRow :=
     rrcKind             := "negative_control"
     weakAxesCnt         := 9
     pistProxyLabel      := none
-    pistExactLabel := none }
+    pistExactLabel      := none
+    operatorTokens      := ["unclassified_equation"]
+    invariantsDeclared  := "unknown"
+    boundaryConds       := "unknown"
+    templateKey         := "hold"
+    templateParams      := "route=unclassified_equation;shape=HoldForUnlawfulOrUnderspecifiedShape" }
 
 def fixtureCorpus : List FixtureRow :=
   [fixtureClf, fixtureSsrc, fixtureLp, fixturePgt, fixtureCad, fixtureHold]
@@ -298,7 +357,12 @@ private def jRrcRow (r : RrcRow) : String :=
   s!"\"alignment_score\":{r.alignmentScore}," ++
   s!"\"promotion\":{jPromotion r.promotion}," ++
   s!"\"warnings\":{jStrList r.warnings}," ++
-  s!"\"receipt_valid\":{jBool r.receipt.valid}}"
+  s!"\"receipt_valid\":{jBool r.receipt.valid}," ++
+  s!"\"operator_tokens\":{jStrList r.operatorTokens}," ++
+  s!"\"invariants_declared\":{jStr r.invariantsDeclared}," ++
+  s!"\"boundary_conds\":{jStr r.boundaryConds}," ++
+  s!"\"template_key\":{jStr r.templateKey}," ++
+  s!"\"template_params\":{jStr r.templateParams}}"
 
 private def jRowList (rs : List RrcRow) : String :=
   "[" ++ String.intercalate "," (rs.map jRrcRow) ++ "]"
@@ -314,17 +378,20 @@ structure EmitResult where
   json          : String
   deriving Repr
 
-def emitFixture : EmitResult :=
+/-- Generic corpus emitter: compile any list of FixtureRows and emit a
-  let rows       := fixtureCorpus.map compileRow
+    labelled JSON receipt.  Used by both `emitFixture` (6 canonical rows)
+    and `emitCorpus278` (full 278-equation corpus in Semantics.RRC.Corpus278). -/
+def emitCorpus (schema : String) (corpus : List FixtureRow) : EmitResult :=
+  let rows       := corpus.map compileRow
   let candidates := rows.filter (·.receipt.valid)
   let summary    :=
     s!"\{\"total\":{rows.length}," ++
     s!"\"passed_alignment\":{candidates.length}," ++
     s!"\"not_promoted\":{rows.length}," ++
-    s!"\"schema\":\"rrc_emit_fixture_v1\"," ++
+    s!"\"schema\":{jStr schema}," ++
     s!"\"claim_boundary\":\"admissibility-and-routing-pass-only\"}"
   let json :=
-    s!"\{\"schema\":\"rrc_emit_fixture_v1\"," ++
+    s!"\{\"schema\":{jStr schema}," ++
     s!"\"claim_boundary\":\"admissibility-and-routing-pass-only\"," ++
     s!"\"summary\":{summary}," ++
     s!"\"rows\":{jRowList rows}}"
@@ -333,6 +400,9 @@ def emitFixture : EmitResult :=
     candidateRows := candidates.length
     json          := json }
 
+def emitFixture : EmitResult :=
+  emitCorpus "rrc_emit_fixture_v1" fixtureCorpus
+
 -- ─────────────────────────────────────────────────────────────────────────────
 -- §9  Eval witnesses
 -- ─────────────────────────────────────────────────────────────────────────────

0-Core-Formalism/lean/Semantics/lakefile.toml

@@ -22,7 +22,9 @@ name = "Semantics"
 # Fast CI target. Only these modules form the "functional Rainbow Raccoon
 # Compiler" proof-of-life:
 #   Semantics.RRC.Emit        — fixture corpus → alignment gate → JSON  (Goal A+)
-#   Semantics.AVMIsa.Emit   — AVM canaries → receipt → RRC projection → JSON (Goal A)
+#   Semantics.AVMIsa.Emit     — AVM canaries → RRC → JSON (Goal A); sole output boundary
+#                               also stamps Semantics.RRC.Corpus278 (278-equation corpus)
+#   Semantics.RRC.Corpus278   — raw 278-equation features (Python-supplied, Lean-gated)
 # Libraries (imported by roots, not roots themselves):
 #   Semantics.AVMIsa.*        — ISA, types, step, run
 #   Semantics.ReceiptCore     — receipt ledger, promotion gates
@@ -30,7 +32,7 @@ name = "Semantics"
 #   Semantics.FixedPoint      — Q16_16, Q0_16 (no Float in compute paths)
 [[lean_lib]]
 name = "Compiler"
-roots = ["Semantics.RRC.Emit", "Semantics.AVMIsa.Emit"]
+roots = ["Semantics.RRC.Emit", "Semantics.AVMIsa.Emit", "Semantics.RRC.Corpus278"]
 
 [[lean_lib]]
 name = "PIST"

4-Infrastructure/shim/build_corpus278.py

@@ -0,0 +1,161 @@
+#!/usr/bin/env python3
+# /// script
+# requires-python = ">=3.10"
+# dependencies = []
+# ///
+"""
+Build Semantics/RRC/Corpus278.lean from rrc_equation_classifier_receipt.json.
+
+Python's role: read raw fields, map to stable IDs, derive generator tokens.
+Lean's role: alignment gate, receipt stamping, all output decisions.
+"""
+from __future__ import annotations
+import hashlib, json, re, sys
+from pathlib import Path
+
+ROOT = Path("/home/allaun/Research Stack")
+RECEIPT_JSON = ROOT / "archive/experimental-shim-probes/rrc_equation_classifier_receipt.json"
+OUT_LEAN = ROOT / "0-Core-Formalism/lean/Semantics/Semantics/RRC/Corpus278.lean"
+
+# ── shape mapping (classifier JSON → Lean RRCShape constructor) ──────────────
+SHAPE_MAP = {
+    "CognitiveLoadField":                   ".cognitiveLoadField",
+    "SignalShapedRouteCompiler":             ".signalShapedRouteCompiler",
+    "ProjectableGeometryTopology":          ".projectableGeometryTopology",
+    "CadForceProbeReceipt":                 ".cadForceProbeReceipt",
+    "LogogramProjection":                   ".logogramProjection",
+    "HoldForUnlawfulOrUnderspecifiedShape": ".holdForUnlawfulOrUnderspecifiedShape",
+}
+
+# ── template_key logic (rrc_kind → template) ─────────────────────────────────
+def template_key(rrc_kind: str, status: str) -> str:
+    if status == "HOLD":
+        return "hold"
+    kind_map = {
+        "cognitive_field_receipt":  "definition",
+        "compression_route_prior":  "master_equation",
+        "geometry_topology_receipt":"definition",
+        "cad_force_receipt":        "gate",
+        "logogram_projection":      "receipt",
+        "negative_control":         "hold",
+    }
+    return kind_map.get(rrc_kind, "definition")
+
+# ── operator token derivation (route_hint + rrc_kind + equation text) ─────────
+def operator_tokens(er: dict) -> list[str]:
+    tokens = []
+    rh = (er.get("route_hint_non_authoritative") or "").strip()
+    rk = (er.get("rrc_kind") or "").strip()
+    if rh and rh != "unclassified_equation":
+        tokens.append(rh)
+    if rk:
+        tokens.append(rk)
+    # Extract simple operator keywords from equation text
+    eq_text = (er.get("equation") or "").lower()
+    for op in ["exp(", "log(", "max(", "min(", "sum(", "integral", "derivative",
+               "laplacian", "nabla", "div(", "curl(", "sigmoid", "softmax",
+               "tanh(", "relu(", "norm(", "dot(", "cross("]:
+        if op in eq_text:
+            tokens.append(op.rstrip("("))
+    return list(dict.fromkeys(tokens))  # deduplicate, preserve order
+
+# ── string escaping for Lean ──────────────────────────────────────────────────
+def lean_str(s: str) -> str:
+    s = s.replace("\\", "\\\\").replace('"', '\\"')
+    return f'"{s}"'
+
+def lean_opt(s: str | None) -> str:
+    if s is None:
+        return "none"
+    return f"some {lean_str(s)}"
+
+def lean_str_list(xs: list[str]) -> str:
+    return "[" + ", ".join(lean_str(x) for x in xs) + "]"
+
+# ── stable equation ID ────────────────────────────────────────────────────────
+def stable_id(raw_id: str) -> str:
+    h = hashlib.sha256(raw_id.encode()).hexdigest()[:16]
+    return f"rrc_eq_{h}"
+
+# ── main ──────────────────────────────────────────────────────────────────────
+def main() -> None:
+    d = json.loads(RECEIPT_JSON.read_text())
+    eqs = d["compiled_equations"]
+    print(f"Loaded {len(eqs)} equations", file=sys.stderr)
+
+    lines: list[str] = []
+    lines.append("-- Semantics.RRC.Corpus278 — AUTO-GENERATED by build_corpus278.py")
+    lines.append("-- DO NOT EDIT BY HAND.  Regenerate with:")
+    lines.append("--   python3 4-Infrastructure/shim/build_corpus278.py")
+    lines.append("--")
+    lines.append("-- Python role: raw feature extraction only.")
+    lines.append("-- Lean role: alignment gate, receipt stamping, all output decisions.")
+    lines.append("--")
+    lines.append("-- Source: archive/experimental-shim-probes/rrc_equation_classifier_receipt.json")
+    lines.append(f"-- Equation count: {len(eqs)}")
+    lines.append("")
+    lines.append("import Semantics.RRC.Emit")
+    lines.append("")
+    lines.append("namespace Semantics.RRC.Corpus278")
+    lines.append("")
+    lines.append("open Semantics.RRC.Emit")
+    lines.append("open Semantics.RRCLogogramProjection")
+    lines.append("open Semantics.ReceiptCore")
+    lines.append("")
+    lines.append("/-- Full 278-equation corpus from rrc_equation_classifier_receipt.json.")
+    lines.append("    Each row carries raw features only; the alignment gate in")
+    lines.append("    Semantics.RRC.Emit.emitCorpus makes all admissibility decisions. -/")
+    lines.append("def corpus278 : List FixtureRow := [")
+
+    row_strs: list[str] = []
+    for eq in eqs:
+        er  = eq["equation_record"]
+        ir  = eq["invariant_receipt"]
+        tw  = eq["type_witness"]
+
+        raw_id   = er["equation_id"]
+        eq_id    = stable_id(raw_id)
+        name     = er["name"]
+        shape_str = ir["shape"]
+        lean_shape = SHAPE_MAP.get(shape_str, ".holdForUnlawfulOrUnderspecifiedShape")
+        status_str = ir["status"]
+        lean_status = ".candidate" if status_str == "CANDIDATE" else ".hold"
+        rrc_kind = er.get("rrc_kind", "")
+        weak_cnt = len(tw.get("missing_or_weak_axes") or [])
+
+        # Generator fields
+        op_tokens    = operator_tokens(er)
+        inv_declared = (er.get("domain_type") or "unknown").strip() or "unknown"
+        bound_conds  = (er.get("bind_class") or "unknown").strip() or "unknown"
+        t_key        = template_key(rrc_kind, status_str)
+        t_params     = f"route={er.get('route_hint_non_authoritative','unclassified_equation') or 'unclassified_equation'};shape={shape_str}"
+
+        row = (
+            f"  {{ equationId          := {lean_str(eq_id)}\n"
+            f"    name                := {lean_str(name)}\n"
+            f"    shape               := {lean_shape}\n"
+            f"    status              := {lean_status}\n"
+            f"    rrcKind             := {lean_str(rrc_kind)}\n"
+            f"    weakAxesCnt         := {weak_cnt}\n"
+            f"    pistProxyLabel      := none\n"
+            f"    pistExactLabel      := none\n"
+            f"    operatorTokens      := {lean_str_list(op_tokens)}\n"
+            f"    invariantsDeclared  := {lean_str(inv_declared)}\n"
+            f"    boundaryConds       := {lean_str(bound_conds)}\n"
+            f"    templateKey         := {lean_str(t_key)}\n"
+            f"    templateParams      := {lean_str(t_params)} }}"
+        )
+        row_strs.append(row)
+
+    lines.append(",\n".join(row_strs))
+    lines.append("]")
+    lines.append("")
+    lines.append("end Semantics.RRC.Corpus278")
+    lines.append("")
+
+    OUT_LEAN.write_text("\n".join(lines))
+    print(f"Wrote {OUT_LEAN}", file=sys.stderr)
+    print(f"Total rows: {len(row_strs)}", file=sys.stderr)
+
+if __name__ == "__main__":
+    main()