mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
bdc98e2a0e
Ports the motif scoring surface from pist_trace_classify_mcp.py (lines 136–149)
into a provable Lean module:
score = frequency / max(library_size, 1) + (0.3 if tactic_family matches)
New module: Semantics.PIST.Motif (201 lines)
§1 familyMatchBonus constant (ofRatio 3 10 = 19660 raw)
§2 MotifInputs, baseScore, motifScore
§3 MotifCandidate record, mkCandidate constructor
§4 rankMotifs / topKMotifs (mergeSort desc, motifId tie-break)
§5 8 executable #eval witnesses with -- expect: annotations
§6 6 proved invariants:
motifScore_bonus_pos (decide)
motifScore_match_ge_base_witness (decide, concrete)
motifScore_zero_freq_base (simp)
motifScore_zero_freq_no_match (simp)
motifScore_zero_freq_match_witness (decide, concrete)
rankMotifs_match_beats_no_match (native_decide — mergeSort sort witness)
Full workspace build: 3570 jobs, 0 errors.
pist_trace_classify_mcp.py PARTIAL BOUNDARY updated: motif score + rank order
now explicitly point to Semantics.PIST.Motif as authoritative.
Generated with [Devin](https://cli.devin.ai/docs)
Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
|
||
|---|---|---|
| .. | ||
| conversions/hardware | ||
| external/OTOM | ||
| LeanGPT | ||
| Semantics | ||
| CHAIN_ALL_REVIEW_REPORT.md | ||