Research-Stack/0-Core-Formalism/lean/Semantics
Brandon Schneider 0a70ba80fe docs(agents): post-interaction workflow + Compiler surface update
Root AGENTS.md:
- Add §Post-Interaction Workflow: mandatory steps after every agent session
  that changes code — update AGENTS.md, verify build, commit, check tree
  cleanliness. Explicit trigger conditions (file edits, lake build, arch
  decisions, new TODO/quarantine). Does NOT trigger for read-only sessions.
- Update AVM glossary entry: ISA is live; AVM is sole output boundary for
  RRC receipts; describe AVMIsa.Emit / RRC.Emit / RRC.Corpus278 roles.

Semantics/AGENTS.md:
- Replace stale Blessed Compiler Surface section with current state (commit
  3f923e2c, 3567 jobs, 3 roots: RRC.Emit, AVMIsa.Emit, RRC.Corpus278)
- Document AVM-sole-output-boundary architecture with ASCII data-flow diagram
- Document 278-corpus current state: (278, 0, 278) — correct and honest
- Document 5 generator fields for EN9wiki page generation
- Document build_corpus278.py regeneration command and Python/Lean role split

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

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
2026-05-26 22:25:26 -05:00
..
.github/workflows initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
Ancillary Track remaining source and documentation inventory 2026-05-11 22:18:31 -05:00
blackboard initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
build-static initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
Core Address fixed-point review findings 2026-05-05 21:26:18 -05:00
ExtensionScaffold WIP: accumulated changes 2026-05-25 16:24:21 -05:00
legacy initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
OpenWormKernelFieldBenchmark initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
Quarantine initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
scripts initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
Semantics feat(rrc): 278-equation corpus — AVM sole output boundary, RRC classifier feeds it 2026-05-26 22:23:56 -05:00
.gitignore initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
AdaptivePrecision.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
AdaptivePrecision.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
AdaptivePrecision.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
AGENTS.md docs(agents): post-interaction workflow + Compiler surface update 2026-05-26 22:25:26 -05:00
BindServer.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
BindServer.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
BindServer.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
Biology.lean Semantics: modularize quaternion, resolve circular dependencies, and eliminate float operations 2026-05-19 14:29:41 +00:00
CombinatorialPrecision.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
CombinatorialPrecision.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
CombinatorialPrecision.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
debug_eval.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
EQUATIONS_EXTRACTION.md initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
EvolutionaryTransfold.lean Track compiling Lean source slice 2026-05-11 22:14:31 -05:00
EvolutionaryTransfoldExpanded.lean Track compiling Lean source slice 2026-05-11 22:14:31 -05:00
ExtensionScaffold.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
EXTERNAL_REVIEW_REQUIREMENTS.md initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
ExtremeParameterTestEval.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
ExtremeParameterTestEval.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
ExtremeParameterTestEval.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
ExtremeParameterTestEval_output.txt initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
F01_Q16_16_FixedPoint.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
F01_Q16_16_FixedPoint.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
FPGAExtraction.lean Expand devcontainer with full Python stack, add MCP servers (Notion/AWS), strengthen Lean theorems 2026-05-19 01:52:14 -05:00
FPGAExtraction.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
FPGAExtraction.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
GenerateLUTMain.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
GenerateSparklePhiS3C.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
GenerateSparklePhiS3C.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
GenerateSparklePhiS3C.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
lake-manifest.json Consolidate research stack updates 2026-05-05 21:09:48 -05:00
lakefile.toml feat(rrc): 278-equation corpus — AVM sole output boundary, RRC classifier feeds it 2026-05-26 22:23:56 -05:00
lean-toolchain Consolidate research stack updates 2026-05-05 21:09:48 -05:00
Main.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
Main.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
Main.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
MANIFOLD_NETWORKING_V0.1_ACCEPTANCE.md initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
ManifoldCompressionAgnostic.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
ManifoldCompressionAgnostic.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
ManifoldCompressionAgnostic.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
MATH_MODEL_MAP.tsv initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
MetadataOverheadBudget.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
MetadataOverheadBudget.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
MetadataOverheadBudget.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
MetaManifoldLanguageMerging.lean Consolidate research stack updates 2026-05-05 21:09:48 -05:00
MetaManifoldLanguageMerging.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
MetaManifoldLanguageMerging.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
MinimumNeuralCompression.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
MinimumNeuralCompression.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
MinimumNeuralCompression.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
MOIMBenchmarkMain.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
MOIMBenchmarkMain.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
MOIMBenchmarkMain.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
NominalParameterTestEval.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
NominalParameterTestEval.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
NominalParameterTestEval.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
OpenWormBenchmark.lean Expand devcontainer with full Python stack, add MCP servers (Notion/AWS), strengthen Lean theorems 2026-05-19 01:52:14 -05:00
OpenWormBenchmark.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
OpenWormBenchmark.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
OriginProtocol.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
OriginProtocol.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
OriginProtocol.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
PHASE_COMPLETION_SUMMARY.md initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
PUBLIC_BENCHMARK_RELEASE.md initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
PUBLIC_THEORY_RELEASE.md initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
PurifyMain.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
QuizTest.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
QuizTest.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
QuizTest.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
README.md initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
SearchServer.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
SearchServer.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
SearchServer.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
Semantics.lean fix(lean): full lake build green — quarantine 29 probe stubs + 3 Lean 4.30 fixes 2026-05-26 21:59:16 -05:00
Semantics.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
Semantics.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
SIGNAL_ANALYSIS_GENETIC_IMPLICATIONS.md Track compiling Lean source slice 2026-05-11 22:14:31 -05:00
TangNano9KEmitter.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
TangNano9KEmitter.lean.pist collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
TangNano9KEmitter.lean.pist.meta collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
test.lean initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
TestFintype.lean Expand devcontainer with full Python stack, add MCP servers (Notion/AWS), strengthen Lean theorems 2026-05-19 01:52:14 -05:00
TRANSFOLD_COMPARISON.md Track compiling Lean source slice 2026-05-11 22:14:31 -05:00
TransfoldEquation.lean Track compiling Lean source slice 2026-05-11 22:14:31 -05:00
TransfoldEquationBaseline.lean Track compiling Lean source slice 2026-05-11 22:14:31 -05:00
UrbanAdaptationTransfold.lean Track compiling Lean source slice 2026-05-11 22:14:31 -05:00

Semantics