Research-Stack/0-Core-Formalism/lean
Brandon Schneider a478af98be feat(rrc): Goal A+ — Semantics.RRC.Emit; fixture corpus → alignment gate → JSON
Semantics/RRC/Emit.lean (new):

Ports the core decision logic of rrc_pist_shape_alignment.py into Lean.
This is the first Lean-only RRC compiler pass replacing shim-space Python.

Schema:
  AlignmentStatus: aligned_exact | aligned_proxy |
                   compatible_structural_projection |
                   alignment_warning | missing_prediction
  scores (integer/100): 100 | 86 | 72 | 35 | 0
  Promotion: always not_promoted at this stage
  RrcRow: {equation_id, name, shape, status, alignmentStatus, alignmentScore,
           promotion, warnings, receipt}

determineAlignment ports determine_alignment verbatim:
  1. no PIST label → missing_prediction
  2. exact label == RRC shape → aligned_exact
  3. proxy label == RRC shape → aligned_proxy
  4. PIST label in structural_labels AND RRC shape is semantic → compatible_structural_projection
  5. else → alignment_warning

Fixture corpus (6 rows, one per RRCShape, from rrc_equation_classifier_receipt.json):
  CognitiveLoadField           CANDIDATE  proxy=LogogramProjection → compatible_structural_projection  score=72
  SignalShapedRouteCompiler    CANDIDATE  proxy=LogogramProjection → compatible_structural_projection  score=72
  LogogramProjection           HOLD       proxy=LogogramProjection → aligned_exact                    score=100
  ProjectableGeometryTopology  HOLD       no PIST label            → missing_prediction               score=0
  CadForceProbeReceipt         HOLD       no PIST label            → missing_prediction               score=0
  HoldForUnlawful...           HOLD       no PIST label            → missing_prediction               score=0

#eval emitFixture.json → valid JSON (python3 -m json.tool passes):
  schema: rrc_emit_fixture_v1
  total: 6, passed_alignment: 3, all not_promoted

This faithfully encodes the current shim state: the PIST classifier has 0%
accuracy against CognitiveLoadField / SignalShapedRouteCompiler because it
predicts LogogramProjection for all rows. The Lean gate correctly classifies
this as compatible_structural_projection (score 72) rather than a hard failure.

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

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
2026-05-26 21:51:45 -05:00
..
conversions/hardware WIP: accumulated changes 2026-05-25 16:24:21 -05:00
external/OTOM WIP: accumulated changes 2026-05-25 16:24:21 -05:00
LeanGPT Remove legacy Python prototypes superseded by Lean formalization 2026-05-19 15:34:17 +00:00
Semantics feat(rrc): Goal A+ — Semantics.RRC.Emit; fixture corpus → alignment gate → JSON 2026-05-26 21:51:45 -05:00
CHAIN_ALL_REVIEW_REPORT.md initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00