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').
240 candidate citations found for 48 cornfield concepts using
pg_trgm GIN indexes and /shm file-based matching against 700k papers.
DB state: 358 total concept_citations (96 grounds, 22 extends, 240 candidates)
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)
Overwrites 6-Documentation/docs/plans/SilverSight_completion_pipeline.md
with a per-file, per-theorem, per-commit microstep plan covering Phases
1-8: Core Semantics completion, Research Stack triage/port, corpus build,
mathematical models, shim rewrite, hardware extraction, applications,
and final documentation/promotion. Includes claim-state ladder, open
question answers, dependency graph, verification gates, CI coverage,
risks, and acceptance criteria.
Adds 6-Documentation/docs/plans/SilverSight_completion_pipeline.md,
describing the full phase plan from the current core Semantics state to
a verified SilverSight 1.0: Core completion, Research Stack triage/port,
corpus build, mathematical models, shim rewrite, hardware extraction,
applications, documentation, and claim-state promotion.
Adds 6-Documentation/docs/specs/SilverSight_Spec.md, documenting the
YaFF-inspired separation of schema, layout, access pattern, wire format,
view, layout bridge, and canal-aware layout selection for the SilverSight
clean-slate architecture.
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)
UniversalMathEncoding.lean (1,000 lines):
- 50 MathTokens organized into 8 Hachimoji groups
- 2^50 = 1.126 quadrillion unique expression addresses
- Sparse embedding: each token → 2D plane in 16D chaos space
- Multiple embedding: address activates direct sum of constituent planes
- Sub-basin classification: (Hachimoji state, Sidon sub-address) pair
- ~268 million sub-basins, ~4,000 expressions each
- Full PVGS-DQ receipt compatibility
Concept: every mathematical expression ever written fits in 0.1%
of the 2^50 address space. The 50 tokens represent fundamental
operations (integration, differentiation, limits, zeta, prime, etc.).
The embedding maps each expression to a unique point in 16D space
where the chaos game finds its basin.
Scaling: 2^50 ≈ 10^15 = number of sand grains on all Earth beaches.
OpenCode was auto-discovering .cursor/mcp.json in addition to .mcp.json and
spawning duplicate contextstream (and other) MCP servers. Remove the
Cursor-specific config from the repo root and keep its content in
.cursor-mcp-config.json for restoration when running Cursor.
- 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)
- ARCHITECTURE.md: update level-0 job counts (8332 full workspace, 3314
Compiler surface, 0 errors).
- PyrochloreSidonBridge.md: point to current pyrochlore_sidon_receipt_v2.json
(S=1) and note removal of stale S=5/2 receipt.
- fiedler_non_identifiability.md: new note on Fiedler non-identifiability.
- 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.
Add Semantics.ChentsovBridge with:
- Discrete simplex, tangent vectors, Markov morphisms
- Fisher-Rao metric field and quadratic form
- Axiom for Chentsov uniqueness (literature reference)
- SIM metric from RandersMetric alpha component
- Main theorem: torsion-free => SIM = Fisher (up to scale)
- mergeTwo coarse-graining example (2 bookkeeping sorries)
- simMetricIsMonotone axiom with TODO(lean-port) proof sketch
Update AGENTS.md pending proof work section.
Verification: narrow target lake build Semantics.ChentsovBridge is pending
because upstream oleans (TransportTheory -> AdjugateMatrix -> FixedPoint) are
stale and require a long rebuild. Syntax was checked via lake env lean.
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.
