mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
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>
This commit is contained in:
Brandon Schneider
parent
95e6cef58d
commit
3f923e2c13
5 changed files with 4016 additions and 95 deletions
|
|
@ -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
|
||||
|
|
|
|||
3639
0-Core-Formalism/lean/Semantics/Semantics/RRC/Corpus278.lean
Normal file
3639
0-Core-Formalism/lean/Semantics/Semantics/RRC/Corpus278.lean
Normal file
File diff suppressed because it is too large
Load diff
|
|
@ -64,24 +64,42 @@ inductive Promotion where
|
|||
|
||||
Fields match the invariant_receipt + equation_record structure from
|
||||
rrc_equation_classifier_receipt.json:
|
||||
- equationId: "rrc_eq_<hex>" stable object identifier
|
||||
- name: human-readable equation name
|
||||
- shape: RRC routing shape (from RRCLogogramProjection.RRCShape)
|
||||
- status: witness status (candidate or hold)
|
||||
- rrcKind: classifier receipt kind tag
|
||||
- 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)
|
||||
- equationId: "rrc_eq_<hex>" stable object identifier
|
||||
- name: human-readable equation name
|
||||
- shape: RRC routing shape (from RRCLogogramProjection.RRCShape)
|
||||
- status: witness status (candidate or hold)
|
||||
- rrcKind: classifier receipt kind tag
|
||||
- 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
|
||||
name : String
|
||||
shape : RRCShape
|
||||
status : WitnessStatus
|
||||
rrcKind : String
|
||||
weakAxesCnt : Nat
|
||||
pistProxyLabel : Option String -- None when PIST has no prediction
|
||||
pistExactLabel : Option String
|
||||
equationId : String
|
||||
name : String
|
||||
shape : RRCShape
|
||||
status : WitnessStatus
|
||||
rrcKind : String
|
||||
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
|
||||
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
|
|
@ -146,15 +164,21 @@ def alignmentWarnings (status : AlignmentStatus) : List String :=
|
|||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
|
||||
structure RrcRow where
|
||||
equationId : String
|
||||
name : String
|
||||
shape : RRCShape
|
||||
status : WitnessStatus
|
||||
alignmentStatus : AlignmentStatus
|
||||
alignmentScore : Nat -- integer, denominator 100
|
||||
promotion : Promotion
|
||||
warnings : List String
|
||||
receipt : Receipt
|
||||
equationId : String
|
||||
name : String
|
||||
shape : RRCShape
|
||||
status : WitnessStatus
|
||||
alignmentStatus : AlignmentStatus
|
||||
alignmentScore : Nat -- integer, denominator 100
|
||||
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 :=
|
||||
|
|
@ -163,15 +187,20 @@ def compileRow (row : FixtureRow) : RrcRow :=
|
|||
let warnings := alignmentWarnings aStatus
|
||||
let passed := aStatus != .missingPrediction && aStatus != .alignmentWarning
|
||||
let receipt := leanBuildReceipt row.equationId passed
|
||||
{ equationId := row.equationId
|
||||
name := row.name
|
||||
shape := row.shape
|
||||
status := row.status
|
||||
alignmentStatus := aStatus
|
||||
alignmentScore := aScore
|
||||
promotion := .notPromoted
|
||||
warnings := warnings
|
||||
receipt := receipt }
|
||||
{ equationId := row.equationId
|
||||
name := row.name
|
||||
shape := row.shape
|
||||
status := row.status
|
||||
alignmentStatus := aStatus
|
||||
alignmentScore := aScore
|
||||
promotion := .notPromoted
|
||||
warnings := warnings
|
||||
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
|
||||
|
|
@ -187,69 +216,99 @@ def compileRow (row : FixtureRow) : RrcRow :=
|
|||
|
||||
/-- CognitiveLoadField — CANDIDATE, proxy=LogogramProjection (PIST mismatch) -/
|
||||
def fixtureClf : FixtureRow :=
|
||||
{ equationId := "rrc_eq_86ccde7bfd669b77"
|
||||
name := "bandwidth_adjusted_threshold"
|
||||
shape := .cognitiveLoadField
|
||||
status := .candidate
|
||||
rrcKind := "cognitive_field_receipt"
|
||||
weakAxesCnt := 7
|
||||
pistProxyLabel := some "LogogramProjection"
|
||||
pistExactLabel := some "LogogramProjection" }
|
||||
{ equationId := "rrc_eq_86ccde7bfd669b77"
|
||||
name := "bandwidth_adjusted_threshold"
|
||||
shape := .cognitiveLoadField
|
||||
status := .candidate
|
||||
rrcKind := "cognitive_field_receipt"
|
||||
weakAxesCnt := 7
|
||||
pistProxyLabel := 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 :=
|
||||
{ equationId := "rrc_eq_ac1a7a22801b7d77"
|
||||
name := "core_equations"
|
||||
shape := .signalShapedRouteCompiler
|
||||
status := .candidate
|
||||
rrcKind := "compression_route_prior"
|
||||
weakAxesCnt := 6
|
||||
pistProxyLabel := some "LogogramProjection"
|
||||
pistExactLabel := some "LogogramProjection" }
|
||||
{ equationId := "rrc_eq_ac1a7a22801b7d77"
|
||||
name := "core_equations"
|
||||
shape := .signalShapedRouteCompiler
|
||||
status := .candidate
|
||||
rrcKind := "compression_route_prior"
|
||||
weakAxesCnt := 6
|
||||
pistProxyLabel := 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 :=
|
||||
{ equationId := "rrc_eq_4c87c96f612f6100"
|
||||
name := "Stamp_Code"
|
||||
shape := .logogramProjection
|
||||
status := .hold
|
||||
rrcKind := "logogram_projection"
|
||||
weakAxesCnt := 9
|
||||
pistProxyLabel := some "LogogramProjection"
|
||||
pistExactLabel := some "LogogramProjection" }
|
||||
{ equationId := "rrc_eq_4c87c96f612f6100"
|
||||
name := "Stamp_Code"
|
||||
shape := .logogramProjection
|
||||
status := .hold
|
||||
rrcKind := "logogram_projection"
|
||||
weakAxesCnt := 9
|
||||
pistProxyLabel := 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 :=
|
||||
{ equationId := "rrc_eq_5193efd26258bc51"
|
||||
name := "UQGET_Hubble_Tension"
|
||||
shape := .projectableGeometryTopology
|
||||
status := .hold
|
||||
rrcKind := "geometry_topology_receipt"
|
||||
weakAxesCnt := 8
|
||||
pistProxyLabel := none
|
||||
pistExactLabel := none }
|
||||
{ equationId := "rrc_eq_5193efd26258bc51"
|
||||
name := "UQGET_Hubble_Tension"
|
||||
shape := .projectableGeometryTopology
|
||||
status := .hold
|
||||
rrcKind := "geometry_topology_receipt"
|
||||
weakAxesCnt := 8
|
||||
pistProxyLabel := 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 :=
|
||||
{ equationId := "rrc_eq_7076f5bdea119531"
|
||||
name := "DAG_Force_Equilibrium"
|
||||
shape := .cadForceProbeReceipt
|
||||
status := .hold
|
||||
rrcKind := "cad_force_receipt"
|
||||
weakAxesCnt := 8
|
||||
pistProxyLabel := none
|
||||
pistExactLabel := none }
|
||||
{ equationId := "rrc_eq_7076f5bdea119531"
|
||||
name := "DAG_Force_Equilibrium"
|
||||
shape := .cadForceProbeReceipt
|
||||
status := .hold
|
||||
rrcKind := "cad_force_receipt"
|
||||
weakAxesCnt := 8
|
||||
pistProxyLabel := 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 :=
|
||||
{ equationId := "rrc_eq_6d33c14a88eb0a12"
|
||||
name := "LASSO_MOGAT_GAT_Propagation"
|
||||
shape := .holdForUnlawfulOrUnderspecifiedShape
|
||||
status := .hold
|
||||
rrcKind := "negative_control"
|
||||
weakAxesCnt := 9
|
||||
pistProxyLabel := none
|
||||
pistExactLabel := none }
|
||||
{ equationId := "rrc_eq_6d33c14a88eb0a12"
|
||||
name := "LASSO_MOGAT_GAT_Propagation"
|
||||
shape := .holdForUnlawfulOrUnderspecifiedShape
|
||||
status := .hold
|
||||
rrcKind := "negative_control"
|
||||
weakAxesCnt := 9
|
||||
pistProxyLabel := 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 :=
|
||||
let rows := fixtureCorpus.map compileRow
|
||||
/-- Generic corpus emitter: compile any list of FixtureRows and emit a
|
||||
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
|
||||
-- ─────────────────────────────────────────────────────────────────────────────
|
||||
|
|
|
|||
|
|
@ -21,16 +21,18 @@ name = "Semantics"
|
|||
# ── Compiler: blessed RRC compiler surface ────────────────────────────────────
|
||||
# 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.RRC.Emit — fixture corpus → alignment gate → 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
|
||||
# Semantics.AVMIsa.* — ISA, types, step, run
|
||||
# Semantics.ReceiptCore — receipt ledger, promotion gates
|
||||
# Semantics.RRCLogogramProjection — projection/merge/lane theorems
|
||||
# Semantics.FixedPoint — Q16_16, Q0_16 (no Float in compute paths)
|
||||
# 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"
|
||||
|
|
|
|||
161
4-Infrastructure/shim/build_corpus278.py
Normal file
161
4-Infrastructure/shim/build_corpus278.py
Normal file
|
|
@ -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()
|
||||
Loading…
Add table
Reference in a new issue