mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
de06a85a83
Lean sorry audit (lake build passes, 3539 jobs): - FixedPointBridge: 10 sorrys quarantined with TODO(lean-port) — all blocked on Float→Q bridge lemmas (Q0_16/Q16_16 round-trip error bounds) - HyperbolicStateSurface: 3 sorrys quarantined — need Q16_16.sqrt error-bound and Q16_16.add_pos_of_pos lemmas - CostEffectiveVerification: 1 sorry quarantined; also fixed pre-existing struct/structure typo, Array.Repr, Real.abs syntax, and Bool/Prop mismatch - MMRFAMMUnification: 1 sorry quarantined — Array.foldl induction lemma missing - WaveformTeleport: constantWaveformAtFixedPoint_base native_decide was numerically false; replaced with sorry + TODO(lean-port) - RcloneIntegration: startTask_pending_non_increasing PROVED — only sorry fully closed, using List.partition_eq_filter_filter + List.filter_sublist - DiffusionSNRBias, GPUVerificationMetaprobe, QFactor, SSMS: already properly quarantined; verified build passes Infrastructure additions: - ene_wiki_body_reingest.py: 5-source priority resolver for ene.wiki_revisions text="" gap (TiddlyWiki → filesystem → Notion → package description → stub) - zfs-pool-setup.sh: stackcache pool (500G sparse vdev) with hot/warm/cold thermal-zone dataset hierarchy; requires reboot to 7.0.9-1-cachyos kernel Docs: - ROADMAP.md: mark Lean→Verilog/FPGA targets as LONG-TERM in Phase 6 - UNIFIED_SIGNAL_ARCHITECTURE.md: add FPGA-column deferral notice Generated with [Devin](https://cli.devin.ai/docs) Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
96 lines
5.6 KiB
Markdown
96 lines
5.6 KiB
Markdown
# Unified Signal Architecture — DisplayPort × Audio × FPGA
|
||
|
||
**Status:** Architecture — bridges 3 deployed hardware pathways into one texel state machine
|
||
**Deployed components:** HDMI shell, PipeWire waveprobe chain, DSP reconfiguration, braid DSP bridge
|
||
|
||
> **FPGA column (Tang Nano 9K) is LONG-TERM only.**
|
||
> The DisplayPort and PipeWire Audio columns are active/deployed.
|
||
> FPGA bring-up (bitstream synthesis, UART beacon, live hardware receipt) is deferred
|
||
> until the Lean → Verilog extraction pipeline is complete (Phase 6 of ROADMAP).
|
||
> Do not treat the FPGA column as a current dependency or near-term deliverable.
|
||
|
||
## Architecture
|
||
|
||
```
|
||
┌──────────────────────────┐
|
||
│ NUVMAP Texel Stream │
|
||
│ (PIST → Cayley V4 → │
|
||
│ braid/rope encoding) │
|
||
└──────────┬───────────────┘
|
||
│
|
||
┌────────────────────┼────────────────────┐
|
||
▼ ▼ ▼
|
||
┌──────────────────┐ ┌──────────────────┐ ┌──────────────────┐
|
||
│ DisplayPort │ │ PipeWire Audio │ │ FPGA Tang Nano 9K│
|
||
│ 8K@60Hz │ │ 192kHz/24-bit │ │ 27MHz UART/BRAM │
|
||
│ │ │ │ │ │
|
||
│ Lane 0: φ-phase │ │ Left: TSM thermal │ │ V4 Cayley verify │
|
||
│ Lane 1: Aₙ ampl │ │ Right: Waveprobe │ │ Mass preserved │
|
||
│ Lane 2: vᵢⱼ tensor│ │ Center: GCL delta │ │ Triangle gate │
|
||
│ Lane 3: witness │ │ │ │ Chiral state LED │
|
||
│ │ │ VBLANK=SUBTRACT │ │ │
|
||
│ NVENC session 0-7 │ │ HBLANK=PAUSE │ │ DAG-LUT burned │
|
||
│ │ │ FRAME=ADD │ │ │
|
||
│ HPD: ternary clock│ │ │ │ CEC: sync clock │
|
||
└────────┬──────────┘ └────────┬──────────┘ └────────┬─────────┘
|
||
│ │ │
|
||
└──────────────────────┼──────────────────────┘
|
||
│
|
||
┌──────────▼───────────┐
|
||
│ Unified Frame Sync │
|
||
│ │
|
||
│ DP VSYNC = audio │
|
||
│ buffer swap │
|
||
│ │
|
||
│ Frame 0: keyframe + │
|
||
│ full attestation │
|
||
│ Frame N: delta only │
|
||
│ │
|
||
│ VBLANK: TVI samples │
|
||
│ + audio FFT bins │
|
||
│ HBLANK: mistake vecs │
|
||
│ + GCL diff deltas │
|
||
│ DDC: ZK-STARK proof │
|
||
└───────────────────────┘
|
||
```
|
||
|
||
## Unified Timing
|
||
|
||
| Signal | DP 8K60 | PipeWire Audio | FPGA |
|
||
|--------|---------|---------------|------|
|
||
| Period | 16.67ms | 5.21µs (192kHz) | 37ns (27MHz) |
|
||
| Per frame | 33.18M texels | 3,200 samples | 450k cycles |
|
||
| Blanking | VBLANK=45 lines | PAUSE buffer | DAG-LUT write |
|
||
| Active | 4320 lines | ADD buffer | Cayley verify |
|
||
| Sync | HPD Morse | Jack transport | CEC clock tick |
|
||
|
||
## Deployed Verification
|
||
|
||
| Component | File | Lines | Status |
|
||
|-----------|------|-------|--------|
|
||
| HDMI Computational Shell | `scripts/hdmi_computational_shell.py` | 301 | Deployed |
|
||
| DP 8K60 Texel Spec | `docs/specs/DP_TEXEL_8K_ENCODING_SPEC.md` | 116 | Written |
|
||
| PipeWire Waveprobe Chain | `tools-scripts/audio/pipewire_waveprobe_compression_chain.py` | 1,422 | Deployed |
|
||
| DSP Reconfiguration | `scripts/execute_swarm_dsp_reconfiguration.py` | — | Deployed |
|
||
| Braid DSP Bridge | `tools-scripts/braid/braid_dsp_bridge.py` | — | Deployed |
|
||
| Hybrid DSP Test | `tools-scripts/testing/test_hybrid_dsp_deterministic.py` | — | Deployed |
|
||
| V4 Cayley Verification | Lean 4 `CayleyFibergraph.lean` | — | Builds clean |
|
||
| FPGA Invariant Scanner | `cff/fpga/bridge.py` + Verilog | — | Flashed + live |
|
||
| GPU Eigenmass | `cff/gpu/eigenmass_engine.py` | — | CUDA 117ms |
|
||
|
||
## Key Equation
|
||
|
||
```
|
||
Frame[t+1] = bind(
|
||
Frame[t],
|
||
{ DP_lane[0..3] → texel_stream,
|
||
audio_left → waveprobe_score,
|
||
audio_right → tsm_thermal,
|
||
fpga_verify → V4_check },
|
||
{ Δ_frame = H(DP_texels[t]) - H(DP_texels[t-1]),
|
||
Δ_audio = |waveprobe[t] - waveprobe[t-1]|,
|
||
gate = Δ_frame < τ_frame ∧ Δ_audio < τ_audio }
|
||
)
|
||
```
|
||
|
||
The frame is admissible iff both the video texel entropy and audio waveprobe score remain within their Landauer thresholds. The FPGA V4 Cayley check is the hardware witness — if it fires a violation, the frame is quarantined via HPD Morse ABORT.
|