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

57 commits

Author SHA1 Message Date
allaun
5d6a4765fc feat(docs): architecture and speculative materials updates 
- 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.
 2026-06-21 01:04:19 -05:00
allaun
2f011c08fb feat(lean): Chentsov->Finsler->QUBO->QAOA routing bridge 
Chentsov's theorem forces the Fisher metric; Finsler-Randers generalizes
with asymmetric drift beta; QUBO discretizes the geodesic; QAOA solves it.

- TransportQUBOBridge.lean (new, 0 sorries, 2 axioms with TODO(lean-port)):
  randersMetricToQUBO, geodesicAssignment, isAnisotropic bridging
  TransportTheory.RandersMetric -> EntropyMeasures.QUBOFormulation.
  Two Q16_16 lemma boundaries: add_self_eq_zero_iff, cost_nonneg.
- computeAlphaCost_neg / computeBetaCost_neg lemmas added to TransportTheory.lean
  (alpha symmetric, beta antisymmetric under direction negation).
- qaoa_adapter.py section III-D: FinslerMetric dataclass + finsler_metric_to_qubo()
  conversion + finsler_demo CLI (verified: anisotropic pair Q_01=0.927, Q_10=0.0).
- docs/chentsov_finsler_qubo_routing.md: full 4-layer pipeline formalization.
- AGENTS.md updated: TransportQUBOBridge in blessed surface + pending proof work.

Build: lake build Semantics.TransportQUBOBridge -> 0 errors, 0 sorries
 2026-06-21 00:32:23 -05:00
allaun
14cde6d09c docs: refresh READMEs, AGENTS.md, and project maps for recent Lean surface 
- Update README.md and 0-Core-Formalism/README.md with build baseline
  (3314 jobs, 0 errors) and new modules (SDPVerify, GoormaghtighCert,
  Hachimoji, SieveLemmas, InteractionGraphSidon, GeneticBraidBridge)
- Update AGENTS.md and 0-Core-Formalism/lean/Semantics/AGENTS.md blessed
  surface tables and build baselines
- Add 6-Documentation/PROJECT_MAP.md and update existing project maps
  (MATH_MODEL_MAP*, LEAN_PORT_ORCHESTRATION_MAP, SIDON_FAMM_MAP,
  BEGINNERS_MAP) with new components and Gremlin mathblob graph loader
 2026-06-20 20:34:09 -05:00
allaun
d63f33fc93 docs(research): path forward for RRC unsolved-problems survey 
- Strategic options and 3-stage roadmap
- Leverage-point analysis and top-10 ranked problems
- Lean stub plan for 7 formalizable problems, 4 deferred
 2026-06-20 19:27:20 -05:00
allaun
514bf8da72 docs(research): RRC survey of 67 unsolved hard problems and alignment clusters 
- 68 problem records (67 unsolved + 1 solved boundary marker)
- 10 alignment clusters spanning number theory, complexity, geometry,
  topology, analysis, logic, physics, and cosmology
- 30×30 crossing matrix of known reductions, shared techniques, and analogies
- RRC shape/axis tags consistent with existing rrc_equation_classification.md
- JSON validated
 2026-06-20 19:12:13 -05:00
allaun
b038778361 feat(lean): SDPVerify, GoormaghtighCert, Hachimoji modules; Gremlin mathblob graph loader; branch cleanup 
- SDPVerify.lean: certificate verification engine (714 lines, compiles cleanly)
- GoormaghtighCert.lean: Goormaghtigh conjecture SDP certificate
- HachimojiManifoldAxiom/HachimojiSubstitution: Hachimoji DNA encoding
- GeneticBraidBridge.lean: genetic algorithm braid bridge
- load_dependency_graph/load_module_graph: Gremlin Cosmos DB graph loaders
- test_graph_queries/rrc_math_xref: graph verification queries
- Gremlin mathblob DB provisioned and accessible
- Branch cleanup: deleted 11 stale remote branches

Build: 3297 jobs, 0 errors (lake build Semantics.SDPVerify)
 2026-06-19 23:06:16 -05:00
