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.
Document the switch from the unreachable k3s llama.cpp NodePort to a
local Ollama service (ollama-hermes3.service) serving hermes3:latest.
Hermes config now points at http://127.0.0.1:11434/v1. Note CPU fallback
until a CUDA-enabled llama-server is available.
Keep Kimi Code on the direct Kimi endpoint by default; document the
Headroom proxy as an opt-in via KIMI_BASE_URL env var. Avoids breaking
Kimi OAuth/search/fetch services when the proxy is not needed.
Add Kimi Code proxy subsection: systemd user service on port 8789,
Headroom anyllm/openai backend targeting https://api.kimi.com/coding/v1,
and ~/.kimi/config.toml base_url update.
