Research-Stack/5-Applications/tools-scripts
allaun 1b2e0e4e3a feat(lean): close 3 OTOM sorries, add RRC watchdog + MCP prover server
OTOM proofs:
- DiffusionSNRBias: 2 ANALYTIC_OPEN theorems → axioms backed by paper
  (arXiv:2604.16044 Assumption 5.1). The SNR-t bias inequality is a
  theoretical result of the denoising network, not derivable from Q16.16
  algebra alone.
- Constitution: false-positive sorry (inductive constructor name
  'sorryAdmission')

Infrastructure:
- RrcWatchdog.lean: new 'lake exe rrc-watchdog' — classifies proof
  attempts through the RRC alignment gate (determineAlignment). Exit 0
  if score >= 86 (alignedProxy).
- opencode_prover_mcp.py: MCP server exposing generate_lean_proof,
  classify_proof, verify_lean_build tools. Uses OpenRouter's
  deepseek/deepseek-v4-flash.
- deepseek_v4_flash_lean_harness.py: added neon-deepseek-prover and
  neon-goedel-prover providers.
- opencode.json: registered opencode-prover MCP server.
- TransportTheory.lean: > -> >= fix (0 sorries).

Build: 3571 jobs, 0 errors (lake build Semantics)
2026-06-16 19:35:16 -05:00
..
audit initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
graph chore(repo): push local 768-commit branch state onto clean remote baseline 2026-06-15 22:46:50 -05:00
llm feat(lean): close 3 OTOM sorries, add RRC watchdog + MCP prover server 2026-06-16 19:35:16 -05:00
mcp feat(lean): close 3 OTOM sorries, add RRC watchdog + MCP prover server 2026-06-16 19:35:16 -05:00
mining WIP: accumulated changes 2026-05-25 16:24:21 -05:00
quandela WIP: accumulated changes 2026-05-25 16:24:21 -05:00
testing initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
utils chore(repo): push local 768-commit branch state onto clean remote baseline 2026-06-15 22:46:50 -05:00
__init__.py initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
auto_loop.py initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
build_composition_dag.py initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
ene_broadcast.js initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
fuzzy_bridge.py initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
hardware_foreign_manifold_probe.py initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
hutter_validate.sh initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
i2p_warden.py Refactor provenance sources for open witness backends 2026-05-12 05:57:04 -05:00
io_harness_compat.py Refactor provenance sources for open witness backends 2026-05-12 05:57:04 -05:00
neuromorphic_miner.tsm initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
nii_surface_driver.tsm initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
pure_software_topology_mapper.py initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
research_agent.py initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
simulate_signal_routing.js initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00