allaun
b6f088d9f1 docs(rrc): add topological braid adapter spec for fibonacci anyons 
Define the mathematical isomorphism between the existing compiler concepts (ColorRope, stairIndex, tensegrityCoherent, phi_pow, Zeckendorf bits) and the Fibonacci anyon braiding/fusion algebraic coordinates.

Build: 0 jobs, 0 errors (lake build - no code changes)
 2026-06-18 22:28:50 -05:00
allaun
558431fc45 feat(lean,infra): Corpus278→250 rename + SLOS-calibrated braid defaults 
- Renamed Corpus278/Matrices278 to Corpus250/Matrices250 across all
  Lean modules, Python shims, JSON schemas, and documentation
- Applied SLOS-calibrated defaults to braid_search.py:
  bracket_cost base=8x/16x, crossing_penalty gap_reward=0.01
- Synced same defaults to research-compute-fabric submodule
- Updated Burgers 0D defaults: nu=0.9995, advection=0.075
- Fixed 278→250 refs in pist_predictions JSON (claim_boundary, total)
- Fixed stale schema refs in .devin/skills/lean-proof/SKILL.md
- Updated AGENTS.md build baselines to post-clean counts (3314 jobs)
- Updated lake-manifest.json sparkle rev to match lakefile.toml
- Fixed Q16_16 signed conversion bug in qaoa_adapter tunable costs
- NBody.lean: pre-existing dirty changes (introN failures, NOT our work)

Build: 3314 jobs, 0 errors (lake build Compiler)
 2026-06-18 22:16:52 -05:00
allaun
77488ac0ae feat(lean): close gaussian_line_integral_unit_dir + consolidate infrastructure 
Lean proof fixes:
- N3L_Energy.lean: fully close gaussian_line_integral_unit_dir (nlinarith+hab
  for unit-circle quadratic, sqrt_mul+neg_div for integral_gaussian_1d match,
  exp_sum_of_sq order fix, add_assoc for h_gauss_shift, sq_sqrt for field_simp,
  sq_abs for perpDistance hd)
- Add Adapters/AlphaProofNexus: 12 Erdos/graph adapter stubs (AlphaProof nexus)
- Add Adapters/ErgodicAdditive.lean, SidonMatroid.lean
- Add AntiDiophantine.lean, EffectiveBoundDQ.lean, PVGS_DQ_Bridge.lean
- Add FormalConjectures/Util/ProblemImports.lean
- Add RRC/EntropyCandidates/Candidates.lean
- Add OTOM external project (lakefile.toml, lake-manifest.json, lean-toolchain)

Infrastructure:
- Add 4-Infrastructure/shim/: 17 Python probes (RRC manifold, Sidon kernel,
  Wannier, arxiv harvest, math_symbols DB, coverage density, geometric entropy)
- Add 4-Infrastructure/NoDupeLabs/: Node server + package files
- Add 6-Documentation/docs/specs/DP_RRC_RECEIPT_ENCODING_SPEC.md
- Add fix_offloat.py

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
 2026-06-18 16:53:23 -05:00
allaun
00e9eed399 fix(lean): complete projectionOrdering proof in GeometricCompressionWorkspace 
Replace the TODO(lean-port) sorry with a complete proof of the
projectionOrdering theorem: for positive SourceValue pairs s1 < s2
with s2 ≤ maxExpected, projectToCoding preserves strict ordering
of the Q0_64 values.

The proof uses Nat-only arithmetic (no Float) and handles two cases:
  - a2 < d: both values fit in Q0_64 range, ordering follows from
    monotonicity of integer division
  - a2 = d: a2*s/d = s clamped to q0_64MaxRaw; a1*s/d < q0_64MaxRaw
    via the key inequality (d-1)*s < (s-1)*d

Build: 8598 jobs, 0 errors (lake build)
 2026-06-18 15:06:50 -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
