Brandon Schneider
ac4e23dc9b
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
2aac65a9b7
Agent sorry-sprint: close 9 sorrys, fix SSMS sign bug, correct false theorem.
...
Closed with proofs:
- CostEffectiveVerification.manifoldGroupsOntologicallyDifferentSystems:
full proof using obtain + simp + exact (added cross-domain diversity hypothesis)
- FixedPointBridge.q0ToQ16_zero: native_decide (finite UInt16→UInt32 computation)
- FixedPointBridge.q0ToQ16_one: corrected false claim (= Q16_16.infinity, not .one),
then native_decide
- WaveformTeleport.constantWaveformAtFixedPoint_base: corrected false claim
(value is 65535, not 0), native_decide
- GPUVerificationMetaprobe: 4 new lemmas fully proved
- gpuVerif_foldl_add_assoc (induction)
- gpuVerif_execBatch_length (simp)
- gpuVerif_foldl_totalVerified (induction)
- verificationStats_valid (simp + exact)
- surface_preservesTotalVerified (simp + exact)
- DiffusionSNRBias.hGammaSq: gamma_t² ≤ 1 via nlinarith + Int.ediv_le_ediv
Bug fixes:
- SSMS.mlgruStep: fixed sign error — oneMf was computing fT − 1 instead of 1 − fT
(doc comment said 1−fT but code did fT−1). This fixes the MLGRU recurrence
formula to match the documented hₜ = f·h + (1−f)·c.
Theorem corrections:
- DiffusionSNRBias.snrBoundedByModelParams: original claim γ·s ≤ γ²·s was
mathematically false for γ < 1, s > 0. Corrected to γ²·s ≤ γ·s with
added signalNorm.raw ≥ 0 hypothesis.
- MMRFAMMUnification.total_causal_cost_invariant_target: added equal-size
hypothesis h_eq (was false for unequal sizes).
Improved TODOs with exact blockers in FixedPointBridge (8 remaining), QFactor,
SSMS, HyperbolicStateSurface, MMRFAMMUnification.
Added Q16_16.add_pos_of_pos lemma (sorry — needs UInt32 automation).
lake build: 3539 jobs, exit 0.
Generated with [Devin](https://cli.devin.ai/docs )
Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
2026-05-18 23:34:57 -05:00
Brandon Schneider
9b1721eea6
integrate infrastructure config, axiom cleanup, and documentation updates
...
- cupfox-config.nix: add Open WebUI container with chat.researchstack.info proxy,
gather-metrics service/timer, rclone, and tmpfiles for persistent storage
- Lean semantics: reduce axiom count from 109 to 18 across 10 files;
FixedPoint now 0 axioms, 0 sorries with 12 theorems
- Documentation: update AGENTS.md with current axiom/sorry counts and
FixedPoint status; refine bind signature
- Add topology scripts, CGA/FAMM/GeneticOptimizer/MMRFAMM Lean modules,
devcontainer config, MEMORY.md, and Modelfile
2026-05-17 12:03:19 -05:00
Brandon Schneider
4eee4a07f6
initial: sovereign research stack (consolidated, weightless, and lfs-optimized)
2026-05-04 18:11:36 -05:00
