902191cfbb
feat(lean): NBody fixes and new exploration modules
...
- ExtensionScaffold.Physics.NBody: migrate remaining Q16_16 calls to
FixedPoint.Q16_16; simplify quantumErasureAffectsWhichPath proof;
fix solveSheetSpeedup match handling. Builds with 1 known sorry at
verlet_preserves_energy_approximate.
- Semantics.CompleteInteractionGraph: complete directed graph / every-point-
touches-every-point exploration module (builds with 1 sorry).
- Semantics.GraphRank: graph rank exploration module (builds with 1 sorry).
Build: 3315 jobs NBody, 3303 jobs GraphRank, 3297 jobs CompleteInteractionGraph, 0 errors
2026-06-21 01:04:19 -05:00
e370f83eb8
feat(infra): parallel Gremlin edge loader; graph load complete
...
- Optimize load_dependency_graph.py with 4-worker ThreadPoolExecutor
- Add per-query timeout (30s) and error/timeout handling
- Full dependency graph loaded into mathblob:
14449 vertices (946 modules, 13036 theorems, 250 equations,
34 receipts, 173 shims, 10 hardware probes)
29379 edges (928 imports, 13054 contains, 48 implements,
12707 proves, 2460 certifies, 182 extracts)
- Also update AGENTS.md docs and NBody/ErdosRenyiPipeline/
HachimojiManifoldAxiom/ImaginarySemanticTime lean WIP
2026-06-20 19:57:29 -05:00
558431fc45
feat(lean,infra): Corpus278→250 rename + SLOS-calibrated braid defaults
...
- Renamed Corpus278/Matrices278 to Corpus250/Matrices250 across all
Lean modules, Python shims, JSON schemas, and documentation
- Applied SLOS-calibrated defaults to braid_search.py:
bracket_cost base=8x/16x, crossing_penalty gap_reward=0.01
- Synced same defaults to research-compute-fabric submodule
- Updated Burgers 0D defaults: nu=0.9995, advection=0.075
- Fixed 278→250 refs in pist_predictions JSON (claim_boundary, total)
- Fixed stale schema refs in .devin/skills/lean-proof/SKILL.md
- Updated AGENTS.md build baselines to post-clean counts (3314 jobs)
- Updated lake-manifest.json sparkle rev to match lakefile.toml
- Fixed Q16_16 signed conversion bug in qaoa_adapter tunable costs
- NBody.lean: pre-existing dirty changes (introN failures, NOT our work)
Build: 3314 jobs, 0 errors (lake build Compiler)
2026-06-18 22:16:52 -05:00
00e9eed399
fix(lean): complete projectionOrdering proof in GeometricCompressionWorkspace
...
Replace the TODO(lean-port) sorry with a complete proof of the
projectionOrdering theorem: for positive SourceValue pairs s1 < s2
with s2 ≤ maxExpected, projectToCoding preserves strict ordering
of the Q0_64 values.
The proof uses Nat-only arithmetic (no Float) and handles two cases:
- a2 < d: both values fit in Q0_64 range, ordering follows from
monotonicity of integer division
- a2 = d: a2*s/d = s clamped to q0_64MaxRaw; a1*s/d < q0_64MaxRaw
via the key inequality (d-1)*s < (s-1)*d
Build: 8598 jobs, 0 errors (lake build)
2026-06-18 15:06:50 -05:00
Brandon Schneider
073a70eb86
WIP: accumulated changes
2026-05-25 16:24:21 -05:00
Brandon Schneider
fd863af6fd
Expand devcontainer with full Python stack, add MCP servers (Notion/AWS), strengthen Lean theorems
...
- .devcontainer/Dockerfile: add PostgreSQL client libs, OpenSSL/libffi headers, gfortran/BLAS for scipy, rclone; install full Python dependency set (boto3, psycopg2-binary, fastapi, uvicorn, notion-client, httpx, pytest, numpy, scipy, etc.) in uv-managed venv; add rclone S3 gateway init script as ENTRYPOINT
- .devcontainer/devcontainer.json: switch from build to pre-built image (localhost/research
2026-05-19 01:52:14 -05:00
Brandon Schneider
5f88abf618
initial: sovereign research stack (consolidated, weightless, and lfs-optimized)
2026-05-04 18:11:36 -05:00