0085136c31 docs: compiled Burgers equation set — Sidon + DualQuaternion with pluggable inputs 
Shows the full architecture as a self-contained equation spec:
- DualQuaternion = 8 components (Sidon-labeled 2^0..2^7)
- BurgersState -> DualQuaternion mapping (pluggable per PDE variant)
- Viscosity = scalar multiplication, advection = group rotation
- 4 theorems all native_decide, kernel-verified
- How to add a new PDE variant in ~24 lines, inheriting all proofs
 2026-06-16 20:15:19 -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
Brandon Schneider
7c1f690e0f feat(infra): Garage 6-node RF3 cluster, Cloudflare Workers deploy, k3s node additions 
- Garage scale-out complete: 6 nodes across 6 zones with replication_factor=3
- neon-64gb: added to Garage cluster (zone netcup-arm, 93 GiB)
- steamdeck: installed Garage v2.3.0, added to cluster (zone gpu, 373 GiB)
- nixos-laptop: converted from k3s server to agent in cupfox cluster
- qfox-1: k3s agent rejoined cupfox cluster
- Cloudflare Workers: WASM trinary VM deployed at wasm-compute-edge.researchstack.workers.dev
- node-registry.json: updated with all 6 Garage nodes
- Documentation: AGENTS.md, WIKI.md, ROADMAP.md, LLM-Context.md updated
- Lake build: 3313 jobs, 0 errors

Build: 3313 jobs, 0 errors (lake build Compiler)
 2026-05-31 03:39:11 -05:00
Brandon Schneider
f38b8cabed docs: hyperlink 50x claim to VCN Pipeline compression table 2026-05-30 20:55:06 -05:00
Brandon Schneider
ae27721a03 docs: update wiki with VAAPI, FLAC DSP, tier limitations, Cloudflare/GitHub 2026-05-30 20:52:58 -05:00
Brandon Schneider
b2414355d1 docs: comprehensive wiki — full architecture reference (May 2026) 
512-line wiki documenting the entire Research Stack:
  1. Architecture Overview (5-layer stack)
  2. Compute Tiers (GPU_CUDA through OFFLINE)
  3. Infrastructure (k3s, Tailscale, KubeRay)
  4. VCN Pipeline (50x compression)
  5. Ray Integration (FrameDispatcher over Ray)
  6. Device Capability Probe (multi-GPU, framebuffer fallback)
  7. Compute Surfaces (GPU, Ethernet, framebuffer, ESP32)
  8. Mesh Networking Plan (Ray over Tailscale)
  9. Formal Verification (23 Lean files, 12 sorries)
  10. Key Files + Quick Reference
 2026-05-30 20:11:58 -05:00
Brandon Schneider
bc9b592dbe docs(infra): update public documentation for virtualized DMA compute backplane 
- Promote the expanded Virtio-Net Packet-as-Computation (PIST) and QEMU graphics backplane spec from the artifacts directory to 6-Documentation/docs/specs/.
- Update root README.md to highlight virtualized DMA computation fabrics.
- Expand 6-Documentation/INFRASTRUCTURE.md to detail host GPU/APU auto-profiling, lossless color ranges, and framebuffer packing shims.
- Keep AGENTS.md aligned with core surfaces.

Build: 3313 jobs, 0 errors (lake build)
 2026-05-30 19:51:24 -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
e203a5215e feat(hardware): Emergency Boot Witness reference implementation 
Add compiling Lean modules and Python shim for the Geometry Emergency
Boot Witness specification (graphene supercapacitor geometric encoding).

Lean modules (Semantics.Hardware.EmergencyBoot.*):
- EmergencyBootTypes: HexCoord, CapClass, OpticalPath, VoltageDifferential,
  GrapheneMemristor, HybridOpticalPath, material properties
- EmergencyBootState: PowerState, SolarPowerState, ScanState, seed assembly,
  emergency boot state machine with 6502 calculator efficiency targets
- EmergencyBootShell: Command opcodes, status byte encoding, process
  definitions, executeCommand dispatch

All use Q16_16 fixed-point arithmetic (no Float in compute paths).
Verified theorems: utilizationWithinBounds, powerFailureMonotonic,
commandOpcode_roundTrip.

