allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
626 commits 18 branches 0 tags 425 MiB
Commit graph

169 commits

Author SHA1 Message Date
allaun
a247dcb1b6 feat: complete all four interconnected solves 
1. NKHodgeFAMM ↔ BurgersPDE bridge — dq_energy_satisfies_scar_condition, burgers_embedding, applyViscosityN induction, scarDensityFromDQ. Build: 8316 jobs, 0 errors.

2. Lonely Runner sim — lonely_runner_sim.py with circular Betti tracking. All k≤4 test cases confirm beta_0 > 0 (lonely times exist). Fixed uint8 wrap-around bug.

3. Taylor-Green Betti tracker — taylor_green_betti.py with 6 scenarios. beta_2 correctly detects voids: TG smooth=0, TG+void>0, noise=77. Fixed int64 serialization in betti_tracker.py.

4. Q1/Q2 vorticity decomposition — VorticityDecomposition.lean: Q1_is_dilatational, Q2_is_solenoidal, enstrophy_proportional_to_Q2, velocity_hodge_decomposition. All rfl proofs + native_decide witnesses. Build: 8598 jobs, 0 errors.
 2026-06-16 22:21:55 -05:00
allaun
8cd2fa02f3 feat: NK-Hodge-FAMM formal axiom + Lonely Runner Betti mapping + numerical Betti tracker + vorticity resolution 
Four interconnected solves:

1. NKHodgeFAMM.lean (218 lines) — formal axiom: beta_2(scar support) = 0 implies global H1 regularity. Includes gradient, simplicial complex, bettiNumber axiom, derived theorems. Build: 8598 jobs, 0 errors.

2. lonely_runner_betti_mapping.md (294 lines) — rigorous mapping: Lonely Runner Conjecture equivalent to beta_0(M_t) > 0 (non-empty scar support), a special case of the beta_2 = 0 condition under S1 thickening.

3. betti_tracker.py + test_betti_tracker.py — numerical Betti tracker via gudhi cubical persistence. Computes beta_0, beta_1, beta_2 from velocity field gradient norms. 7 unit tests pass including spherical void detection.

4. cole_hopf_vorticity_resolution.md (293 lines) — resolves the irrotational base flow tension: Cole-Hopf constrains only Q1 (dilatational); Q2 (solenoidal) carries vorticity independently.
 2026-06-16 22:14:10 -05:00
allaun
2d7d9bc2b8 proof(lean): close e8_singer_improvement and erdos30_e8_conditional; restate two invalid sorries 
- 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>
 2026-06-16 14:50:02 -05:00
allaun
475f6319ea chore(repo): push local 768-commit branch state onto clean remote baseline 
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)
 2026-06-15 22:46:50 -05:00
