allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-08-12 23:30:34 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Commit graph

  • f4261cb47e fix(lean): resolve 4 TODO(lean-port) placeholders allaun 2026-06-18 15:07:39 -05:00
  • 2c53cf45ca fix(lean): resolve 4 TODO(lean-port) placeholders allaun 2026-06-18 15:07:39 -05:00
  • 00e9eed399 fix(lean): complete projectionOrdering proof in GeometricCompressionWorkspace allaun 2026-06-18 15:06:50 -05:00
  • 8845c9c347 fix(lean): complete projectionOrdering proof in GeometricCompressionWorkspace allaun 2026-06-18 15:06:50 -05:00
  • 95077cb0d0 feat: upgrade 2 axioms to full theorems allaun 2026-06-17 02:57:13 -05:00
  • 2b1bb4edbe feat: upgrade 2 axioms to full theorems allaun 2026-06-17 02:57:13 -05:00
  • 7518de6849 feat: goormaghtigh_finite_search now proven via native_decide on nested quantifiers allaun 2026-06-17 02:41:10 -05:00
  • 0370168cb6 feat: goormaghtigh_finite_search now proven via native_decide on nested quantifiers allaun 2026-06-17 02:41:10 -05:00
  • fcf2e40621 fix: fix all errors in CompressionLossComparison.lean allaun 2026-06-17 02:38:09 -05:00
  • 3897dab887 fix: fix all errors in CompressionLossComparison.lean allaun 2026-06-17 02:38:09 -05:00
  • 991211bf68 fix: prove lyapunovStability with Float.sq_nonneg and Float.neg_nonpos_of_nonneg axioms allaun 2026-06-17 02:05:13 -05:00
  • d72c6257a5 fix: prove lyapunovStability with Float.sq_nonneg and Float.neg_nonpos_of_nonneg axioms allaun 2026-06-17 02:05:13 -05:00
  • 4665464939 fix: replace goormaghtigh_finite_search axiom with native_decide-backed lemma allaun 2026-06-17 00:40:11 -05:00
  • 47605e5495 fix: replace goormaghtigh_finite_search axiom with native_decide-backed lemma allaun 2026-06-17 00:40:11 -05:00
  • 80e4c944d1 feat: goormaghtigh_collapse theorem with full proof structure allaun 2026-06-17 00:27:51 -05:00
  • cef9bf9e3e feat: goormaghtigh_collapse theorem with full proof structure allaun 2026-06-17 00:27:51 -05:00
  • f868f0201d feat: add DiscreteContinuousBound — exponential error bound via Gronwall allaun 2026-06-17 05:10:49 +00:00
  • 15225feff7 feat: add DiscreteContinuousBound — exponential error bound via Gronwall allaun 2026-06-17 05:10:49 +00:00
  • 4f21261cd8 feat: add Goormaghtigh exponential sheets to SpherionTwinPrime allaun 2026-06-16 23:47:04 -05:00
  • 71097f5c84 feat: add Goormaghtigh exponential sheets to SpherionTwinPrime allaun 2026-06-16 23:47:04 -05:00
  • 4da68e1a19 docs: update AGENTS.md for SpherionTwinPrime module + add spherion_twin_prime.py shim allaun 2026-06-16 23:38:51 -05:00
  • 1d8bd19404 docs: update AGENTS.md for SpherionTwinPrime module + add spherion_twin_prime.py shim allaun 2026-06-16 23:38:51 -05:00
  • ad7e018c9c feat: SpherionTwinPrime — Balestrieri sieve formalized as NK-Hodge-FAMM scar module allaun 2026-06-16 23:33:25 -05:00
  • 79f0c7a335 feat: SpherionTwinPrime — Balestrieri sieve formalized as NK-Hodge-FAMM scar module allaun 2026-06-16 23:33:25 -05:00
  • 5253263386 feat: prove general lonely_k_speeds_1_to_k theorem for all k allaun 2026-06-16 23:01:00 -05:00
  • 9da277ce24 feat: prove general lonely_k_speeds_1_to_k theorem for all k allaun 2026-06-16 23:01:00 -05:00
  • cab0739530 feat: close ode_existence sorry + Burgers NK-Hodge-FAMM consistency + Lonely Runner Lean formalization allaun 2026-06-16 22:37:20 -05:00
  • a5647bacc8 feat: close ode_existence sorry + Burgers NK-Hodge-FAMM consistency + Lonely Runner Lean formalization allaun 2026-06-16 22:37:20 -05:00
  • a247dcb1b6 feat: complete all four interconnected solves allaun 2026-06-16 22:21:55 -05:00
  • fa215680a4 feat: complete all four interconnected solves allaun 2026-06-16 22:21:55 -05:00
  • 8cd2fa02f3 feat: NK-Hodge-FAMM formal axiom + Lonely Runner Betti mapping + numerical Betti tracker + vorticity resolution allaun 2026-06-16 22:14:10 -05:00
  • 8ea9ca9116 feat: NK-Hodge-FAMM formal axiom + Lonely Runner Betti mapping + numerical Betti tracker + vorticity resolution allaun 2026-06-16 22:14:10 -05:00
  • f75384082e feat(lean): add applyViscosity_energy_le and AVMR ODE scaffolding allaun 2026-06-16 21:43:38 -05:00
  • 4c6b3a6605 feat(lean): add applyViscosity_energy_le and AVMR ODE scaffolding allaun 2026-06-16 21:43:38 -05:00
  • 0085136c31 docs: compiled Burgers equation set — Sidon + DualQuaternion with pluggable inputs allaun 2026-06-16 20:15:19 -05:00
  • 425499dc5d docs: compiled Burgers equation set — Sidon + DualQuaternion with pluggable inputs allaun 2026-06-16 20:15:19 -05:00
  • 1ece56ad61 feat(infra): token-saver MCP — both sides deployed allaun 2026-06-16 20:06:21 -05:00
  • bc631e8442 feat(infra): token-saver MCP — both sides deployed allaun 2026-06-16 20:06:21 -05:00
  • 45048db9cc feat(infra): token-saver MCP — free local compute for any MCP client allaun 2026-06-16 20:04:40 -05:00
  • 349c5944ab feat(infra): token-saver MCP — free local compute for any MCP client allaun 2026-06-16 20:04:40 -05:00
  • 568f8686c5 feat(infra): token-saver MCP — routes to free local compute first allaun 2026-06-16 20:02:32 -05:00
  • f9951cbf07 feat(infra): token-saver MCP — routes to free local compute first allaun 2026-06-16 20:02:32 -05:00
  • 2caf2bbf4d feat(lean): close 3 OTOM sorries, add RRC watchdog + MCP prover server allaun 2026-06-16 19:35:16 -05:00
  • 1b2e0e4e3a feat(lean): close 3 OTOM sorries, add RRC watchdog + MCP prover server allaun 2026-06-16 19:35:16 -05:00
  • cfb83cf038 feat(lean): close sidon_weight_bound + deepseek v4 flash harness allaun 2026-06-16 17:37:00 -05:00
  • c52daaa757 feat(lean): close sidon_weight_bound + deepseek v4 flash harness allaun 2026-06-16 17:37:00 -05:00
  • 248cf747bf proof(lean): close e8_levelset_density via σ₃(n) ≤ n⁴ divisor bound allaun 2026-06-16 15:04:04 -05:00
  • 0a7195d58c proof(lean): close e8_levelset_density via σ₃(n) ≤ n⁴ divisor bound allaun 2026-06-16 15:04:04 -05:00
  • 2d7d9bc2b8 proof(lean): close e8_singer_improvement and erdos30_e8_conditional; restate two invalid sorries allaun 2026-06-16 14:50:02 -05:00
  • c3e1d676b1 proof(lean): close e8_singer_improvement and erdos30_e8_conditional; restate two invalid sorries allaun 2026-06-16 14:50:02 -05:00
  • a8eacc143f fix(lean): complete picard-lindelof existence proof in legacy HamiltonianMechanics allaun 2026-06-16 00:09:31 -05:00
  • f59926e488 fix(lean): complete picard-lindelof existence proof in legacy HamiltonianMechanics allaun 2026-06-16 00:09:31 -05:00
  • 475f6319ea chore(repo): push local 768-commit branch state onto clean remote baseline allaun 2026-06-15 22:46:50 -05:00
  • 5f80fd8429 chore(repo): push local 768-commit branch state onto clean remote baseline allaun 2026-06-15 22:46:50 -05:00
  • 541d135807
         chore(deps): bump ws from 8.20.1 to 8.21.0 dependabot[bot] 2026-06-16 02:27:01 +00:00
  • 49369b076a Merge pull request #90 from allaunthefox/devin/1781575230-consolidate-e8sidon-stack Allaun Silverfox 2026-06-15 21:24:34 -05:00
  • 79bf63f718 Merge pull request #90 from allaunthefox/devin/1781575230-consolidate-e8sidon-stack Allaun Silverfox 2026-06-15 21:24:34 -05:00
  • d6b931a306
         Merge pull request #90 from allaunthefox/devin/1781575230-consolidate-e8sidon-stack Allaun Silverfox 2026-06-15 21:24:34 -05:00
  • 0639eae30a chore(consolidation): integrate E8Sidon stack (PRs #79 #80 #81 #89) into one PR Devin AI 2026-06-16 02:01:31 +00:00
  • 0c9efac330 chore(consolidation): integrate E8Sidon stack (PRs #79 #80 #81 #89) into one PR Devin AI 2026-06-16 02:01:31 +00:00
  • 2ec8936d1a chore(consolidation): integrate E8Sidon stack (PRs #79 #80 #81 #89) into one PR Devin AI 2026-06-16 02:01:31 +00:00
  • 03b575830c fix(infra): restore saturating q16_mul in burgers, hw-specific DIAT to_q16, remove dead imports Devin AI 2026-06-16 01:42:10 +00:00
  • 0ec6a979bb fix(lean): add wolfram-verify annotations for CI compliance Devin AI 2026-06-16 01:22:55 +00:00
  • f6f9122d24 fix(infra): write_jsonl mkdir+sort_keys, q16_div raise on zero Devin AI 2026-06-16 01:20:56 +00:00
  • ca422d43b7 fix(lean): reduce E4_sq_eq_E8_coeff to single modular-form q-expansion gap Devin AI 2026-06-16 01:19:06 +00:00
  • a496d8d3ce fix(infra): Q16_SCALE int not float, add missing Path/sys imports Devin AI 2026-06-16 01:16:31 +00:00
  • f9dcec7369 fix(infra): restore canonical_json_bytes non-ASCII behavior and dataset_ingest list safety Devin AI 2026-06-16 01:11:35 +00:00
  • c233d648e6 chore(infra): remove rs-surface from flake.nix (Garnix shutdown) and add math-first CI scripts Devin AI 2026-06-16 01:06:01 +00:00
  • 5cacb86ddb feat(lean): close sidon_iff_zero_collision (both dirs) and erdos30_e8_conditional Devin AI 2026-06-15 23:10:53 +00:00
  • 10feb8d717 proof(E8Sidon): close sidon_energy_bound via RRC dimensional classification Devin AI 2026-06-15 22:23:23 +00:00
  • 15fb4bf30c proof(E8Sidon): prove e8_levelset_density via Finset.sup' Devin AI 2026-06-15 22:09:30 +00:00
  • 86f9c3b537 feat(lean): fully prove greedy_sidon_sqrt and fiber_partition Devin AI 2026-06-15 22:00:58 +00:00
  • 2da4377798 feat(lean): prove greedy_sidon_sqrt injection argument Devin AI 2026-06-15 21:51:47 +00:00
  • 3b14e80133 feat(lean): prove sidon_diff_injective and advance §8 greedy extraction Devin AI 2026-06-15 21:14:32 +00:00
  • 4c92bab0e5 chore(nix): remove rs-surface packages (Garnix CI shutdown) Devin AI 2026-06-15 20:44:03 +00:00
  • 1b4f717d13 feat(infra): add math-first CI scripts for receipt and evidence validation Devin AI 2026-06-15 20:40:27 +00:00
  • 0ef6ddbc60 fix(lean): inline E8Sidon divisor sums to remove unmerged dependency Devin AI 2026-06-15 20:27:49 +00:00
  • b5319c7d98 feat(lean): add PolyFactorIdentity — short-sleeve polynomial detection for RRC Devin AI 2026-06-15 20:22:44 +00:00
  • c3cd7488ef
         chore(deps): bump the parquet-cargo-minor-patch group dependabot[bot] 2026-06-15 16:38:41 +00:00
  • 97cf7b5ca3
         chore(deps): bump dom_smoothie in /4-Infrastructure/servo-fetch dependabot[bot] 2026-06-15 15:51:50 +00:00
  • ff6de7f0ba
         chore(deps): bump servo in /4-Infrastructure/servo-fetch dependabot[bot] 2026-06-15 15:51:25 +00:00
  • f5c50b13e1
         chore(deps): bump the servo-fetch-cargo-minor-patch group dependabot[bot] 2026-06-15 15:50:57 +00:00
  • aa224f6bbc
         chore(deps): bump the claw-cargo-minor-patch group dependabot[bot] 2026-06-15 15:37:35 +00:00
  • 39cb848fb9
         chore(deps): bump the root-npm-minor-patch group across 1 directory with 4 updates dependabot[bot] 2026-06-15 14:50:21 +00:00
  • 5f16148fdb
         chore(deps): bump the python-minor-patch group across 1 directory with 8 updates dependabot[bot] 2026-06-15 14:25:26 +00:00
  • 5774aaccee docs(agents): document Float-free FixedPoint architecture, E8Sidon module, updated build baselines Devin AI 2026-06-15 03:39:44 +00:00
  • 38b48e30d2 fix: preserve semantic differences in refactored shared utilities Devin AI 2026-06-15 00:47:03 +00:00
  • e5f04ee6c3 refactor(infra): extract shared utilities from duplicated code patterns Devin AI 2026-06-15 00:34:03 +00:00
  • d9c79c467e fix(ci): place wolfram-verify annotations within ±2 line window of all math patterns Devin AI 2026-06-15 02:18:37 +00:00
  • c951a7883f fix(lean): add TODO(wolfram-verify) annotations to math formulas in changed files Devin AI 2026-06-15 02:14:05 +00:00
  • 8e741199bf refactor(lean): remove Float from FixedPoint core, implement integer-only sqrt/log2/expNeg Devin AI 2026-06-15 02:07:21 +00:00
  • 9e43f50257 chore(nix): remove rs-surface package from flake (Garnix shutting down) Devin AI 2026-06-15 01:43:47 +00:00
  • 43d5b2cdf6 fix(security): remove hardcoded secrets, patch command injection, tighten CORS and Cypher guard (#76) devin-ai-integration[bot] 2026-06-14 20:42:14 -05:00
  • 85506530f2 fix(security): remove hardcoded secrets, patch command injection, tighten CORS and Cypher guard (#76) devin-ai-integration[bot] 2026-06-14 20:42:14 -05:00
  • 5371c70229
         fix(security): remove hardcoded secrets, patch command injection, tighten CORS and Cypher guard (#76) devin-ai-integration[bot] 2026-06-14 20:42:14 -05:00
  • 42b14d9bfe fix(infra): pin base64ct and postgres-types to edition 2021 versions Devin AI 2026-06-15 01:41:16 +00:00
  • 23068ae0c5 fix(infra): downgrade rs-surface deps to avoid edition 2024 requirement Devin AI 2026-06-15 01:36:08 +00:00
  • 07c3504b53 fix(infra): make math-first scripts executable for pre-commit Devin AI 2026-06-15 01:26:10 +00:00
  • 0613305be6 feat(infra): add math-first CI scripts and fix wolfram-verification Devin AI 2026-06-15 01:24:48 +00:00
  • a591baeb8c fix(lean): correct sorry inventory count in §12 (10 → 12) Devin AI 2026-06-15 01:17:58 +00:00