Python shim (4-Infrastructure/hardware/emergency_boot/):
- EmergencyBootEngine simulating FPGA geometric scan and seed extraction
- Demo CLI showing power failure → self-powered calculator mode →
  geometric scan → seed assembly flow

Build: 3302 jobs, 0 errors (narrow target), 3313 jobs, 0 errors (Compiler)

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

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-27 23:00:39 -05: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
Brandon Schneider
3044f36df7 docs(agents): project-wide AGENTS.md audit — cross-refs, baseline, contracts 
Actions taken from 5-agent audit sweep (audit date 2026-05-26):

AGENTS.md / docs sync:
- root AGENTS.md: add scripts/qc-flag and lean_expert_agent to Nested Contracts
- All 6 nested AGENTS.md files: append Cross-References section pointing to
  root for Post-Interaction Workflow, Programming Choice Flow, Do Not Sweep,
  Git Remote Hygiene (Lean, Infra, text-to-cad, docs, qc-flag, lean_expert_agent)
- 6-Documentation/docs/AGENTS.md: cross-ref also lists AVMIsa.Emit sole output
  boundary and Compiler surface blessing

Lean build baseline:
- 0-Core-Formalism/lean/Semantics/AGENTS.md: update blessed Compiler Surface
  header to commit 49f0dfb3; correct job count to 3311 (lake build Compiler)

ARCHITECTURE.md:
- §7 repo table: add RRC.Emit, AVMIsa.Emit, RRC.Corpus278 to Lean/Semantics entry
- New §7.1 Compiler Surface: documents 3-root pipeline and sole output boundary
- §4 Data Flow: annotate output with AVMIsa.Emit sole-boundary note

TODO_MAP.md:
- Phase A6: add 3 new Lean deliverables (Corpus278, RRC.Emit, AVMIsa.Emit);
  update status/result with Compiler build baseline; refine next action

Build: Compiler 3311 jobs, 0 errors (no Lean changes).

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:34:46 -05:00
Allaun Silverfox
2c725fb6fd docs: add Lean-first boundary contract (Lean vs shims, receipts, float ban) 2026-05-26 17:31:54 -05:00
Allaun Silverfox
6d73a1b251 docs(avm): strengthen float prohibition and documentation requirement 2026-05-26 16:02:05 -05:00
Allaun Silverfox
1b6f58c5ce docs(avm): add stripping policy and bad-code elimination rules 2026-05-26 15:59:41 -05:00
Allaun Silverfox
3b4ee97588 docs(avm): redefine AVM as Lean-only ISA with adapter shims/backends 2026-05-26 15:58:25 -05:00
Allaun Silverfox
07c31da663 docs: add RRC PIST shape-alignment phase 2026-05-26 15:47:19 -05:00
Allaun Silverfox
34c82705b5 docs: add receipt-density verification sequence 2026-05-26 15:19:07 -05:00
Allaun Silverfox
d18b414ea0 docs: add PIST receipt-density backfill guide 2026-05-26 14:46:55 -05:00
Allaun Silverfox
c9ff24e5f0 docs: add PIST route-repair and receipt update 2026-05-26 14:36:15 -05:00
Brandon Schneider
073a70eb86 WIP: accumulated changes 2026-05-25 16:24:21 -05:00
Allaun Silverfox
99d3edfcb5 Add Talagrand convexity fold-in note 2026-05-23 02:53:19 -04:00
Allaun Silverfox
eeb7d217d0 Add Auro Zera modular-cover audit note 2026-05-23 02:47:25 -04:00
Brandon Schneider
546783faaf docs: add external research import maps 2026-05-20 18:41:21 -05:00
Brandon Schneider
4b828e369c ROADMAP.md: correct 9 phantom/stale claims flagged by review agents 
**CRITICAL fixes**
- Header: note UNIVERSAL_SUBSTRATE_ROADMAP.md no longer exists on disk;
  add note that TODO_MAP.md may lag this file
- §11: replace dead cross-reference with accurate statement; mark full
  census reconstruction as Phase 0 deliverable
