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

129 commits

Author SHA1 Message Date
allaun
59db58d954 docs(agent): break-glass test list for 4D × 2 fusion validation 
15 tests across 4 dimensions + 4 cross-dimension tests:
- Math (T1.1-T1.3): Q16_16 positivity, q16_merge_nz, boolMerge_preservesGap
- Proof (T2.1-T2.3): gap_factors, disjoint_factors, crossgap_factors
- Code (T3.1-T3.3): verifySpectralGap8, toPattern_merge, mergeCheck8_all
- Diversity (T4.1-T4.3): architecture, rewrite fix, counterexample search
- Cross-dim (T5.1-T5.4): chain proofs across dimensions

Estimated cost: -10 for full suite.
Success: cleanMerge_preservesGap compiles with 0 sorry.
 2026-06-22 16:09:09 -05:00
allaun
7f09d0c1a3 docs(agent): break-glass problem statement — transcendental work with division-impaired brains 
Defines the core tension: formal verification of novel mathematical
structures using LLMs that can't reliably do arithmetic. Documents
why panels help (diversity > quality), what makes the work
transcendental, and how the break-glass protocol addresses it.
 2026-06-22 15:44:26 -05:00
allaun
2cbba82406 feat(agent): break-glass MCP agent for novel problem attacks 
Last-resort multi-model panel via OpenRouter Fusion. Only invoked
when all other approaches (local model, single frontier, existing
skills) have failed on the same problem.

Architecture:
- Problem classification (lean_proof, code_bug, architecture, math_novel, infra_debug)
- Per-type model panel selection (Opus + DeepSeek + Gemini for proofs)
- Context assembly (files, build logs, AGENTS.md constraints)
- OpenRouter Fusion call (parallel panel + judge synthesis)
- Structured output (diagnosis, solution, alternatives, risks, cost)

Safety:
- Explicit 'break glass:' trigger required
- Cost gate: /usr/bin/bash.30-.50 per invocation, .00/session cap
- Rate limit: 3 invocations per session
- Audit trail via ContextStream

Files:
- 4-Infrastructure/shim/break_glass_mcp.py (MCP server)
- 6-Documentation/docs/specs/break_glass_mcp_agent.md (design spec)
- .opencode/skills/break-glass/SKILL.md (skill definition)
- .mcp.json (server registration)
 2026-06-22 15:33:16 -05:00
