fix: receipt well-formedness witnesses in AVMIsa.Emit, Erdős test in entry gate

- 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
This commit is contained in:
allaun 2026-06-30 05:58:19 -05:00
parent 8e927d8311
commit 023d4c68e0
3 changed files with 16 additions and 14 deletions

View file

@ -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

View file

@ -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

View file

@ -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