Hermes already handles model routing. Remove MCP server, keep skill
as a cost-optimized model selection guide.
Key insight: DeepSeek V4 Pro is 55x cheaper than Claude Opus and
nearly as good at math/code. Default to DeepSeek, escalate to Opus
only when stuck.
Removed: break_glass_mcp.py (unnecessary — Hermes handles routing)
When --rrc is given, the shim runs pist-classify-trace on the trace fixture
and rrc-watchdog for RRC alignment, then writes an additional
rrc_alignment receipt into ene.receipts alongside the build receipt.
Sets content_hash to NULL for build_log packages so the partial unique
index ene_pkg_hash_idx does not prevent multiple ingestions of the same
build output. Each build session now gets its own package row. Also makes
receipt/ingest_event inserts idempotent with ON CONFLICT DO NOTHING.
Adds a Build-log automation section noting the post-commit hook runs lake_build_ingest.py Compiler in the background, inserting into ENE on neon-64gb. Includes log path and reinstall note.
Adds canonical database location notes to 4-Infrastructure/AGENTS.md:
- Postgres canonical instance is the arxiv-pg container on neon-64gb.
- Gremlin canonical instance is the Azure Cosmos DB endpoint.
- Explicitly warns against spinning up local Postgres on qfox for
production data.
Also adds `lake_build_ingest.py` to the stack-solidification anchors.
Adds 4-Infrastructure/shim/lake_build_ingest.py, a pure-I/O shim that:
- runs `lake build <target>` in the Semantics directory,
- parses job count, error count, warnings, and status,
- inserts a session, package, receipt, and ingest_event into the
ENE database on neon-64gb (arxiv-pg container).
The script contains no admissibility logic and no Float arithmetic.
Tested with `lake build Semantics.NKHodgeFAMM` — 8316 jobs, 0 errors,
session d1ea53db2185df87dd41497da12101f5.
Adds logViscosityRatio, log_viscosity_monotone, and ν_eff_monotone
to Semantics/NKHodgeFAMM.lean section 6b. The adaptive viscosity law
ν_eff = ν₀*(1+μ) is multiplicative in ν₀ and additive in scar density μ;
taking λ = log(ν_eff/ν₀) = log(1+μ) turns the multiplicative feedback into
an additive coordinate. This gives nlinarith a direct handle on viscosity
monotonicity and connects the module to Kritchevsky's "Everything Is
Logarithms" framing (SilverSight CITATION.cff).
Also marks a few pre-existing unused variables with underscores to silence
the linter.
Build: 8316 jobs, 0 errors (lake build Semantics.NKHodgeFAMM)
- Updates CHANGELOG.md with 2026-06-21 entry describing the two-regime
phase transition observed on neon-64gb: bosonic MC (p<=4) vs
distinguishable approximation (p>=5) in rrc_bosonic_tensor_network.py.
- Adds BMCTE, SBOE, LPMCE, effective support, and observable-estimation
vs exact-simulation terms to 6-Documentation/docs/GLOSSARY.md.
- Fixes Hilbert-dimension summary in rrc_bosonic_tensor_network.py to use
C(N+p-1, p) instead of C(N, p).
No core logic changed; documentation and summary-output correction only.
Check file sizes before loading bytes into memory and stream large files
directly into the tarball to prevent OOM errors on Steam Deck. Skip downloading
files that already exist locally.
Build: 0 errors (py_compile)
Adds 4-Infrastructure/shim/mcp_drive_gccl_compress.py:
- downloads a Google Drive folder via @piotr-agier/google-drive-mcp
- GCCL-delta-compresses contents into .tar.zst + JSON manifest
- uploads archive + manifest back to Drive
- optionally trashes the original folder
- handles MCP listFolder pagination
Updates 4-Infrastructure/AGENTS.md with the new shim anchor.
No rclone or egress-heavy operations; all Drive I/O goes through MCP.
Finds related arxiv papers for cornfield concepts via keyword overlap.
Uses /shm/arxiv_texts.tsv (559 MB) for fast local matching.
pg_trgm GIN indexes on neon-64gb for Postgres queries.
Results: 240 candidate citations for 48 concepts.
Loaded into concept_citations table (relation_type='candidate').
Moves all classification authority from Python into Lean:
- Adds `0-Core-Formalism/lean/Semantics/PistClassifyTrace.lean` executable.
Reads a raw trace JSON and emits spectral radius, RRC shape, and tactic
family using `Semantics.PIST.Spectral` and `Semantics.PIST.Classify`.
- Registers `pist-classify-trace` in `lakefile.toml`.
- Fixes `Semantics.PIST.Spectral` power iteration to handle directed
transition matrices:
- `symmetrize` now preserves half-integer weights as Q16_16 raw values.
- `matVecMul` uses saturated Q16_16 arithmetic to prevent overflow.
- Rewrites `4-Infrastructure/shim/pist_trace_classify_offline.py` as a pure
I/O wrapper: reads JSON, calls the Lean classifier, optionally calls
`rrc-watchdog`, and emits the combined JSON. Removes Python-side spectral
computation, shape thresholds, tactic heuristic, and KNN.
- Updates `AGENTS.md` and `4-Infrastructure/AGENTS.md` with the new build
baseline and shim contract.
Verification:
- `lake build` → 8604 jobs, 0 errors
- Canary trace outputs match previous Python outputs to within Q16_16 rounding
(e.g., apply_chain λ_q16 = 59044 vs 59045).
- `python3 -m py_compile` on the rewritten shim passes.
Created a local, offline Python shim `pist_trace_classify_offline.py` that computes trace transition matrix spectra, maps the max eigenvalue to the Q16.16 spectral radius, evaluates the color-space shape classification logic from `Semantics.PIST.Classify`, and invokes the local `rrc-watchdog` Lean binary inside the podman container to verify alignment. This avoids querying the dead AWS RDS instance and saves LLM API tokens.
Build: 3314 jobs, 0 errors (lake build Compiler)
Added a python-based wrapper script for lean-lsp-mcp that intercepts and cleans the 'severity' schema field from the tools/list output, resolving the 400 error from Moonshot API which strictly forbids defining 'type' in parent schemas alongside 'anyOf'.
Build: 3314 jobs, 0 errors (lake build)
- Replace repo .mcp.json with minimal config (10 essential servers instead
of 29). Full backup retained as .mcp.json.full.
- Remove inline MCP section from ~/.config/opencode/config.json so OpenCode
loads only repo .mcp.json (also removes hardcoded Linear token leak).
- Add singleton guards to opencode_prover_mcp.py, token_saver_mcp.py, and
remote_lean_proof_mcp.py to prevent duplicate instances when multiple
IDE configs reference them.
Build: N/A (Python shims)
- qaoa_adapter.py: fix finsler_metric_to_qubo to store Q_ij + Q_ji per
undirected pair; update is_anisotropic and _find_anisotropic_pair to
accept raw_matrix so asymmetry detection still works after summation;
add measure option to pauli_to_cirq.
- benchmark_finsler_qaoa.py: new benchmark harness for Finsler-Randers
routing via QAOA.
Formulate directed Finsler routing as TSP-MTZ (QAP) using HiGHS MIP and
benchmark against QUBO subset-selection. Five solvers across four sizes.
Key results:
- QAP-MIP scales well: n=48 solves to feasibility in 13s
- QUBO degenerate for all-positive Q_ij (unconstrained always selects 0)
- 2-phase strategy viable: QUBO-card to select K, then TSP-on-subset
Build: N/A (Python shim)
Perceval is the photonic quantum simulation SDK used by
rrc_photonic_stress_test.py (SLOS backend). Already installed
system-wide; added to requirements.txt for venv reproducibility.
- 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)
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.
- 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>
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>
