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
574 commits 18 branches 0 tags 425 MiB
Commit graph

153 commits

Author SHA1 Message Date
Brandon Schneider
c73e9c4f02 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
ce0367405b 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
989017aa57 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
1c272eb197 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
c87dfaaea5 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
a2940b7092 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
e7230f47e8 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
10670e2d10 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
c8908036d2 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
7234669ddb 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
6b1e9e5bb0 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
b14cb8ad37 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
547d6ac1de 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
83bbd23331 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
4475bff0be 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
98d48c30d4 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
b54f597690 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
c01ecc469d 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
25f0ec2b53 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
3dace5fe73 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
377f48f6b1 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
36740d65bb 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
0178d5d820 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
c59510196a 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
696e86443d 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
2aef54d052 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
58b95a9814 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
5e12f21fa1 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
48eb892f49 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
42b5f7ea4f 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
2cf52fa913 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
093d8ef43f 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
096a566aaf 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
159ba50059 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
Brandon Schneider
f8554a3736 fix: braid_search.py QUBO/soliton from float to Q16_16 integer arithmetic 
AGENTS.md §1.4 compliance: all internal computation now uses Q16_16 integers.
Float only at HiGHS API boundary and display statements.

- Q16_SCALE = 65536, _q16(), _q16_to_float(), _q16_signed()
- bracket_cost, crossing_penalty, build_qubo_matrix: all int
- soliton_search, qubo_optimize: Q16_16 temperature/energy
- 68/68 tests pass
 2026-05-28 17:47:40 -05:00
Brandon Schneider
d956ac7583 fix: update Sidon tests for Mian-Chowla API (68/68 pass) 2026-05-28 17:06:40 -05:00
Brandon Schneider
6f650be6ab feat: dense Sidon sets from sum-product conjecture disproof 
Mian-Chowla sequence replaces powers-of-2 as default:
- 8 slots: max 128 → 45 (65% reduction)
- 16 slots: max 32768 → 252 (99% reduction)
- All constructions verified as valid Sidon sets

Methods: 'powers_of_2' (old), 'greedy_optimal' (Mian-Chowla, default),
'algebraic' (number field construction for large n).

Based on Bloom-Sawin-Schildkraut-Zhelezov (2026) sum-product disproof.
 2026-05-28 16:57:35 -05:00
Brandon Schneider
2fed2b3e41 feat: HiGHS wired as default QUBO solver in braid_search.py 
- solve_qubo_highs() tried first, SA fallback on failure
- build_qubo_matrix(): bracket_cost (diagonal) + crossing_penalty (off-diagonal)
- find_optimal_crossing() returns method: 'highs_mip' or 'simulated_annealing'
- Timing: HiGHS 8.4ms vs SA 53.5ms (6.4x speedup)
 2026-05-28 16:35:05 -05:00
Brandon Schneider
5979046715 feat: optimized route proof + scale space solver fix 
Lean:
- OptimizedRoute.lean: 2-opt route shorter than exactishRoute
  optimizedRoute cost: 345147 vs exactishRoute: 401666 (14.1% shorter)
  Proofs: optimizedRoute_length, optimizedRoute_shorter, costSavings_positive
  All via native_decide. lake build: 3571 jobs, 0 errors.

Python:
- scale_space_solver.py: replaced Gaussian cost smoothing with cluster-based
  multi-scale optimization. Single-linkage clustering at each sigma, reduced
  TSP on representatives, expand + 2-opt polish. Fixed voltage/scale mapping.
 2026-05-28 15:53:28 -05:00
Brandon Schneider
ea3eedef77 feat: HiGHS integration, scale space solver, adjugate matrix, FPGA voltage/BRAM modules 
HiGHS Optimization:
- qubo_highs.py: QUBO→MIP reformulation via highspy (exact, not approximate)
- solve_route_lp: TSP/VRP assignment relaxation for RouteCost 39-node graph
- scale_space_solver.py: multi-scale optimization (coarse LP → fine MIP)
- Gaussian kernels in Q16_16, voltage↔scale mapping
- alphaproof_loop.py: Ollama → lake build → feedback proof search

Lean Formalization:
- AdjugateMatrix.lean: division-free matrix inversion (291 lines, 3300 jobs, 0 errors)
- det2/det4/det8 via cofactor expansion, all Q16_16
- adjugate, matrixInverse, cayleyTransform
- 7 #eval witnesses all pass

