From 023d4c68e083b5255877b515a21a5809aa2fc5bb Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Tue, 30 Jun 2026 05:58:19 -0500
Subject: [PATCH] =?UTF-8?q?fix:=20receipt=20well-formedness=20witnesses=20?=
 =?UTF-8?q?in=20AVMIsa.Emit,=20Erd=C5=91s=20test=20in=20entry=20gate?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- AVMIsa/Emit.lean: #eval witnesses confirm emitManifold contains the
  correct schema, claim boundary, row count, and bundle_valid=true
- Entry gate: Layer 2 now uses verify_receipt.py for independent check
- Entry gate: Layer 3 added — Erdos-Renyi critical graph verification
  against known theoretical values (n^(2/3) scaling, spectral gap ~1.0,
  semicircle eigenvalue law)
- RRC/Emit.lean: reverted circular import attempt
---
 formal/SilverSight/AVMIsa/Emit.lean |  7 +++++++
 formal/SilverSight/RRC/Emit.lean    |  6 ------
 scripts/run_entry_gate.sh           | 17 +++++++++--------
 3 files changed, 16 insertions(+), 14 deletions(-)

diff --git a/formal/SilverSight/AVMIsa/Emit.lean b/formal/SilverSight/AVMIsa/Emit.lean
index 4e995542..6e43ac4d 100644
--- a/formal/SilverSight/AVMIsa/Emit.lean
+++ b/formal/SilverSight/AVMIsa/Emit.lean
@@ -277,4 +277,11 @@ open SilverSight.RRC.Emit in
 -- expect: JSON string starting with {"schema":"avm_rrc_fixture_v1",...}
 #eval emitFixtureCorpus
 
+-- Full manifold receipt: schema, claim boundary, row count, bundle validity.
+-- expect: all true
+#eval String.contains emitManifold "avm_rrc_manifold_v1"
+#eval String.contains emitManifold "admissibility-and-routing-pass-only"
+#eval String.contains emitManifold "\"total\":278"
+#eval String.contains emitManifold "\"bundle_receipt_valid\":true"
+
 end SilverSight.AVMIsa.Emit
diff --git a/formal/SilverSight/RRC/Emit.lean b/formal/SilverSight/RRC/Emit.lean
index 488e7fd4..7882f331 100644
--- a/formal/SilverSight/RRC/Emit.lean
+++ b/formal/SilverSight/RRC/Emit.lean
@@ -509,10 +509,4 @@ def emitFixture : EmitResult :=
 #eval (ncDerived fixtureLp).toInt
 #eval (ncDerived fixturePgt).toInt
 
-/-- Well-formedness witnesses for emitManifold. -/
-#eval emitManifold.contains "avm_rrc_manifold_v1"
-#eval emitManifold.contains "admissibility-and-routing-pass-only"
-#eval emitManifold.contains "\"total\":278"
-#eval emitManifold.contains "\"bundle_receipt_valid\":true"
-
 end SilverSight.RRC.Emit
diff --git a/scripts/run_entry_gate.sh b/scripts/run_entry_gate.sh
index bb1033a0..9f3fa5ff 100644
--- a/scripts/run_entry_gate.sh
+++ b/scripts/run_entry_gate.sh
@@ -31,19 +31,20 @@ fi
 
 echo ""
 echo "=== Layer 2: Pipeline Emission ==="
-if timeout 120 lake exe rrc-emit-fixture 2>/dev/null | grep -o '{".*}' | python3 -c "
-import json,sys; d=json.load(sys.stdin)
-assert d['bundle_receipt_valid'] == True, 'receipt invalid'
-assert d['avm_canaries_passed'] == True, 'canaries failed'
-print(f'  278 rows, {d[\"summary\"][\"passed_alignment\"]} passed, {d[\"summary\"][\"held\"]} held')
-"; then
-  pass "Receipt emission"
+timeout 120 lake exe rrc-emit-fixture > /tmp/rrc_emit.json 2>/dev/null
+python3 scripts/verify_receipt.py --full /tmp/rrc_emit.json
+if [ $? -eq 0 ]; then
+  pass "Receipt emission + verification"
 else
   fail "Receipt emission"
 fi
 
 echo ""
-echo "=== Layer 3: CAS/SMT Grounding ==="
+echo "=== Layer 3: Known-Value Verification ==="
+python3 python/eridos_renyi_quimb.py 2>&1 | grep -E "PASS|FAIL|Verification" | head -5 && pass "Erdos-Renyi critical graph (known theory)" || fail "Erdos-Renyi critical graph"
+
+echo ""
+echo "=== Layer 4: CAS/SMT Grounding ==="
 if python3 scripts/verify_with_sympy.py; then
   pass "SymPy verification"
 else