Devin AI
0639eae30a chore(consolidation): integrate E8Sidon stack (PRs #79 #80 #81 #89) into one PR 
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>
 2026-06-16 02:01:31 +00:00
devin-ai-integration[bot]
6db78dccf3 test(coverage): add 138 unit tests for least-covered modules (#78) 
Four test files covering the modules with zero or near-zero test coverage:

- scripts/qc-flag/test_lean_qc_flagger.py (55 tests)
  Covers all pure helpers, code-line detection, QCIssue/FileResult classes,
  and all 5 check functions (structural, naming, Q16, proof quality, deps).

- 4-Infrastructure/shim/test_braid_diat_codec.py (22 tests)
  Covers Q0_2 encode/decode, ChiralityDIAT roundtrips and verify_b,
  MountainPacked dict↔bytes, BraidResidualPacked bracket↔bytes.

- 5-Applications/tools-scripts/llm/test_emitter_utils.py (33 tests)
  Covers sha256_bytes, canonical_json_bytes, repo_relative, safe_slug,
  timestamps, context bundles, message building, extract_answer,
  auth guard, and verify_receipt schema rules.

- 4-Infrastructure/shim/test_validate_rrc_predictions.py (28 tests)
  Covers require_path, parse_equation, build_proof_metrics,
  build_receipt with all domain mappings, and MATH_* constant sets.

Build: all 138 tests pass (pytest), py_compile clean

Co-authored-by: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com>
Co-authored-by: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>
 2026-06-14 19:31:16 -05:00
Brandon Schneider
aba1fba7ad fix(adversarial-review): resolve 35 critical coding bugs across 8 subsystems 
Security & correctness fixes from full adversarial review:

Lean (7 fixes):
- FixedPoint.lean: guard false theorem with n > 0 precondition
- QFactor.lean: remove double-scaling error in energy decrease
- AVMIsa/Step.lean: implement addSatQ16/subSatQ16 primitives
- BraidEigensolid.lean: fix crossStep second output argument swap
- SSMS.lean: complete ACI preservation proof (with rounding caveat)
- HouseholderQR.lean: add n > 0 precondition to spectral theorem

Verilog (7 fixes):
- q16_lut_core.v: fix multiply shift (16 → 32 bits)
- q16_lut_top.v: fix valid bit (0 → 1)
- cff_accelerator.v: fix SHA-256 padding (len < 448 check)
- research_stack_top.v: fix trigger aliasing (unique counters)
- Blitter6502OISC_small.v: fix address width (15 → 16 bits)
- spatial_hash_bram.v: add OOB write guard
- tmr_oepi_safety_fsm.v: fix double-increment race

WGSL (6 fixes):
- shaders.wgsl: atomicAdd for concurrent writes
- frustration_qubo.wgsl: double-buffer + CAS loop
- braid_fft.wgsl: workgroupBarrier synchronization
- burgers_scar_filter.wgsl: atomic E_bins array

Rust (9 fixes):
- thermodynamic.rs: Arc::from_raw → Arc::clone (double-free)
- thermodynamic.rs: Box::into_raw → Box (leak)
- tools/src/lib.rs: shell injection → shlex.quote
- ene-node/src/lib.rs: LRU caps, constant-time HMAC, peer caps

Python (6 fixes):
- similarity/__init__.py: pickle.load → RestrictedUnpickler
- AI-Feynman: torch.load → weights_only=True (14 calls)
- fetch_arxiv.py, fetch_s2.py: eval → ast.literal_eval
- topology.py: os.system → shutil.copy2
- SSH pipe: os.system → base64 pipe

Build: lake build 3572 jobs, 0 errors
 2026-05-31 23:38:03 -05:00
Brandon Schneider
9e80ac68ca feat(infra): Jellyfin wizard complete, SSO-Auth plugin files deployed 
- Jellyfin setup wizard completed, admin account created (admin/jellyfin-admin)
- SSO-Auth plugin v4.0.0.3 downloaded and placed in plugins directory
- Authentik OIDC provider for Jellyfin updated with correct redirect URI
- All services verified running

Build: 3313 jobs, 0 errors (lake build Compiler)
 2026-05-31 14:14:20 -05:00
Brandon Schneider
008cf8fefe feat(infra): migrate external service registry to aiven mysql with ssl 
- Migrated service_registry.py defaults from InfinityFree to Aiven MySQL.
- Enforced REQUIRED SSL mode on connections (ssl_mode for mysql-connector, ssl dict for pymysql).
- Added helper _get_dict_cursor to resolve pymysql compatibility issues.
- Configured registry password and encryption key in decrypted/encrypted .env via SOPS.

Build: 3313 jobs, 0 errors (lake build)
 2026-05-31 02:10:10 -05:00
Brandon Schneider
aff285be30 fix(infra): service registry is backup/fallback, not primary 
Primary: Tailscale mesh + internal PostgreSQL/SQLite
Backup:  InfinityFree MySQL (this file)

Use cases for backup path:
  - Edge nodes that cant reach mesh (ESP32, Cloudflare Workers)
  - Mesh-down fallback (Tailscale outage)
  - Cross-mesh discovery (different tailnets)
  - Low-impact config distribution
 2026-05-30 21:19:24 -05:00
Brandon Schneider
ebcf0571ec feat(infra): external service registry via InfinityFree MySQL 
service_registry.py — mesh-independent node discovery and credential store.

Tables:
  nodes       — registered devices with capabilities, tier, IPs
  credentials — encrypted blobs (ChaCha20) with TTL auto-expiry
  config      — distributed key-value configuration

Features:
  - auto_register() — uses device_capability_probe to register
  - discover_nodes() — find nodes by tier, with max-age filter
  - store/get_credential() — encrypted at rest, short TTL
  - heartbeat() — keepalive for node registry
  - CLI: init, register, discover, store, get, cleanup, config-set/get

Any node with internet can reach it (no Tailscale required).
Credentials encrypted with ChaCha20, key from REGISTRY_ENCRYPT_KEY env.
 2026-05-30 21:14:51 -05:00
Brandon Schneider
6d4d099625 fix(infra): tier limits leave headroom for device function 
Each tier now reserves resources for its primary function:
  GPU_CUDA:     8GB VRAM (not 12 — keep 4GB for display/compositor)
  GPU_VAAPI:    256MB (keep VRAM headroom for desktop)
  GPU_APU:      128MB (shared DDR, OS needs bandwidth)
  CPU_FFMPEG:   64MB, half cores (leave for OS/k3s)
  BATCH:        1500 min/month (reserve 500 for actual CI/CD)
  ETHERNET:     500ms timeout (leave bandwidth for SSH/mgmt)
  FRAMEBUFFER:  768KB (half — keep display visible, compute in top rows)
  WASM:         512B payload, 8ms CPU (leave 2ms for JSON overhead)
  DSP:          2048 samples (half FFT, leave for overlap buffer)
  ESP32:        512B (WiFi/BLE stack needs ~80KB of 520KB SRAM)
 2026-05-30 20:45:50 -05:00
Brandon Schneider
ba1bf871f8 feat(infra): per-tier device limitations for Ray scheduling 
DeviceLimitations dataclass with hard constraints per tier:
  GPU_CUDA:     1GB payload, 16 concurrent, 60s, NVENC, 12GB VRAM
  GPU_VAAPI:    512MB payload, 8 concurrent, 60s, VAAPI HW
  GPU_APU:      256MB payload, 4 concurrent, 30s, shared DDR
  CPU_FFMPEG:   128MB payload, 2 concurrent, 120s, software
  BATCH:        64MB payload, 1 concurrent, 6h, 2000 min/month
  ETHERNET:     1400B payload, 1 concurrent, 1s, virtio-net
  FRAMEBUFFER:  1.5MB payload, 1 concurrent, 100ms, DMA only
  WASM:         1KB payload, 1 concurrent, 10ms, 100K req/day
  DSP:          16KB payload, 1 concurrent, 5s, FFT only
  ESP32:        2KB payload, 1 concurrent, 100ms, Q0_16 scalar

get_limitations(caps) returns actual hardware-aware limits
(vram override, framebuffer capacity, memory override)
 2026-05-30 20:44:31 -05:00
Brandon Schneider
cadb38cc1b feat(infra): add AMD VAAPI + FLAC DSP to FrameDispatcher 
FrameDispatcher now routes 6 tags:
  TAG_STRAND(0x01)  → BraidBackend (VCN compute)
  TAG_CROSSING(0x02) → BraidBackend (VCN compute)
  TAG_PIST(0x03)    → BraidBackend (VCN compute)
  TAG_LUPINE(0x04)  → CUDABackend (NVIDIA CUDA)
  TAG_VAAPI(0x05)   → VAAPIBackend (AMD/Intel VA-API)  ← NEW
  TAG_FLAC(0x06)    → FLACBackend (PipeWire/FLAC DSP)  ← NEW

New backends:
  - VAAPIBackend/LocalVAAPIBackend: AMD/Intel hardware encode/decode
  - FLACBackend/LocalFLACBackend: FFT spectral analysis, centroid, RMS
  - RayVAAPIBackend: Ray actor for VA-API operations
  - SyncVAAPIWrapper/SyncFLACWrapper: sync bridges for FrameDispatcher

Capability probe: DSP tier(1) added between FRAMEBUFFER(2) and ESP32(0)
 2026-05-30 20:35:42 -05:00
Brandon Schneider
5320a08105 feat(infra): integrate edge WASM and GitHub batch compute tiers 
- Update device_capability_probe.py to add BATCH and WASM tiers and fix a NameError bug on has_virtio_net.
- Build Cloudflare Workers WASM compilation and JS fetch handler in 4-Infrastructure/cloudflare/ executing trinary VM steps.
- Create GitHub Actions batch_compute.yml workflow to harvest runner minutes.
- Keep 4-Infrastructure/AGENTS.md updated with the WASM core library anchor.

Build: 3313 jobs, 0 errors (lake build)
 2026-05-30 20:08:31 -05:00
Brandon Schneider
d6fc9cfe6d feat(infra): add ETHERNET compute tier for virtio-net PistPacket DMA 
New tier between CPU_FFMPEG and FRAMEBUFFER:
  GPU_CUDA(7) > GPU_VAAPI(6) > GPU_APU(5) > CPU_FFMPEG(4) >
  ETHERNET(3) > FRAMEBUFFER(2) > ESP32(1) > RELAY(0)

- _detect_virtio_net(): probes /sys/class/net for virtio driver (0x1af4)
- PistPacket computation via TX/RX descriptor rings
- Host vhost-user backend does matrix transforms
- CRC32 hardware offload = witness verification
- Works in any VM with network (even without framebuffer)
 2026-05-30 20:02:06 -05:00
Brandon Schneider
66abf92214 fix(infra): handle Cirrus Logic virtual VGA and DRM naming edge cases 
- Add Cirrus Logic (0x1013) and virtio (0x1af4) to vendor map
- Fix DRM card parsing for names like "card0-VGA-1"
- Virtual GPUs (cirrus, virtio) never classified as discrete
- Virtual GPUs skip VA-API tier, fall to FRAMEBUFFER

Racknerd microVM (2vCPU, 715MB, Cirrus VGA) correctly classified as
FRAMEBUFFER tier: 1024x768 @ 16bpp = 1.57 MB DMA backplane.
 2026-05-30 19:59:38 -05:00
Brandon Schneider
16101a787f feat(infra): device capability probe with framebuffer fallback 
device_capability_probe.py: classify every device into a compute tier.

Tiers (highest to lowest):
  GPU_CUDA    — NVIDIA discrete + CUDA (NVENC, Ray GPU worker)
  GPU_VAAPI   — AMD/Intel discrete + VA-API (hardware encode)
  GPU_APU     — AMD integrated, yuvj420p, bandwidth-optimized
  CPU_FFMPEG  — Software encode only (libx264)
  FRAMEBUFFER — /dev/fb0 DMA backplane (8.29 MB/frame at 1080p)
  ESP32       — MCU, Q0_16 scalar in FreeRTOS idle hook
  RELAY       — Network only, no compute
  OFFLINE     — Unreachable

Features:
  - Multi-GPU DRM render node scanning (card0=AMD, card1=NVIDIA)
  - APU vs dGPU classification via device name + VRAM heuristics
  - Framebuffer detection with /sys/class/graphics/fb0 resolution
  - Ray scheduling helpers (get_ray_placement_strategy)
  - Cluster probe via SSH
  - JSON + human-readable output
 2026-05-30 19:57:07 -05:00
Brandon Schneider
cf907e2835 feat(infra): add QEMU graphics framebuffer packing shim and spec 
- Add qemu_framebuffer_packer.py supporting ARGB8888/RGB24 raw matrix mapping
- Implement zero-copy mmap write/read interface to /dev/fb0 with signature headers
- Document the QEMU graphics framebuffer backplane in Section 11 of spec
- Update 4-Infrastructure/AGENTS.md and walkthrough.md documentation
- Verify syntax and workspace compilation baseline status

Build: 3313 jobs, 0 errors (lake build)
 2026-05-30 19:49:25 -05:00
Brandon Schneider
850f644e0f feat(infra): Ray VCN bridge — FrameDispatcher over Ray transport 
ray_vcn_bridge.py: Ray transport for the VCN-LUPINE bridge.
  Replaces GPUNodeConnection TCP/MKV transport with Ray ObjectRef.
  FrameDispatcher, BraidBackend, CUDABackend are unchanged — only
  the wire between daemon and GPU node changes.

  - RayBraidBackend: compute actor matching VCNBraidBackend pattern
  - RayCUDABackend: GPU actor with /dev/dri (Mesa, no NVIDIA plugin)
  - RayVCNBridge: full bridge as Ray actor (replaces daemon)
  - RayGPUNodeConnection: drop-in for GPUNodeConnection
  - SyncBraidWrapper/SyncCUDAWrapper: bridge Ray actors to sync interface

  STRAND 42B → 63B, CROSSING 42B → 22B, PIST 24B → 57B
  Batch 10: 5ms (0.5ms/frame), 10/10 non-empty
 2026-05-30 19:48:34 -05:00
Brandon Schneider
30d4772a3f feat(infra): support heterogeneous environments in video compute decoder 
- Implement dynamic resolution and format probing using ffprobe inside decode_frames
- Eliminate hardcoded YUV420 frame size slicing during video file readback
- Standardize NVIDIA hardware config to 8-bit full-range yuv444p to keep byte layout unified
- Verify Python compilation and Lean workspace integrity checks

Build: 3313 jobs, 0 errors (lake build)
 2026-05-30 19:48:09 -05:00
Brandon Schneider
2bce7abaa9 feat(infra): optimize AMD APU/iGPU lossless pipeline targeting H.265 cores 
- Add detection for integrated AMD graphics (APUs/iGPUs) based on hardware model name
- Configure UMA-friendly full-range yuvj420p format to reduce system memory bandwidth footprint by 50%
- Force lossless constant QP (-qp 0) and full PC range to prevent clamping loss
- Re-run syntax checks and Lean compiler verification tests

Build: 3313 jobs, 0 errors (lake build)
 2026-05-30 19:46:34 -05:00
Brandon Schneider
6ea34fbae6 feat(infra): add GPU-specific math optimization loader for H.265 VCN/NVENC 
- Implement MathOptimizationLoad dataclass to represent GPU packing configurations
- Update probe_vcn_capabilities to resolve optimizations for NVIDIA/AMD/Intel GPUs
- Extend compute_frame_size to support yuvj420p, 10-bit YUV, and YUV444p
- Propagate optimized pixel formats into select_optimal_resolution and spec
- Update _build_ffmpeg_cmd to inject lossless/zero-latency options and HEVC/H.265 metadata SEI NAL parameters
- Update 4-Infrastructure/AGENTS.md documentation

Build: 3313 jobs, 0 errors (lake build)
 2026-05-30 19:45:09 -05:00
Brandon Schneider
63093f56da feat(infra): Ray VCN transport + cluster restoration 
- ray_vcn_transport.py: @ray.remote wrappers for braid VCN encode/decode
  - Distributed encode on CPU workers, compute on GPU workers
  - RayVCNTransport actor with frame counter + ObjectRef storage
  - FAMM-gated encode task, batch encode/decode helpers
  - 20 strands in 576ms (28.8ms/strand), 20/20 CRC ok

- raycluster.yaml: KubeRay cluster on qfox-1
  - Head + CPU worker + GPU worker (RTX 4070 SUPER via /dev/dri)
  - No NVIDIA device plugin — Mesa direct device access
  - Tolerations for desktop taint on qfox-1
  - num-gpus instead of custom GPU resource

- fix-nftables-k3s.sh: nftables forward rules for flannel/cni0
  - nftables default policy=drop blocks pod-to-pod networking
  - systemd service nftables-k3s-fix for persistence

- KubeRay operator moved to nixos (control plane can reach API server)
- FFmpeg 8.0 + reedsolo installed in Ray head pod via conda
 2026-05-30 19:42:39 -05:00
Brandon Schneider
61b38ca697 refactor(infra): optimize YUV420 frame packing using numpy 
- 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)
 2026-05-30 19:32:11 -05:00
Brandon Schneider
30d8c56158 feat(infra): improve RRC Ray Layer Tagger and align registry 
Improved rrc_ray_tagger.py with prioritized source name-based variant matching, corrected NetworkRayReceipt (3 variants, 67us) and BurgersRGSolver (5 variants) shapes, fixed Hopf-Cole fallback bug using string normalization, dynamically deduced workspace root path, and quarantined phase_update due to adversarial review falsification. Registered anchor in 4-Infrastructure/AGENTS.md.

Build: 3313 jobs, 0 errors (lake build Compiler)
 2026-05-30 19:18:02 -05:00
Brandon Schneider
4965029758 feat: integrate May 2026 math papers into Research Stack 
1. Singer Sidon Sets (2605.03274):
   - New SidonSets.lean: IsSidon, IsSidonMod, IsIntervalSidon, h(N)
   - 5 fully proved lemmas, 13 sorry with TODO(lean-port)
   - GoldenRatioSeparation.lean: singer_density_lt_golden (proved)
   - lake build: 3303 jobs, 0 errors

2. Hexagonal lattice + RG (2605.09974):
   - New test_hexagonal_lattice_rg() in unified_rg_tests.py
   - Avila's global theory exact phase diagram
   - RG confirms localized/extended regimes
   - Fractal dimension: extended→1, critical→0.5, localized→0
   - 7 tests, all pass

3. Burgers + Hopf-Cole + Fokas (2605.11788):
   - Added solve_heat_fokas() — unified transform method
   - Added solve_burgers_fokas() — full Burgers via Hopf-Cole + Fokas
   - Added solve_heat_fourier_series() — comparison solver
   - Fokas converges in ~64 quadrature points vs Fourier 2000 terms
   - Hopf-Cole FFT: 8-208x faster than finite differences
 2026-05-30 18:16:57 -05:00
Brandon Schneider
a53e023cbe feat: Hopf-Cole exact solver for 1D Burgers — 151x speedup 
Hopf-Cole transformation maps Burgers to heat equation:
  u = -2v * d(ln ψ)/dx
  dψ/dt = v * d²ψ/dx² (exact via FFT)

Benchmark results:
  N=512,  v=0.01: 1.45x speedup
  N=1024, v=0.01: 83.4x speedup
  N=2048, v=0.01: 151.3x speedup

Key insight from adversarial review:
  - RG assumption (nonlinear term vanishes) is FALSE
  - But 1D Burgers IS integrable via Hopf-Cole
  - Exact solution in O(N log N), no time stepping
  - The 'insultingly easy' regime exists — just not via RG

This is the exact solution the agents found when they
broke the RG fixed point assumption.
 2026-05-30 17:36:12 -05:00
Brandon Schneider
c556d64ae0 feat: QEMU compute surfaces — virtio-crypto + ivshmem 
virtio_crypto_transform.py:
- VirtioCryptoSession: HASH session (SHA-256, SHA-512, MD5)
- VirtioCryptoHashTransform: encode as HASH request, produce receipt
- Receipt: {schema, transform_type, algo, payload_bytes, result_hex, witness_hash}
- Wire-format structs: CtrlHdr(20B), HashSessionPara(8B), HashDataReq(28B)
- RFC 6234 test vectors: all pass

ivshmem_client.py:
- IvshmemClient: mmap /dev/shm/ivshmem_bar0
- IvshmemRing: doorbell notification
- IvshmemTransform: write payload, ring doorbell, produce receipt
- Receipt: {schema, transform_type: shared_memory, offset, length, witness_hash}
- Memory layout: registers 0x0000, metadata 0x10000, data 0x20000
- /dev/shm fallback test: verified
 2026-05-30 17:35:24 -05:00
Brandon Schneider
f63e4b5179 feat(infra): virtio-net ring as compute pipeline 
Add virtio_net_transform.py: three Class-1 computation primitives via
virtio-net TX/RX rings — zero backend code changes needed.

  1. HASH_REPORT — host writes Toeplitz RSS hash into RX header
     (virtio_net_hdr_v1_hash.hash_value return channel)
  2. TSO gso_size — host splits large buffer via TCP segmentation offload
     (spatial partition into N × gso_size chunks)
  3. MRG_RXBUF — host merges multiple RX buffers (aggregation primitive)

Structs: VirtioNetHdr (12B), VirtioNetHdrHash (20B), VringDesc (16B).
Receipt schema: virtio_transform_receipt_v1 with CRC32 witness_hash.

The copy-if filter (skip zero deltas, process non-zeros) maps directly
onto the HASH_REPORT return channel: delta=0 → hash skip, delta≠0 →
hash_as_function_of_payload. This is the ambient compute model:
any QEMU/firecracker microVM is already a computation device without
knowing it.

Build: 3313 jobs, 0 errors (lake build)
Tools: glslang, spirv-as, spirv-dis (native); tint from nixpkgs for WGSL
 2026-05-30 16:54:09 -05:00
Brandon Schneider
9c5fe97dc1 feat(infra): SPIR-V packet generator and WGSL scar filter shader 
Add spirv_packet_generator.py: reads SPIR-V assembly, applies copy-if
optimization (OpPhi→OpSelect transform), and emits JSON packet descriptors
with the 5 OpPhi-derived fields (type_id, cond_id, true_val_id,
false_val_id, result_id) that fully specify the packet layout.

Add burgers_scar_filter.wgsl: 291-line WGSL compute shader for spectral
scar filtering in 2D Burgers RG solver. Uses three copy-if patterns:
  1. scar_pressure > threshold → apply hyperviscosity damping
  2. |kx| > k_cut || |ky| > k_cut → zero (dealiasing)
  3. factor < 0.999 → multiply velocity components

Also fix spirv_copy_if_optimizer.py: OpSelect now uses phi_instr.args[0]
(type operand) as its type, instead of compute_instr.result_id. This
produces structurally correct SPIR-V where the result type matches the
OpSelect opcode layout.

Build: 3313 jobs, 0 errors (lake build)
Tools: glslang, spirv-as, spirv-dis (native); tint from nixpkgs for WGSL
 2026-05-30 16:40:58 -05:00
Brandon Schneider
cfd43e1e95 feat(codec): extend BraidDiatCodec with BraidDiatFrame encoder/decoder 
- BraidDiatCodec.lean: BraidDiatFrame now handles encode/decode of full
  SpherionState × BraidReceipt with 256-bit header and variable mountain list
- braid_diat_codec.py: Python extraction updated to match, benchmark artifact
  at shared-data/artifacts/braid_diat_codec_benchmark.json (714B avg vs
  messagepack 1748B avg)

Build: lake build Compiler 3313 jobs, 0 errors
 2026-05-30 16:23:41 -05:00
Brandon Schneider
81d4338627 feat: ARM64 copy-if optimizer — branches to CSEL 
Transforms branch patterns to ARM64 conditional selects:
  Before: CMP + BEQ + compute + B + MOV = 5-47 cycles
  After: CMP + compute + CSEL = 4-6 cycles

ARM64 CSEL instruction:
  CSEL Xd, Xn, Xm, cond
  - Single cycle on most ARM64 processors
  - No branch prediction penalty
  - No pipeline flush on mispredict

Pattern detection:
  - CMP + BEQ/BNE/B.LT/etc
  - True block: 1-3 compute instructions + B
  - False block: single MOV
  - Merge point

Same pattern as:
  - SPIR-V OpSelect (GPU shaders)
  - VCN delta+RLE (3.3x)
  - QR spatial hash (2.18x)
  - Lean CopyIfTactic (2.7x)

Works on ARM64 assembly from GCC/LLVM/Rust.
No compiler fork needed — post-processing pass.

Targets: Neon-64GB (18 vCPU ARM64 EPYC)
 2026-05-30 15:59:24 -05:00
Brandon Schneider
2e15c7c0a5 feat: SPIR-V copy-if optimizer — skip zero deltas in GPU shaders 
Transforms branch-based patterns to OpSelect:
  Before: 3 blocks, OpBranchConditional, OpPhi
  After: 1 block, OpSelect (single-cycle on most GPUs)

Pattern detection:
  - OpSelectionMerge + OpBranchConditional
  - True block: single compute + OpBranch
  - False block: empty (just OpBranch)
  - Merge block: OpPhi merging true/false values

Transformation:
  - Remove SelectionMerge + BranchConditional
  - Inline compute instruction
  - Replace OpPhi with OpSelect
  - Collapse 3 blocks to 1

Same pattern as:
  - VCN delta+RLE (3.3x): skip zero bytes
  - QR spatial hash (2.18x): skip non-neighbors
  - Lean compilation (2.7x): skip trivial theorems
  - Spatial hash (86.5% cache hit): skip empty cells

Driver-agnostic: works at SPIR-V level before Mesa.
No Mesa fork required. No NIR pass needed.
 2026-05-30 15:57:08 -05:00
Brandon Schneider
d5428a8950 feat: QR spatial hash integration — 2.18x speedup 
Cache-friendly Householder QR via Morton-code spatial hash:
- When adding column, only apply reflections to 3x3x3 neighborhood
- Reduces per-update from O(n) to O(27) per column
- 50x50 matrix, 500 updates: 2.18x faster than naive

Naive: 0.124ms/update
Spatial: 0.057ms/update
Speedup: 2.18x

Key insight: Morton code ordering means nearby columns in 3D
are nearby in memory → cache-friendly access → fewer misses.

This completes all 4 next steps:
1. ✅ O_AMMR_QRNode wired into BraidDiatFrame (already done)
2. ✅ O_AMMR_valid strengthened with residual bounds (NS_MD.lean)
3. ✅ Hash benchmark: Morton wins (86.5% cache hit rate)
4. ✅ QR spatial hash: 2.18x speedup
 2026-05-30 15:30:06 -05:00
Brandon Schneider
bdc227459a feat: O_AMMR_valid strengthened + hash benchmark complete 
NS_MD.lean:
- Added QRResidualWitness structure (Q16_16 fixed-point)
- Added residual_bound_ok, basis_size_ok, orthogonality_ok predicates
- Extended O_AMMR_Node with qr_witness field
- Strengthened O_AMMR_valid: 4 conjuncts (admission + residual + basis + ortho)
- lake build: 3300 jobs, 0 errors

hash_benchmark.py (240 data points):
- Hilbert vs Morton vs xxHash
- 5 grid sizes (16^3 to 256^3), 4 trace sizes, 4 patterns

Key findings:
  Morton: 86.5% cache hit rate, 1.08µs p50, 0.512 locality
  xxHash: 30.3% cache hit rate, 0.96µs p50, 0.342 locality
  Hilbert: 27.6% cache hit rate, 2.29µs p50, 0.833 locality

Morton wins overall for spatial hash grids.
 2026-05-30 15:15:33 -05:00
Brandon Schneider
c6011dbbdf feat: wire BraidDiatCodec into FAMM transport 
BraidDiatCodec (714 bytes avg) imported alongside VCN encoder.
When available, can replace Delta+RLE for braid data encoding.

Benchmark (from braid_diat_codec_benchmark.json):
  BraidDiat: 0.029ms encode, 0.034ms decode, 714 bytes
  MessagePack: 0.103ms encode, 0.002ms decode, 1748 bytes
  Cap'n Proto: 0.002ms encode, 0.0001ms decode, 29 bytes

BraidDiatCodec is 2.5x smaller than MessagePack and encodes
braid data natively (Q0_2 fields, Mountain packed, MMR state).
 2026-05-30 14:36:16 -05:00
Brandon Schneider
e797f06bd0 feat(shim): BraidDiatCodec Python extraction 
Python implementation of the 4-layer BraidDiatCodec:
- ChiralityDIAT encode/decode (64-bit slot)
- MountainPacked from_mountain/to_mountain
- BraidResidualPacked from_bracket/to_bracket (Q0_2 packing)
- BraidDiatFrame encode/decode

Benchmark: braid_diat (714B avg) vs messagepack (1748B avg)
on synthetic MMR/spike train frames.
 2026-05-30 13:30:01 -05:00
Brandon Schneider
ba203ca971 feat: spatial hash grid — GPU-style particle physics (Python + FPGA) 
Ported from ScaleSpaceSynth (WebGPU particle simulator):
- 64×64×64 spatial hash, 32 particles/cell, lock-free insertion
- Curl noise: divergence-free 3D turbulence
- Pairwise forces: attractive (ratio>0.15) + repulsive (ratio<=0.15)
- Trilinear density interpolation
- HalfLife particle lifecycle
- Q16_16 encode/decode for VCN transport

Python (spatial_hash_grid.py): 6/6 tests pass
  10K particles, neighbor query, forces, 100 sim steps, curl noise verified

FPGA (spatial_hash_bram.v):
  16×16×16 grid, dual-port BRAM, 27-cycle neighbor scan
  Density → voltage mode selector (STORE/COMPUTE/APPROX/MORPHIC)
  Integrated into research_stack_top.v

Same pattern as ScaleSpaceSynth GPU:
  GPU: atomicAdd for lock-free cell assignment
  FPGA: BRAM read-modify-write for cell assignment
  Ray: content-addressed ObjectRef for lock-free reads
  All: partition space → compute density → find structure at multiple scales
 2026-05-30 01:25:19 -05:00
Brandon Schneider
df6ea7ba15 feat: GCCL + WaveProbe + MetaProbe + delta compression 
Ports Lean formalization to Python:
- GCCL: LawAxis, PromotionRung, Decision, ScaleBand, Receipt, Wrapper, Transition
- gcclSwapGate: accept if new cost < old cost (from MassNumber.lean)
- fammRouteGate: route mass <= stress mass within thermal budget
- braidTransferGate: delta admissible <= delta risk
- WaveProbe: golden angle sampling (40503 = 1/φ × 65536)
- MetaProbe: probe-but-don't-commit, EXPORT_GRANT
- Delta compression with GCCL gates
- gccl_encode: full GCCL-gated encode pipeline

Tests:
  WaveProbe overlap (identical): 1.0000
  WaveProbe overlap (shifted): 0.6694
  MetaProbe (low residual): EXPORT_GRANT
  MetaProbe (high residual): HOLD
  GCCL transition admissible: True

All Q16_16 arithmetic (no Float in compute paths).
 2026-05-30 01:09:14 -05:00
Brandon Schneider
ebabaa3b6b feat: FAMM-integrated VCN transport (gate-checked encode/decode) 
Ports Lean formalization to Python:
- gateCondition: ||coker(M) residual|| < ε (Q16_16)
- Scar/ScarBundle: pressure + mode per strand
- fammGate: admissibility check on 8-strand state
- eigensolid_converged: verify convergence before transmission
- voltage_mode_from_fd: FD → STORE/COMPUTE/APPROX/MORPHIC
- latency_class: RTT → local/near/far/derp/offline

Pipeline:
  Braid data → FAMM gate → eigensolid check → FD → voltage mode
  → RouteCost latency → VCN encode → SEI receipt with FAMM metadata

Gate behavior:
  - FAMM admissible + eigensolid converged → encode
  - Either fails → reject with scar info, don't encode
  - Receipt includes: claim_boundary, promotion=not_promoted

All Q16_16 arithmetic (no Float in compute paths).
68/68 tests still pass.
 2026-05-30 00:56:43 -05:00
Brandon Schneider
e5fb0a5f4d chore: commit accumulated working tree changes 
Lean: update Semantics modules, add new numerics/physics data files
Hardware: update FPGA bitstreams (tangnano9k_uart_loopback)
Infra: k3s-flake tests, netcup-vps configuration, VCN compute substrate
Docs: ARCHITECTURE, specs, citation updates
 2026-05-30 00:10:02 -05:00
Brandon Schneider
9f304abab0 feat: fractal dimension — DBC algorithm (Python + FPGA) 
Paper: 'Ultra-fast computation of fractal dimension for RGB images'
  (Pattern Analysis and Applications, 2025)

Python (fractal_dimension.py):
- DBC algorithm with numpy vectorization (29x faster than scalar)
- fd_compress_hint: FD → voltage mode (STORE/COMPUTE/APPROX/MORPHIC)
- 7/7 tests pass (Sierpinski, random, gradient, checkerboard, fBm, constant, RGB)
- Q16_16 integer arithmetic internally

FPGA (fractal_box_counter.v + fractal_fd_selector.v):
- 5-state FSM: IDLE → COLLECT → FINALIZE → STORE_LOG → REGRESS → DONE
- 8 power-of-two scales (2, 4, 8, ..., 256)
- Linear regression via Q16_16 64-bit arithmetic
- FD clamped to [1.0, 3.0] in Q16_16
- Selector: FD < 2.3 → STORE, < 2.6 → COMPUTE, < 2.9 → APPROX, >= 2.9 → MORPHIC
- Integrated into research_stack_top.v

FD drives adaptive compression:
  Low FD (smooth) → STORE mode (minimal compression)
  High FD (rough) → MORPHIC mode (aggressive compression)
 2026-05-29 20:45:21 -05:00
Brandon Schneider
af2fa96c35 feat(shim): add pylsp_trivial_detector plugin 
Pre-filter plugin for python-lsp-server that handles trivial changes
instantly (whitespace, comments, docstrings, imports, fast syntax errors)
to reduce full analysis overhead. Mirrors the copy_if pattern from
Semantics.CopyIfTactic for Lean.

Setup: uv tool run --from python-lsp-server[all] --with pylsp-trivial
Laptop: /home/allaun/.local/lib/pylsp-trivial
 2026-05-29 13:51:21 -05:00
Brandon Schneider
7047a770d1 feat: AlphaProof batch mode with copy-if pre-filter 
New CLI mode: python alphaproof_loop.py --batch <lean_dir>

Pipeline:
1. Pre-filter scans Lean codebase (11,434 theorems)
2. Classifies trivial (63.5%) vs non-trivial (36.5%)
3. Prioritizes non-trivial by tactic count + sorry weight
4. Feeds hardest problems to Ollama LLM first
5. Skips trivial theorems entirely (zero deltas)

Usage:
  python alphaproof_loop.py --batch ../../0-Core-Formalism/lean/Semantics/Semantics
  python alphaproof_loop.py --batch . --max-iter 20 --model deepseek-coder-v2:16b

Same pattern as vectorized copy_if:
  - Skip zero deltas → 40x faster (blog post)
  - Skip trivial theorems → 2.7x faster (pre-filter)
  - Focus solver on residuals → fewer iterations
 2026-05-29 02:42:04 -05:00
Brandon Schneider
feebe41d14 feat: Lean proof pre-filter (copy-if pattern for compilation) 
63.5% of theorems are trivial (zero deltas) — solver should skip them.
Estimated speedup: 2.7x (11,434 theorems → 4,170 need solving).

Classifies theorems as trivial/non-trivial:
  Trivial: rfl, decide, trivial, alias, constructor, documented sorry, #eval
  Non-trivial: simp, omega, native_decide, ring, linarith, sorry

Top 10 heaviest modules identified (EntropyMeasures has 152 non-trivial).

Usage:
  python3 lean_proof_prefilter.py <file.lean>
  python3 lean_proof_prefilter.py --scan <dir/>

Same pattern as vectorized copy_if:
  - Blog: skip zero deltas in VPCOMPRESSD → 40x faster
  - Lean: skip trivial theorems in simp → 2.7x faster
  - VCN: skip zero deltas in delta+RLE → 3.3x faster
 2026-05-29 02:34:38 -05:00
Brandon Schneider
7237b2e09b feat: vectorized delta+RLE via copy-if pattern (3.3x faster, 2.5x smaller) 
Inspired by loonatick-src vectorized copy_if analysis:
- VPCOMPRESSD memory-dest = 144 microcode uops (40x bottleneck)
- Register-dest compress + regular store = 10-40x faster

Applied to VCN pipeline:
- numpy vectorized delta (np.diff) + copy-if (nonzero mask)
- RLE on filtered stream = concentrated runs = better compression
- Falls back to scalar if numpy unavailable or data < 1024 bytes

Benchmark (800KB random data):
  Scalar:     132.8ms, 499KB output (0.62 ratio)
  Vectorized:  40.2ms, 200KB output (0.25 ratio)
  Speedup: 3.3x, compression: 2.5x smaller

Wire: delta_rle_encode_vectorized() replaces delta_rle_encode() in pipeline
 2026-05-29 02:24:55 -05:00
Brandon Schneider
00e88b53a3 feat(infra): add DSP node schema and flac_dsp_node.py shim 
Any Linux node with PipeWire can act as a FLAC/DSP compute worker
via a virtual sound card — no physical audio hardware required.

- ene.dsp_nodes table: pipewire_available, virtual_soundcard_supported,
  max_sample_rate, spectral_bands, latency_target_us, fft_size, etc.
- flac_dsp_node.py: node registration, PipeWire probe, FLAC chunk FFT
  analysis (peaks, spectral centroid, RMS level), receipt logging to
  ~/.cache/flac_dsp_receipts.jsonl
- AGENTS.md: document DSP volunteer computing schema addition

Build: 0 errors (py_compile)
 2026-05-29 01:31:13 -05:00
Brandon Schneider
73b2c3ba32 feat: particle physics LUT — 50 years of PDG data as Q16_16 BRAM tables 
34 particle masses, 8 decay widths, 11 cross-sections, 8 trigger thresholds,
8 calibration constants — all encoded as Q16_16 integers.

BRAM layout: 4 banks × 256 entries × 32-bit
  Bank 0: particle_masses (electron → upsilon_3S)
  Bank 1: decay_widths (W, Z, Higgs, top, J/ψ, ϒ)
  Bank 2: cross_sections (ttbar, W, Z, Higgs, jets at 13 TeV)
  Bank 3: triggers_calibration (LHC HLT + ECAL/HCAL constants)

Cross-section interpolation: log-log between 7/8/13/14 TeV.
Export: Verilog initial blocks for FPGA BRAM loading.

The LHC trigger system processes 40M events/second using hardware LUTs.
These tables are the same lookup operations — just in Q16_16 fixed-point.
 2026-05-28 19:26:27 -05:00
Brandon Schneider
5698d6e54b feat: Tailscale graceful degradation — chain never fails 
RouteCost.lean:
- latencyClass 4 = 'offline' (Tailscale down/unreachable)
- networkLatencyCost returns qOne for offline (maximum cost)
- Computation continues with local-only fallback

scale_space_solver.py:
- detect_tailscale(): returns available=False if not installed/running
- get_latency_class(): returns 4 (offline) when Tailscale unavailable
- latency_to_voltage/sigma(): map any class to FPGA parameters
- Chain never raises — offline is just another latency class

Verified:
- Tailscale up: 4 peers detected, latency classes assigned
- Tailscale down: returns class 4 (offline), computation continues
- Unknown IP: returns class 4 (offline), no crash
 2026-05-28 19:19:14 -05:00