FPGA (Tang Nano 9K):
- voltage_mode_controller.v: 4-mode BRAM (STORE/COMPUTE/APPROX/MORPHIC)
- scale_space_bram.v: 4 Gaussian kernel banks (σ=0.25/0.50/0.75/1.00)
- highs_pivot_accelerator.v: 3-stage pipeline, Q16_16 division, 64-element columns
- blitter_memory_map.v: 8-bit CPU ↔ 32-bit Q16 bridge, full I/O map at $8000
 2026-05-28 15:42:14 -05:00
Brandon Schneider
a3b298230b feat: wire pipeline into VCN substrate + FPGA bitstream for Q16 LUT 
Pipeline wiring:
- vcn_compute_substrate.py: Delta+RLE → RS ECC → ChaCha20 now in live path
- encode_braid_strand/crossing/mountain_merge accept key + compress params
- New CLI: encode_enhanced/decode_enhanced for full pipeline
- 67/67 tests pass

FPGA synthesis:
- q16_lut_core → Tang Nano 9K (GW1NR-9C)
- 266 LUTs, 68 FFs, 2 DSPs, 1 BRAM
- 3.4MB bitstream (q16_lut_top.fs)
- Constraint file + build script + wrapper module
 2026-05-28 15:02:13 -05:00
Brandon Schneider
e0df130453 feat: 12 math enhancements — Q16 LUT, braid VCN encoder, FPGA Verilog, FFT, crypto 
Pipeline:
- q16_lut_vcn.py: Q16_16 LUT generation + VCN frame encoding (8 ops)
- braid_vcn_encoder.py: Delta+RLE → RS ECC → ChaCha20 → VCN → MKV
- braid_search.py: Sidon set slots, soliton search, QUBO optimization
- test_braid_pipeline.py: 67 tests covering full round-trip

WebGPU/Scripts:
- braid_fft.wgsl: Cooley-Tukey radix-2 FFT on phase vectors
- reed_solomon_vcn.py: Reed-Solomon ECC for VCN frame data
- chacha20_braid.py: ChaCha20 encryption + key derivation
- polynomial_commitment.py: KZG scheme for receipt verification

Lean:
- BraidBitwiseODE.lean: XOR crossing, O(1) integration, 2 proved theorems

FPGA (Tang Nano 9K):
- q16_lut_core.v: 8-op arithmetic, 2-stage pipeline, BRAM reciprocal
- braid_crossing_core.v: 4-stage crossing residual, 7 Q16 instances
- Testbenches with edge cases + VCD dumps
 2026-05-28 14:49:26 -05:00
