mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00

Brandon Schneider 6679908f7b fix(arch): enforce Lean-first hierarchy across project — remove all secondary-Lean language

Project-wide sweep to find and fix every place Lean was treated as secondary,
optional, or subordinate to Python/Rust. The invariant: Lean is the source of
truth. Python and Rust are extraction targets only; they contain no logic, no
invariant checks, no decisions.

Changes:

1-Distributed-Systems/ene/src/lib.rs
  - CRITICAL: Remove 'Rust is the canonical implementation language for
    operational components' — replace with correct extraction-target framing

1-Distributed-Systems/agents/claw/README.md
  - Remove 'canonical implementation lives in rust/' and 'source of truth is
    ultraworkers/claw-code' blanket claims — scope to CLI binary only;
    add Research Stack domain-logic note (Lean is source of truth per AGENTS.md)
  - 'canonical Rust workspace' → 'Rust workspace (I/O extraction target)'

1-Distributed-Systems/agents/claw/src/Tool.py
  - 'Python-first porting summary' → 'Lean-to-Python extraction summary'

1-Distributed-Systems/agents/claw/src/projectOnboardingState.py
  - python_first: bool = True → lean_first: bool = True (Lean always leads)

6-Documentation/docs/specs/ENE_MEMORY_ATLAS_SPEC.md
  - CRITICAL: 'Python first (reference) ... Lean-formal next' → correct order:
    Lean specification first, Python extraction shim, Verilog hardware extraction

6-Documentation/docs/recovered/geocognition_equation_types_map.mmd
  - 'Lean owns logic; Rust owns boundary' → 'Lean owns all logic and decisions;
    Rust is boundary shim only'

6-Documentation/docs/semantics/HYPER_DIMENSIONAL_PHYSICS_INTRO.md
  - 'Python implementation ... Lean formalization' → 'Lean specification (source
    of truth) ... Python extraction shim'

6-Documentation/docs/geometry/GEOMETRY_TAXONOMY_FOR_NLOCAL_ADAPTATION.md
  - 'reference specification for the Python implementation' → 'source of truth;
    Python is an extraction shim against this spec'

6-Documentation/docs/protocols/TM_MCP_SPECIFICATION.md
  - 'Python reference implementation' → 'Python extraction shim' (×2)

5-Applications/scripts/snn/README.md
  - 'deterministic Python reference' → 'Python extraction shim / golden-vector
    harness'; add TODO(lean-port) note; RTL must match 'Python shim (pending
    Lean golden vector)' not 'Python reference'

6-Documentation/docs/METAPROBE_APPROACH.md
  - 'DeltaGCLCompression.lean — Lean implementation / scripts/delta_gcl_encoder.py
    — Python reference implementation' → Lean is source of truth / Python is
    extraction shim

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:40:03 -05:00

3 KiB

Raw Permalink Blame History

SNN / NII / RGFlow / FAMM Test Harness

Imported 2026-04-24 from external triage pack. Calibration fixes applied on import — see "Calibration deltas" below.

Layout

snn_nii_reference.py — Python extraction shim / golden-vector harness. Pipeline: predict → nii_step (clamp + bounded Δw + decay) → msnn_step (LIF + FAMM-modulated drive) → rgflow_step (3-verdict) → famm_update (saturating + exp decay). Writes per-record JSONL with SHA-tagged hash for golden-vector compare. TODO(lean-port): Port pipeline logic to Lean; Python remains I/O harness only.
generate_snn_vectors.py — 4-phase synthetic stream (stable / drift / repeated bad / near-miss osc) OR pulls from a uc_records.jsonl topology18 stream.
snn_test_config.json — Q8 fixed-point + thresholds.
RTL siblings live at 4-Infrastructure/hardware/tangnano9k/rtl/ and must bit-match this Python shim (pending Lean golden vector).

Quick start

python generate_snn_vectors.py --out vectors.jsonl --n 256
python snn_nii_reference.py --vectors vectors.jsonl --config snn_test_config.json --out results.jsonl --summary summary.json

The reference prints a pass/fail JSON to stdout. All four flags must be true for the run to count: bounded_nii, all_verdicts_present, famm_unsaturated, and any custom hardware-equivalence check.

Calibration deltas (vs upstream pack)

The upstream harness produced a misleading pass_fail: famm_updated: True when FAMM was actually pegged at 255 across all three counters from i≈40 onward — half the run was testing a dead controller. Fixes applied on import:

Exponential FAMM decay (decay_q8 = 232 ≈ 9.4%/step). Replaces the upstream linear -1/step on lawful-only. Time constant ~10 steps, so phase 2's 64 consecutive heavy rejects can saturate momentarily but recover before phase 3.
Reduced reject contribution (rp/8 and rp/16 instead of rp/4 and rp/8). Even with decay, the upstream scaling drove phase 2 to saturation in ~5 events.
Widened near-miss band (32 → 48). Upstream produced 0/256 near-miss events.
Saturation surfaces as failure (famm_unsaturated, famm_saturation_steps, final_famm now in pass/fail JSON). Failure contract: silent saturation is unacceptable, must be observable.

Verified end-to-end after fixes: 189 lawful / 1 near-miss / 66 reject, no counter saturated >25% of the run, max abs surprise 359 ≤ NII clip 384.

Known follow-ups

Synthetic generator phase 3 produces only 1 near-miss event in 64 steps — the σ corridor [262, 293] is too narrow for the current amplitude swings. Either re-tune phase 3 amplitudes or add a fifth phase explicitly designed for the near-miss band.
RTL nii_core.v uses a one-tap obs - prev_obs predictor; the Python reference uses 4 weighted delay taps. They will not bit-match until the RTL is upgraded.

3 KiB Raw Permalink Blame History Unescape Escape