opencode rejects the mcpServers key in ~/.config/opencode/opencode.jsonc.
Remove it from global config and add consensus as a remote MCP server in
the project-level opencode.json under the correct mcp key.
Drop the pist-trace-classify server (and any lingering aws block) from
.mcp.json and opencode.json. It depended on RDS/AWS env vars. Already
removed from ~/.kimi/mcp.json as well.
Update Credential-System.md and RDS-Rust-Workspace.md to describe a
provider-neutral PostgreSQL backend instead of AWS RDS. Replace IAM
auth examples with standard libpq env-var connection. Remove the
~/.aws/ file layout and AWS hostname defaults.
- Corrected type mismatches in SOSCertificate and SemialgebraicSet constraints, ensuring polynomial components are correctly typed as ((σ → ℝ) → ℝ).
- Resolved block comment syntax errors (/-- unexpected token) by converting section commentaries to standard block comments.
- Decomposed foldl list inductions into generalized induction helper lemmas foldl_nonneg and foldl_weighted_nonneg to resolve type mismatches.
- Unfolded let bindings in softplus_derivative_bounded via dsimp only to allow linarith to successfully find contradictions.
- Updated CITATION.cff, GEMINI.md, and local AGENTS.md files with baseline records.
Build: 3314 jobs, 0 errors (lake build Compiler)
- Unfolded decideGate and used dsimp only to eliminate local let/have bindings in stableSignal_implies_coherent and noCfd_avoids_continuum.
- Used split_ifs to automatically resolve contradictory branches and extracted correct boolean/decidable subgoals.
- Unfolded tensegrityCoherent and applied decide_eq_true_iff.mp to resolve the tensegrity_implies_braid_coherence theorem.
- Updated 0-Core-Formalism/lean/Semantics/AGENTS.md to reflect the completed tasks.
Build: 8332 jobs, 0 errors (lake build)
Created the new TopologicalBraidAdapter.lean module, connecting AnyonBraid, SLUG3State, UnitQuaternion, DualQuaternion, SemanticMassPoint, and TopoPhinVector types. Fixed trailing comma let-expression syntax for eval statements and verified correctness of Fibonacci Hilbert space dimensions.
Build: 8332 jobs, 0 errors (lake build)
Added theoretical entropy power laws, physical target scales, RTX 4070 SUPER hardware limits (VRAM & time complexity), and scaling recommendations to the ContextStream blocks in AGENTS.md and GEMINI.md.
Build: 3314 jobs, 0 errors (lake build Compiler)
- Redirected the default RDS_HOST/PGHOST database connection default
to neon-64gb (100.92.88.64) across all Python shims, shell wrappers,
and Rust probes.
- Cleaned up local defaults in rds_connect.py, sync_wiki_to_rds.py,
dataset_ingest_rds.py, batch_embed_artifacts.py, db.rs, cache-offload.sh,
db-consolidate.sh, backup.sh, and ene-api-wrapper.sh.
Build: 0 jobs, 0 errors (lake build)
- Replaced database-1-instance-1.cghu8yqogqwo.us-east-1.rds.amazonaws.com
with 'localhost' as default.
- Removed AWS IAM generate-db-auth-token CLI subprocessing and boto3
token generation blocks from rds_connect.py, ingest_flexure_joints.py,
pist_route_repair.py, and ene-api-wrapper.sh.
- Purged AWS DEFAULT_REGION and AWS_REGION configurations where applicable.
- Updated Rust rds_probe to use standard PG environment variables.
Build: 0 jobs, 0 errors (lake build)
Implemented rrc_bosonic_db_buffer.py containing AsyncDatabaseBuffer
which queues, batches, and flushes PostgreSQL inserts for bosonic tensor
network receipts and metrics. Documented both rrc_bosonic_tensor_gpu.py
and rrc_bosonic_db_buffer.py in 4-Infrastructure/AGENTS.md.
Build: 0 jobs, 0 errors (lake build)
Encodes each Burgers representation as a node connected by proven
isomorphisms from the codebase. Continuous-time quantum walk e^{-iAt}
on the adjacency matrix converges to eigenvector centrality; the
0D DualQuat Braid is confirmed as the universal hub (#1 in all three
rankings: centrality, quantum walk probability, and degree).
Build: N/A (Python shim, no Lean files touched)
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)
Key change: goormaghtigh_finite_search is no longer an axiom. Replaced
with native_decide proof using nested ∀ x ∈ Icc, ∀ m ∈ Icc, ... which
is fast (avoids constructing a 958K-element Finset).
Also added:
- repunit_mod_pred lemma: R(x,m) ≡ m (mod x-1)
- goormaghtigh_collision_mod lemma: cross-residue sieve
- Theorem now includes 4 ordered forms (adding (2,5,5,3) and
(2,13,90,3) for completeness)
Only goormaghtigh_boundedness remains as axiom.
Build: 8317 jobs, 0 errors.
repunit_collisions_unique proven via native_decide on a 979-element Finset:
only 2 repunit values (31 and 8191) have multiplicity > 1 in [2,90]×[3,13].
goormaghtigh_finite_search remains an axiom (the full finite search
conclusion requires the specific collision pairs, not just their count).
Build: 8317 jobs, 0 errors.
Theorem: For x>1, y>1, m>2, n>2, (x,m)≠(y,n),
if R(x,m) = R(y,n) then (x,m,y,n) = (5,3,2,5) or (90,3,2,13).
Two axioms remain:
- goormaghtigh_finite_search: 979 repunit pairs enumerated in Python,
only 2 collisions (31 and 8191) — verified externally
- goormaghtigh_boundedness: the 16D→0D projection bounds x,y≤90, m,n≤13
(equivalent to the full conjecture — this is the open number theory)
Goormaghtigh's requirement m,n>2 ensures no trivial solutions like
R(6,2)=7=R(2,3). The (x,m)≠(y,n) condition excludes identity solutions.
Build: 8317 jobs, 0 errors.
AGENTS.md: added SpherionTwinPrime architecture section, updated Burgers energy dissipation to parametric form.
spherion_twin_prime.py (20KB): priority-queue walk with polarity energy tuning.
Build: 8598 jobs, 0 errors.
General theorem: for speeds [1,2,...,k] at t = 1/(k+1), the origin
is uncovered. Proves the Lonely Runner Conjecture for the infinite
family of consecutive integer speeds. Subsumes k=2 and k=3 lemmas.
A. ode_existence (AVMRTheorems.lean) — proven via
ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt.
vectorFieldℝ is affine linear (ContDiff ℝ 1 via fun_prop), satisfying
Picard-Lindelöf. Zero sorries remaining in file.
B. BurgersNKConsistency.lean (167 lines) — 4 theorems mapping Burgers
theorems to NK-Hodge-FAMM conditions. Main theorem: energy bounded
for all n via applyViscosity_energy_le induction.
C. LonelyRunner.lean (311 lines) — 10 sections: circle distance, runner
positions, coverage density, scar region, scar complex, beta0.
Proved lonely_k2_speeds_1_2 and lonely_k3_speeds_1_2_3.
Betti bridge to NK-Hodge-FAMM framework.
All builds: 8598/8313 jobs, 0 errors.
Shows the full architecture as a self-contained equation spec:
- DualQuaternion = 8 components (Sidon-labeled 2^0..2^7)
- BurgersState -> DualQuaternion mapping (pluggable per PDE variant)
- Viscosity = scalar multiplication, advection = group rotation
- 4 theorems all native_decide, kernel-verified
- How to add a new PDE variant in ~24 lines, inheriting all proofs
8 tools, all routing to free compute first:
verify_build, classify_proof, compile_check, linter_check,
generate_proof (neon → paid fallback), format_code, doc_lookup, health
Any MCP-compatible agent (Claude Code, OpenCode, Cursor) can call
these tools and avoid burning API tokens on compilation/verification.
- e8_singer_improvement: proven via Singer set as direct witness; (119/120)^k ≤ 1 by
pow_le_one₀, bound follows from mul_le_of_le_one_right.
- erdos30_e8_conditional: proven via interval_sidon_exists (Singer's theorem bridge);
C=1/4, Nat.sqrt ↔ Real.sqrt bridge via nlinarith on squared terms.
- sidon_weight_bound: restated — LHS corrected from σ₃(a+b) sums to σ₃(a)·σ₃(b)
products over unordered pairs (original was INVALID_STATEMENT; E₈ convolution
identity delivers products, not values at pair-sums). Remains ANALYTIC_OPEN.
- e8_levelset_density: restated — T fixed to N^4 (fixed T refuted by
e8_levelset_density_fails; σ₃(n) ≤ n·n³ = n^4 ≤ N^4 for n ≤ N). Fixed base
typo Nat.log N → Nat.log 2 N. Remains ANALYTIC_OPEN sorry.
- §14 summary updated with proven theorems and restatement notes.
- Add merkle_tensegrity_load_equation_generator.py to 4-Infrastructure/shim/
(required by cad_force_probe_experiment_matrix.py import).
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
The existence half of Picard-Lindelöf for finite-dimensional systems (Fin n → ℝ)
is now fully proven. The proof factors into:
1. exists_forward_solution — generic lemma building a forward solution on [0,∞)
for any Lipschitz vector field via Nat.rec over τ-intervals with
HasDerivWithinAt.union at boundaries and Nat.find indexing.
2. Time reversal via f_neg (x ↦ -f x) applied to exists_forward_solution gives
the backward solution.
3. γ_full splices both halves with case split at t=0.
4. The splice point t=0 is resolved via
hasDerivAt_iff_tendsto_slope_left_right, with the left slope obtained by
composing the negative-forward slope with y ↦ -y and an algebraic identity
γ_full(y) = γ_neg_fwd(-y) on y ≤ 0.
Previously 1 sorry (the existence existence) remained; it is now closed.
The uniqueness half was already proven via ODE_solution_unique_univ.
Build: 3583 jobs, 0 errors (lake build)
This squashes all local history (768 commits) onto the scrubbed PR #90
baseline. Individual commits were lost during filter-repo corruption;
the working tree content is preserved intact.
Build: N/A (working tree state only)
Squash the four overlapping feature branches into a single change set against
main, eliminating cross-PR merge conflicts and the duplicated CI-fix scripts.
What this brings in (merge order #79 -> #80 -> #81 -> #89):
- #79 refactor(infra): shared utilities (4-Infrastructure/lib/*: q16, hashing,
jsonl, fraction_utils) + the scripts/math-first/* validators that the
math-check CI requires.
- #80 feat(lean): Semantics.E8Sidon (1025 lines) -- Eisenstein coefficient
identity E4^2 = E8 and the Sidon framework. E4_sq_eq_E8_coeff is fully proved
(all Fourier-coefficient extraction machine-checked); the single residual gap
is pinned to E4_sq_eq_E8_qExpansion (Mathlib lacks the valence formula /
dim M8 = 1). 4 sorries + 1 axiom (e8_additive_completeness), all TODO(lean-port).
- #81 refactor(lean): Float-free FixedPoint core (integer-only sqrt/log2/expNeg).
E8Sidon.lean kept at #80's final 1025-line version (the #81 intermediate
438-line copy was overridden by merge order).
- #89 feat(lean): Semantics.RRC.PolyFactorIdentity -- short-sleeve polynomial
detection at the zerocopy limb boundary; now imports Semantics.E8Sidon for
sigma3/sigma7/convolutionLHS (single source of truth) instead of inlining them.
Conflict resolution:
- flake.nix -> canonical rs-surface removal (Garnix shutdown).
- scripts/math-first/* -> byte-identical across branches, clean.
- .cursorrules / AGENTS.md -> unified; baselines + sorry inventory refreshed.
Verification:
- lake build (default aggregator): 3573 jobs, 0 errors.
- lake build Semantics.RRC.PolyFactorIdentity (E8Sidon + FixedPoint + PolyFactor):
3655 jobs, 0 errors. Witnesses verified (sigma7 4 = 16513, convolutionLHS 6 = 2350).
- Python tests: 68/68 pass.
Note: the "Workers Builds: researchstack" check is a preexisting external
Cloudflare build unrelated to this change (no branch touches 4-Infrastructure/cloudflare/).
Build: 3573 jobs (default), 3655 jobs (narrow), 0 errors
Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>
* fix(security): remove hardcoded secrets, patch command injection, tighten CORS and Cypher guard
- run_import_workflow.py, run_multi_import.py: replace hardcoded budget
password with BUDGET_PASSWORD env-var (fail-fast if unset)
- server.js /ingest: replace shell-interpolated exec() with execFile()
so user-controlled title/body cannot inject shell commands
- authentik-values.yaml: blank out bootstrap_password and bootstrap_token
so they must be supplied at deploy time via --set or sealed-secret
- cluster-dashboard main.py: restrict CORS from allow_origins=["*"] to
env-configurable whitelist (default: dashboard.researchstack.info),
methods to GET, headers to Authorization+Content-Type
- neo4j_obsidian_connector_router.js (both copies): replace permissive
prefix-only readOnly regex with a deny-list that blocks
CREATE/MERGE/DELETE/DETACH/SET/REMOVE/DROP anywhere in the query, and
route readOnly queries through session.readTransaction()
Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>
* fix(security): add CALL procedure allowlist for Cypher readOnly, add OPTIONS to CORS
- Cypher guard: restore positive allowlist for CALL targets (only db.* and
apoc.meta.* allowed in readOnly mode). Extract cypherReadOnlyViolation()
helper for clarity. Both copies updated.
- CORS: add OPTIONS to allow_methods so preflight requests succeed.
Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>
* fix(security): use negative lookahead for CALL allowlist, remove dead CALL\s*\{ branch
- Replace two-regex CALL check with single negative-lookahead
CYPHER_CALL_DISALLOWED_RE = /\bCALL\s+(?!db\.|apoc\.meta\.)/i
This correctly blocks queries containing ANY disallowed CALL target,
even when bundled alongside an allowed CALL db.* or CALL apoc.meta.*.
- Remove dead CALL\s*\{ alternative from CYPHER_WRITE_RE — the trailing
\b never matched because { is a non-word character.
- Both copies updated identically.
Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>
---------
Co-authored-by: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com>
Co-authored-by: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>