Brandon Schneider
d86625e220 feat(infra): cluster dashboard + VCN shim indentation fix 
- Add LyteNyte Grid cluster dashboard (React + FastAPI + k3s)
  - Real-time telemetry: GPU util/VRAM/temp, CPU/memory, pod counts,
    Tailscale connectivity, OS/kernel info for all 5 cluster nodes
  - WebSocket live updates every 3s, dark theme, virtualized grid
  - k3s deployment with hostNetwork, NodePort 30820, SSH-based collectors
  - Backend uses /proc/stat + /proc/meminfo for portable NixOS metrics
  - Tailscale status via SSH to host (container doesn't run tailscaled)
- Fix vcn_compute_substrate.py indentation (lines 45-269 had 1 extra
  leading space). Script now compiles and runs encode/decode/receipt.

Build: py_compile OK, npm build OK, podman build OK
 2026-05-28 01:13:54 -05:00
Brandon Schneider
92bc00c4d5 feat(lean): complete goldenContractionEnergyDecrease proof + PIST predictions pipeline v2 
- PistSimulation.lean: proven goldenContractionEnergyDecrease (no sorry)
  7 supporting lemmas, h_u'_nonneg + h_pt hypothesis, fold induction
- Connectors.lean: restored zeroIsVoid theorem with Q16_16 proof
- CanonSerialization.lean: removed dead theorem, documented blocker
- FixedPointBridge.lean: eliminated Float from compute paths

PIST predictions pipeline:
- pist_matrix_builder.py: reproducible matrix-only builder (SHA256)
- build_pist_matrices_278.py: generates PIST/Matrices278.lean
- PIST/Classify.lean: classifyProxy/classifyExact stubs (v2 surface)
- PIST/Matrices278.lean: 250-entry matrix HashMap
- build_corpus278.py: reads predictions artifact, uses classify*
- Pipeline contract documented in root AGENTS.md

Cleanup:
- Archived 5 orphan pist_* shims, 5 old route_repair variants
- Quarantined PIST/Repair.lean (no external callers)
- Created 4 opencode agents for remaining TODO items

Build: PistSimulation 3309, Compiler 3313, Full 3571 (0 errors)
 2026-05-27 12:40:16 -05:00
Brandon Schneider
36b5b6914e feat(lean): wire 278-equation corpus end-to-end; emit emit278.json 
- AVMIsa/Emit §7: fix emitRrcCorpus278 JSON structure (summaryStr
  sub-object + classified.rowsJson instead of nested classified.json);
  add #eval emitRrcCorpus278 witness (line 261)
- RRC/Emit §8: add rowsJson field to EmitResult (flat JSON array of
  rows, usable by outer envelope builders without re-serializing)
- 4-Infrastructure/shim/emit278_extract.py: new extractor — runs
  lake build Semantics.AVMIsa.Emit, captures #eval output, strips
  Lean repr escaping, validates JSON, writes
  shared-data/data/stack_solidification/emit278.json
- emit278.json: 278 rows, schema=avm_rrc_corpus278_v1,
  avm_canaries_passed=true, bundle_receipt_valid=true,
  claim_boundary=admissibility-and-routing-pass-only;not-promoted
  (all 278 rows missing_prediction — no PIST labels supplied yet)
- Full lake build: 3570 jobs, 0 errors

Generated with [Devin](https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-27 00:11:55 -05:00
Brandon Schneider
bdc98e2a0e feat(lean): port pist_trace_classify motif scoring to Semantics.PIST.Motif 
Ports the motif scoring surface from pist_trace_classify_mcp.py (lines 136–149)
into a provable Lean module:

  score = frequency / max(library_size, 1) + (0.3 if tactic_family matches)

New module: Semantics.PIST.Motif (201 lines)
  §1  familyMatchBonus constant (ofRatio 3 10 = 19660 raw)
  §2  MotifInputs, baseScore, motifScore
  §3  MotifCandidate record, mkCandidate constructor
  §4  rankMotifs / topKMotifs (mergeSort desc, motifId tie-break)
  §5  8 executable #eval witnesses with -- expect: annotations
  §6  6 proved invariants:
      motifScore_bonus_pos (decide)
      motifScore_match_ge_base_witness (decide, concrete)
      motifScore_zero_freq_base (simp)
      motifScore_zero_freq_no_match (simp)
      motifScore_zero_freq_match_witness (decide, concrete)
      rankMotifs_match_beats_no_match (native_decide — mergeSort sort witness)

Full workspace build: 3570 jobs, 0 errors.

pist_trace_classify_mcp.py PARTIAL BOUNDARY updated: motif score + rank order
now explicitly point to Semantics.PIST.Motif as authoritative.

Generated with [Devin](https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-26 23:45:07 -05:00
Brandon Schneider
34f58d12d9 feat(lean): port route_repair_v14a rank_patches to Semantics.PIST.Repair 
Ports the decision-critical scoring functional from route_repair_v14a.py
into a provable Lean surface:

  rank_patches: S = α·specificity − β·cost + γ·success_prior − δ·residual_risk
  ALPHA=0.4, BETA=0.3, GAMMA=0.2, DELTA=0.1  (all as Q16_16.ofRatio)

New module: Semantics.PIST.Repair (232 lines)
  §1  PatchScoreInputs, PatchWeights structures
  §2  rankScore (linear functional), rankScoreDefault, mkInputs, embedResidualRisk
  §3  Patch record + mkPatch constructor
  §4  rankPatches / rankPatchesDefault (mergeSort desc, tag tie-break)
  §5  5 executable #eval witnesses with -- expect: annotations
  §6  8 proved invariants (native_decide):
      defaultWeights_sum, defaultWeights_pos, defaultWeights_ordered,
      rankScore_zero_inputs_negative, embedResidualRisk_one/zero,
      rankScore_monotone_specificity_witness, rankScore_zero_lt_full

Full workspace build: 3569 jobs, 0 errors.

route_repair_v14a.py PARTIAL BOUNDARY comment updated to name this module
as the authoritative source for the scoring surface.

Generated with [Devin](https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-26 23:32:36 -05:00
Brandon Schneider
8ee3d431d2 feat(lean): port pist_trace_classify_mcp spectral logic to Semantics.PIST.Spectral 
## New module: Semantics.PIST.Spectral

Ports the two domain-logic functions from pist_trace_classify_mcp.py
that were previously executing in unverified Python:

### classify_tactic_from_name → classifyTacticFromName
- `TacticFamily` inductive (rewrite, normalization, arithmetic, induction,
  algebraic, case_analysis, discharge, reflexivity, unknown)
- Pure string-lookup; 5 executable witnesses confirm all branches.

### compute_spectral → computeSpectral
- `isqrt` — integer Newton's method for floor(√n); 4 witnesses.
- `powerIteration` — Q16_16 fixed-point dominant eigenvalue via power
  iteration with Rayleigh quotient; identity-matrix witness = 65536.
- `SpectralProfile` structure — 10 fields (matrix_size, rank,
  spectral_gap, density, trace_val, frobenius_norm, laplacian_zero_count,
  adjacency_eigenvalue_max, laplacian_eigenvalue_max, singular_value_max).
- `computeSpectral` — symmetrize → lap → powerIteration → shift-deflation
  for second eigenvalue → AᵀA for singular value; 3 witnesses on 2×2 fixture.

No Float in any compute path. All magic constants documented with formulas.

## Other changes
- Semantics.lean: add `import Semantics.PIST.Spectral`
- AgenticOrchestration.lean:163: expand bare `-- TODO(lean-port):` label
- pist_trace_classify_mcp.py: update PARTIAL BOUNDARY comment to name
  the Lean module that now owns spectral logic

## Build baseline
  lake build Compiler → 3311 jobs, 0 errors

Generated with [Devin](https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-26 23:25:50 -05:00
Brandon Schneider
f9b5ac25fb fix(lean+shim): enforce lean-coding rules across audit surface 
## Lean fixes

- RRCLogogramProjection.lean: replace `native_decide` → `decide` in 5
  compiler-surface theorem witnesses (semantic_tear_projects_after_repair,
  semantic_tear_does_not_merge, semantic_tear_uses_quarantine_lane,
  unrepaired_tear_does_not_project, ordinary_logogram_projects_and_merges).
  All 5 pass under `decide`; no logic change.

- PistSimulation.lean: add `-- expect: <value>` to every `#eval`/`#eval!`
  block across §6–§11 (~104 annotation lines). Document 8 undocumented
  `ofRawInt` magic integers in fixtureSpectralWindow (10.0, 20.0, 100.0,
  40.0, 20.0, 10.0, 5.0, 5.0 × 65536).

- DynamicCanal.lean: add `-- expect:` to all 15 #eval witness blocks in
  §17 (fixed-point constructors, DIAT encoding, coarse-graining tests).

- MISignal.lean: add `-- expect: 131072` to both #eval witnesses.

- Functions/BracketedCalculus.lean: add `-- expect: 327680` to #eval.

- AVMIsa/Emit.lean, RRC/Emit.lean, RRC/ReceiptDensity.lean, ReceiptCore.lean:
  previously-staged `-- expect:` additions (from prior session) carried
  forward in this commit.

## Python shim fixes

- Add `# PARTIAL BOUNDARY: contains domain logic; not a provable surface.
  Port to Lean/RRC before treating as authoritative.` to 9 shim files:
  pist_trace_classify_mcp.py, genus0_sphere_shell_demo.py,
  routing_benchmark.py, route_repair_v14a.py, pist_prove_and_classify.py,
  label_canary_theorems.py, validate_rrc_predictions.py,
  pist_receipt_density_injector.py, rrc_pist_shape_alignment.py.

## Build baseline

  lake build Compiler  →  3311 jobs, 0 errors
  lake build           →  3567 jobs, 0 errors

Generated with [Devin](https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-26 23:17:40 -05:00
Brandon Schneider
d1017fbbbd feat(lean): port receipt-density scoring to Semantics.RRC.ReceiptDensity 
Adds Semantics/RRC/ReceiptDensity.lean — a new Lean module that ports
the entire scoring pipeline from pist_receipt_density_injector.py into
Lean-native Q16_16 fixed-point arithmetic:

  spectralQuality   ← spectral_quality()   (0.24/0.18/0.18/0.12/0.12/0.16 weights)
  shapeAgreement    ← shape_agreement()    (exact=1.0, proxy=0.82, any=0.35)
  axisScore         ← axis_score()         (hits/4, capped at 1.0)
  statusScore       ← status_score()       (BLOCKED=0, HOLD=0.12 … VERIFIED=0.84)
  computeDensity    ← compute_density()    (density: 26/24/26/24, confidence: 20/20/28/32)

No Float in compute paths — all arithmetic is Q16_16 (raw Int, scale=65536).
Two #eval witnesses verify CANDIDATE/VERIFIED case outputs.

Build: lake build Compiler → 3311 jobs, 0 errors (baseline preserved).

Update shim BOUNDARY comments:
  pist_receipt_density_injector.py → Semantics.RRC.ReceiptDensity
  rrc_pist_shape_alignment.py      → Semantics.RRC.Emit

Generated with [Devin](https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-26 22:48:55 -05:00