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.
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.
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)
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)
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)
- Bootstrapped microvm-racknerd node on its live Tailscale IP 100.80.39.40.
- Connected racknerd to the central QFox cluster.
- Assigned racknerd to its own vps zone with 1G capacity.
- Made garage-cluster-init.sh robust and idempotent.
- Updated comments and topology mappings.
Build: 3313 jobs, 0 errors (lake build)
- Vectorized create_yuv420_frame when numpy is available to eliminate the 500k-iteration scalar Python loop.
- Pre-filled memoryview slice buffers in the fallback path.
- Updated 4-Infrastructure/AGENTS.md to document the optimization.
Build: 3313 jobs, 0 errors (lake build)
Synthesized and placed-and-routed the UART beacon design on Tang Nano 9K with physical reset bypassed (rst_n_internal = 1'b1). Programmed the SRAM using openFPGALoader (CRC check: Success). Verified the physical UART blockage due to BL702 bridge firmware limitations via local probe, confirming the virtual serial route (virtual://q16-pty) as the active verification path. Updated scoped AGENTS.md files with the latest hardware status and Lean build baselines.
Build: 3313 jobs, 0 errors (lake build)
- Revert builder image in embedded_surface Dockerfile to rust:bookworm for glibc compatibility with bookworm-slim runner.
- Replace racknerd-surface.json Git LFS pointer with the actual retrieved JSON config to resolve parse errors.
- Separated and imported regenerated docker images for stubs and credential-server on all cluster nodes.
- Fixed Ingress resources and middleware to target the correct authentik-server service name.
- Rewrote verification script checks to handle iptables-based ports and relative redirects robustly.
- Updated nixos-laptop IP in node topology documentation.
Build: 0 jobs, 0 errors
Full Observe→Decide→Act→Emit loop for the restic + Garage + rclone stack:
- storage_agent.py: probes Garage health, restic snapshot count and dedup
ratio (Q16_16), backup log staleness, cold-copy drift; triggers corrective
actions (snap, cold-copy, verify, forget, offload, garage restart) based
on Q16_16 threshold comparisons. Emits hash-chained receipts to both a
local JSONL log (~/.cache/storage-agent.jsonl) and
s3://research-stack/agent-receipts/ in Garage.
- storage-agent.service / storage-agent.timer: systemd units installed
system-wide; timer fires every 15 min (RandomizedDelaySec=60). Includes
PATH=/home/allaun/.local/bin:... so aws cli and restic are resolved.
- .git/hooks/post-commit updated: agent runs (--once) in the background
after each restic snap, so post-commit state is always observed.
- 4-Infrastructure/AGENTS.md: full documentation of agent contract,
receipt schema, trigger table, log paths, and usage examples.
Shim boundary: zero logic — pure subprocess calls to existing CLI tools.
No Float, no new dependencies. py_compile and live dry-run verified.
Generated with [Devin](https://cli.devin.ai/docs)
Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