allaun
0d387902bb docs(lean): standalone proof guide for cleanMerge_preservesGap 
Self-contained document for LLM agents to close the 6 remaining
bridge sorries. Covers:
- Theorem statement and definitions
- Proof architecture (3 verified kernels + 6 bridge sorries)
- What each sorry needs and the proof strategy
- The key insight (zero/non-zero pattern only)
- The blocker (simp can't reduce List operations on 8 elements)
- Possible solutions and file context
 2026-06-22 14:52:15 -05:00
allaun
5da90cd1d1 docs: add Clebsch diagonal cubic claim + update GraphRank proof status 
- Added silversight_claim_clebsch_diagonal_cubic to manifest (Phase 2 geometry witness: 42 nodes→scar-absence, 27 lines→strand topology)
- Updated cleanMerge_preservesGap theorem with crossInputGap hypothesis and documented TODO(lean-port) boundary for Q16_16↔Bool bridge
- Compiler surface unchanged (3314 jobs, 0 errors), full workspace verified (8604 jobs)

Build: 8604 jobs, 0 errors (lake build)
 2026-06-22 13:50:59 -05:00
allaun
73db623848 feat(silversight): Phase 1 core + claim promotions + theorem triage 
Phase 1 core (7 new Lean files, 3307 jobs, 0 errors):
- Schema.lean: Schema class with 6 type instances
- WireFormat.lean: WireFormat structure + Layout enum
- ProductSchema.lean: Schema (α × β) instance
- ProductWireFormat.lean: Row-major pair encoders with roundTrip proofs
- Receipt.lean: Receipt structure + GateType enum
- Bind.lean: bindReceipt composition + 8 theorems
- SilverSight.lean: root import module

Claim promotions (3 claims → VERIFIED):
- silversight_claim_q16_unified: FixedPoint.lean 12 theorems, 0 sorry
- silversight_claim_eigensolid_convergence: BraidEigensolid.lean:175
- silversight_claim_receipt_invertible: BraidEigensolid.lean:249

Theorem triage (3,057 theorems classified):
- TIER_1_CORE: 118 theorems (6 modules, direct port)
- TIER_2_FOUNDATION: 1,591 theorems (121 modules)
- TIER_3_EXTENSION: 1,084 theorems (291 modules)
- TIER_4_QUARANTINE: 137 theorems (15 modules)
- TIER_5_EXCLUDED: 127 theorems (18 modules)

Build: SilverSight 3307 jobs, 0 errors, 0 sorries
 2026-06-22 13:00:29 -05:00
allaun
aefd06dc84 chore(cleanup): remove shared-data archive lean_binned from repo 
These directories were tracked despite gitignore patterns. Removing them
frees ~120 GB (shared-data), ~1.5 GB (archive), and ~7 GB (lean_binned).
They are either offloaded to Garage S3/Google Drive or superseded
proof artifacts.
 2026-06-22 05:01:33 -05:00
allaun
94b04ae321 docs: add rebase rules manifest and SilverSight claims manifest 2026-06-22 03:28:53 -05:00
allaun
69988453bc chore(infra): stage working tree modifications 
Build: 8604 jobs, 0 errors (lake build)
 2026-06-22 01:23:17 -05:00
allaun
8079ca3a20 docs(infra): document bosonic tensor network regime discovery and fix dim formula 
- Updates CHANGELOG.md with 2026-06-21 entry describing the two-regime
  phase transition observed on neon-64gb: bosonic MC (p<=4) vs
  distinguishable approximation (p>=5) in rrc_bosonic_tensor_network.py.
- Adds BMCTE, SBOE, LPMCE, effective support, and observable-estimation
  vs exact-simulation terms to 6-Documentation/docs/GLOSSARY.md.
- Fixes Hilbert-dimension summary in rrc_bosonic_tensor_network.py to use
  C(N+p-1, p) instead of C(N, p).

No core logic changed; documentation and summary-output correction only.
 2026-06-22 01:11:17 -05:00
allaun
bc8657ff15 docs(glossary): update Jaccard Matcher with live results 
240 candidate citations found for 48 cornfield concepts using
pg_trgm GIN indexes and /shm file-based matching against 700k papers.

DB state: 358 total concept_citations (96 grounds, 22 extends, 240 candidates)
 2026-06-22 01:11:17 -05:00
allaun
3cdf0d11e9 docs(glossary): add concept map, citations, PIST classifier, SilverSight entries 
New glossary sections:
- Concept Mapping & Citations: Concept Map, Drive Concept Map, Cornfield Concepts,
  concept_citations, paper_refs, is_novel_claim, novelty_statement, Jaccard Matcher,
  relation_type
- SilverSight: Product Schema/WireFormat/LayoutBridge/View, ReceiptHeader, Gate,
  Claim-State Ladder
- PIST Trace Classifier: PistClassifyTrace, Spectral Profile, RRC Shape Thresholds,
  Tactic Family, rrc-watchdog

Acronym additions: CM (Concept Map), JM (Jaccard Matcher), PTC (PIST Trace Classifier),
SS (SilverSight)
 2026-06-22 01:11:17 -05:00
allaun
4dd0c18759 docs(plans): address review conditions on completion pipeline 
- Reorders Phase 1 next steps to dependency order.
- Adds Q16_16 / UInt64 justification notes and explicit ReceiptHeader
  56-byte layout with #eval witness.
- Redesigns Core Gate.bind as a Kleisli arrow with separate Invariant
  certificate to avoid proof holes.
- Registers SilverSight.Bind in lakefile.lean integration step.
- Removes forced Core Gate ↔ CoreFormalism Bind bridge; documents boundary.
- Clarifies Verilog extraction as static, reviewed Lean→template mapping.
- Specifies compression benchmark sample source and reproducibility.
- Fixes fixed-point comparison operators in classifyRegime.
- Adds phase/focus table to dependency graph.

Build: docs only; no Lean/Python changes
 2026-06-22 01:11:17 -05:00
allaun
f7c08f7a6a docs(plans): expand SilverSight completion pipeline to microstep level 
Overwrites 6-Documentation/docs/plans/SilverSight_completion_pipeline.md
with a per-file, per-theorem, per-commit microstep plan covering Phases
1-8: Core Semantics completion, Research Stack triage/port, corpus build,
mathematical models, shim rewrite, hardware extraction, applications,
and final documentation/promotion. Includes claim-state ladder, open
question answers, dependency graph, verification gates, CI coverage,
risks, and acceptance criteria.
 2026-06-22 01:11:17 -05:00
allaun
37d05d1a77 docs(plans): add SilverSight completion pipeline design 
Adds 6-Documentation/docs/plans/SilverSight_completion_pipeline.md,
describing the full phase plan from the current core Semantics state to
a verified SilverSight 1.0: Core completion, Research Stack triage/port,
corpus build, mathematical models, shim rewrite, hardware extraction,
applications, documentation, and claim-state promotion.
 2026-06-22 01:11:17 -05:00
allaun
7098ee0d64 docs(specs): add SilverSight specification draft with Core Semantics sections 
Adds 6-Documentation/docs/specs/SilverSight_Spec.md, documenting the
YaFF-inspired separation of schema, layout, access pattern, wire format,
view, layout bridge, and canal-aware layout selection for the SilverSight
clean-slate architecture.
 2026-06-22 01:11:17 -05:00
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
5f528502b0 docs(infra): remove AWS-specific credential and RDS backend details 
Update Credential-System.md and RDS-Rust-Workspace.md to describe a
provider-neutral PostgreSQL backend instead of AWS RDS. Replace IAM
auth examples with standard libpq env-var connection. Remove the
~/.aws/ file layout and AWS hostname defaults.
 2026-06-19 22:44:38 -05:00
allaun
318db01e31 refactor(infra): decommission AWS deployment artifacts 
Remove EC2/RDS deployment scripts, EC2 watchdog, and RDS substrate
provisioning files. Drop the legacy AWS API MCP server from all IDE
configs. Replace hardcoded AWS proof-server and RDS default endpoints
with localhost/env-only placeholders.

Deleted:
- 4-Infrastructure/infra/deploy_aws_language_proof_server.sh
- 4-Infrastructure/infra/aws_language_proof_server_user_data.sh
- 4-Infrastructure/infra/ec2-configuration.nix
- 4-Infrastructure/infra/ec2_idle_watchdog.py
- 4-Infrastructure/infra/ec2-idle-watchdog.service
- 4-Infrastructure/infra/ec2-idle-watchdog.timer
- 4-Infrastructure/deploy/rds-substrate/*

Changed:
- .mcp.json, .cursor/mcp.json, .roo/mcp.json, .vscode/mcp.json:
  remove aws server, make remote-lean-proof URL env-only
- .vscode/settings.json: remoteLeanProof.url -> localhost
- 4-Infrastructure/infra/remote_lean_proof_mcp.py: default URL -> localhost
- ene-rds/ene-session-sync: default RDS_HOST -> localhost
- RECOVERY.md, INFRASTRUCTURE.md, TODO_MAP.md: remove AWS/EC2 refs

Build: cargo check ene-rds OK; python3 -m py_compile OK; JSON valid
 2026-06-19 22:42:34 -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
6600af4dbd docs: fold k3s cluster setup + netcup-vps into infrastructure docs 
Added to INFRASTRUCTURE.md:
- k3s cluster topology (cupfox control plane)
- Ollama inference serving (Neon-64GB, Caddy reverse proxy)
- netcup-vps ARM64 math stack (openblas, petsc, z3, julia)
- Reference to 4-Infrastructure/docs/k3s-cluster-setup.md
 2026-05-30 14:38:32 -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
18963e7053 docs: mark AWS instances as shut down, self-hosted bare metal only 
- Added hosting note: self-hosted bare metal, no cloud instances
- Marked AWS MCP server as legacy
- All compute on physical nodes via Tailscale mesh
 2026-05-29 02:09:46 -05:00
Brandon Schneider
7a6df586b2 docs: runbook, FPGA programming guide, disaster recovery, API docs 
- RUNBOOK.md: k3s/FPGA/Tailscale/GPU/DNS ops procedures
- FPGA_PROGRAMMING_GUIDE.md: SUBLEQ format, memory map, 3 examples
- DISASTER_RECOVERY.md: backup/restore for all components
- API_DOCS.md: dashboard, credential, registry, jobs, blobs APIs
 2026-05-29 01:26:41 -05:00
Brandon Schneider
251ea9d9bf docs: comprehensive infrastructure documentation 
Covers:
- 5-node Tailscale mesh (nixos, qfox, 361395-1, racknerd, steamdeck)
- k3s cluster: 7 namespaces, 20+ services, Traefik ingress
- FPGA: Tang Nano 9K, 6-module bitstream, 195.92 MHz
- GPU: RTX 4070, Ollama deepseek-coder-v2:16b
- Lean: 3572 jobs, 10 modules, 8 sorries
- Python: 68/68 tests, HiGHS 8.4ms
- Skills: 111 enabled (6 local, 12 hub, 85 builtin)
- MCP servers: eda, lean, sympy, contextstream, aws
- DNS/TLS: researchstack.info, Porkbun, LE certs
- Key constants: Q16_16, golden angle, baud rate, Kolmogorov
 2026-05-29 01:12:18 -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