- Phase 0: split into completed infrastructure vs pending Lean work;
  explicitly note `USTSM_State` does not yet exist in any Lean file

**ERROR fixes**
- §1: retract unverified "2,634 models" figure; replace with measured
  1,126 ingested equation rows (source: equations.csv 2026-05-18)
- §6 Invariant 7: clarify Q0_64 universality is a Phase 0-1 design
  goal, not a current enforced fact; note Bind.lean uses Q16_16
  exclusively by design ("all values require integer component for
  gradient computation") — no contradiction, different scopes
- §8: expand Semantics/Semantics description to reflect 946+ entries
  (not a handful of named modules); update §4-Infrastructure/infra/
  description to reflect Rust-only state (Python shims removed)
- §12 Credential Gateway: remove reference to deleted credential_server.py;
  credit rs-surface binary and credential.rs module

**WARNING fixes**
- §10 FPGA Hardware: change ✅ Synthesized → 🔄 Bitstream ready; add
  "live hardware receipt pending" caveat
- Phase 4 heading: rename to clarify concurrent-with-Phases-2-3; add
  explanatory note

**BLOCKED annotation**
- Immediate action #8 (Flash Tang Nano 9K): mark as blocked on physical
  board + USB programmer

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

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-19 17:04:45 +00:00
Brandon Schneider
4d715908fd docs: full documentation + roadmap refresh (2026-05-19) 
- CHANGELOG: add 2026-05-09 through 2026-05-19 entry covering Lean
  hardening, storage stack, 20+ new gates, physics RG suite
- ROADMAP: update layer model (746 modules, 3529 jobs, 0 errors);
  mark eigensolid_convergence proven; add section 12 (Infrastructure
  & Data Layer) covering ENE RDS, Garage S3, storage agent, devcontainer
- TODO_MAP: add B11 (eigensolid convergence, DONE), Phase I (infra),
  Phase J (adversarial gates); rename old Phase I to Phase K
- README: update Lean module/build counts; add Infrastructure table
- ARCHITECTURE: update L0 row; add repository structure rows for
  ene-rds, storage, devcontainer; add sections 11-13 (Storage &
  Persistence Layer, ENE RDS Workspace, Braid Eigensolid Compressor)
- CONCEPTS: add Braid Eigensolid Compressor, Constrained Agent
  Framework, and Garage S3 Storage Stack concept entries
- 4-Infrastructure/README: rewrite to reflect ENE RDS Rust workspace,
  restic/Garage/rclone storage stack, storage agent, GPU dispatch,
  adversarial harnesses

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

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-19 09:12:16 +00:00
Brandon Schneider
fd863af6fd Expand devcontainer with full Python stack, add MCP servers (Notion/AWS), strengthen Lean theorems 
- .devcontainer/Dockerfile: add PostgreSQL client libs, OpenSSL/libffi headers, gfortran/BLAS for scipy, rclone; install full Python dependency set (boto3, psycopg2-binary, fastapi, uvicorn, notion-client, httpx, pytest, numpy, scipy, etc.) in uv-managed venv; add rclone S3 gateway init script as ENTRYPOINT
- .devcontainer/devcontainer.json: switch from build to pre-built image (localhost/research
 2026-05-19 01:52:14 -05:00
Brandon Schneider
de06a85a83 Quarantine sorry blocks, fix RcloneIntegration proof, add ENE wiki re-ingest and ZFS setup. 
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>
 2026-05-18 23:01:44 -05:00
Brandon Schneider
5a763468c9 integrate infrastructure config, axiom cleanup, and documentation updates 
- cupfox-config.nix: add Open WebUI container with chat.researchstack.info proxy,
  gather-metrics service/timer, rclone, and tmpfiles for persistent storage
- Lean semantics: reduce axiom count from 109 to 18 across 10 files;
  FixedPoint now 0 axioms, 0 sorries with 12 theorems
- Documentation: update AGENTS.md with current axiom/sorry counts and
  FixedPoint status; refine bind signature
- Add topology scripts, CGA/FAMM/GeneticOptimizer/MMRFAMM Lean modules,
  devcontainer config, MEMORY.md, and Modelfile
 2026-05-17 12:03:19 -05:00
Brandon Schneider
b5139fb484 docs(system): separate FRT core from personal software inventory 
Provide two lists for clean system recovery:

- frt-core-packages.txt: 90 packages required to build, verify, and run
  the Research Stack (VITAL + NEEDED tiers). Install first on fresh system.

- personal-packages.txt: ~200 packages that are NOT required for FRT work.
  These are quality-of-life, niche domain, or redundant tools. Safe to remove
  for a clean research environment; reinstall on demand.

Total potential savings: ~3-5GB by removing personal tier.

Also includes the full 391-package master inventory with per-package
justifications in software_inventory_2026-05-13.md.
 2026-05-13 18:29:40 -05:00
Brandon Schneider
a1907360dc docs(system): inventory all 391 installed packages with FRT separation 
Categorize every explicitly installed package into:
- VITAL: system boot/connectivity/authentication/update backbone
- NEEDED: core Research Stack toolchain (Rust, Lean, Python, Ollama, etc.)
- USEFUL: quality-of-life and secondary workflows
- IF YOU MUST: heavy/duplicate/niche tools safe to remove

Purpose: enable clean separation between personal/cosmetic software
and Fractal Recursion Theory runtime dependencies. Provides
per-package removal commands for ~2-3GB quick savings.
 2026-05-13 18:28:08 -05:00
Brandon Schneider
a6311ed940 chore: preserve working tree before secure wipe 
- Update .gitignore with **/target/ for Rust build artifacts
- Add eval receipts to UniversalBridge.lean (compile-time verification comments)
- Add PCIe Idle-Cycle Compute Harvester to ROADMAP.md
- Clean up deprecated scripts, generated Verilog, and old tools (23 deletions)
- Stage new infrastructure: Xen/Alpine embedded surface, QFOX topology manager
- Stage new probes: boundary activation field, holographic carving
- Stage new applications: finance manager, script roots
- Stage new research spec: PCIe idle-cycle substrate
 2026-05-13 17:36:02 -05:00
Brandon Schneider
cb96c6bed2 Update repository agent operating contracts 2026-05-11 22:48:54 -05:00
Brandon Schneider
a99e839bab Track remaining source and documentation inventory 2026-05-11 22:18:31 -05:00
Brandon Schneider
d9995cf2de Stage JXL starfield replay slice 2026-05-11 22:08:44 -05:00
Brandon Schneider
29f9b78b6d Stage stack solidification source slice 2026-05-11 22:08:10 -05:00
Brandon Schneider
06c83af4c8 Add EntropyCollapseDetector kernel and arithmetic spec 
- Add EntropyCollapseDetector.lean: executable checks for triple condition
  (braid crossings, σ_q/Hurst, D_q/Rényi D_2) with dense_rank tie handling
- Add Manifest.lean: imports EntropyCollapseDetector into HCMMR
- Add ArithmeticSpec_Corrected_2026-05-11.md: verified arithmetic constants
  K=21 for W=8 (~5% FPR), σ_c=0.4, D_c=0.7 (heuristic)

Arithmetic self-verified in Python:
- Braid crossings: 12 (K=7 non-selective, K=21 selective)
- σ_q = H = 0.032 (anti-persistent oscillating series)
- D_2 = 0.514 (moderate concentration)
- D_c=1.2 invalid for 1D Rényi D_2; corrected to 0.7

Prime gap re-test with K=21 shows signal mostly dies:
- 1M primes: 86,565 fires at K=7 (artifact) vs 38 at K>21 (genuine)
- Detector now selective but potentially too conservative

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

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-11 21:44:47 -05:00
Brandon Schneider
c7989636b7 Document legacy recovery trigger 2026-05-11 15:11:18 -05:00
Brandon Schneider
38ddec024d Add RRC projection receipts and roadmap mirrors 2026-05-08 14:50:03 -05:00
Allaun Silverfox
c6e2d33ef3 docs: add LLM refinement protocol 2026-05-07 08:21:35 -05:00