allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-08-13 17:20:34 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
199 commits 18 branches 0 tags 425 MiB
Commit graph

199 commits

This branch
This branch
All branches
Author SHA1 Message Date
Allaun Silverfox
9d3e65c9a7 Add Sidon 16D anchor pack 2026-05-16 17:21:03 -05:00
Allaun Silverfox
c3c8a1d481 Add Sidon FAMM map example config 2026-05-16 17:20:33 -05:00
Allaun Silverfox
a539fdb1d5 Add Sidon FAMM map receipt schema 2026-05-16 17:19:43 -05:00
Allaun Silverfox
3c0fd24c72 Add Sidon FAMM map runner 2026-05-16 17:18:49 -05:00
Allaun Silverfox
118661906b Add Sidon FAMM map documentation 2026-05-16 17:17:26 -05:00
Allaun Silverfox
bfec63fe15 Add Builder-Judge-Warden Erdos-Szekeres example 2026-05-16 17:06:26 -05:00
Allaun Silverfox
125a768385 Add Builder-Judge-Warden cleanup receipt schema 2026-05-16 17:00:28 -05:00
Allaun Silverfox
207d854a12 Add Builder-Judge-Warden geodesic cleanup runner 2026-05-16 16:59:26 -05:00
Allaun Silverfox
e8ab9b812c Add Builder-Judge-Warden geodesic cleanup filter documentation 2026-05-16 16:57:56 -05:00
Allaun Silverfox
b21d2326d7 Add 16D logogram chirality anchor pack 2026-05-16 16:36:53 -05:00
Allaun Silverfox
fe6a58e1ec Add logogram chirality witness example 2026-05-16 16:35:55 -05:00
Allaun Silverfox
8136c8b173 Add logogram chirality witness schema 2026-05-16 16:35:07 -05:00
Allaun Silverfox
797eca1aca Add logogram chirality route gate runner 2026-05-16 16:31:01 -05:00
Allaun Silverfox
f495ff55d6 Add logogram chirality route gate documentation 2026-05-16 16:30:15 -05:00
Allaun Silverfox
9432a113c6 Add NUVMAP Delta-DAG graph coloring example 2026-05-16 16:15:20 -05:00
Allaun Silverfox
864fa9af94 Add NUVMAP Delta-DAG receipt schema 2026-05-16 16:14:43 -05:00
Allaun Silverfox
d20a8f613c Add NUVMAP Delta-DAG graph coloring compressor 2026-05-16 16:13:58 -05:00
Allaun Silverfox
ac109d817e Add NUVMAP Delta-DAG sharding spec 2026-05-16 16:12:10 -05:00
Allaun Silverfox
6f914fc3ba Add NUVMAP Delta-DAG search compressor documentation 2026-05-16 16:05:53 -05:00
Allaun Silverfox
85caddd1af Add common-noise MFG 16D anchor pack 2026-05-16 15:11:10 -05:00
Allaun Silverfox
0925264f3f Add common-noise MFG Riccati gate documentation 2026-05-16 15:04:56 -05:00
Allaun Silverfox
1327224837 Add bio-organoid 16D anchor pack 2026-05-16 14:54:17 -05:00
Allaun Silverfox
8a59e92d27 Add bio-organoid signal field gate documentation 2026-05-16 14:49:05 -05:00
Allaun Silverfox
30553fb92d Add 16D Chaos Game example config 2026-05-16 14:44:29 -05:00
Allaun Silverfox
4df47395b5 Add 16D Chaos Game receipt schema 2026-05-16 14:43:21 -05:00
Allaun Silverfox
7e75631810 Add 16D Chaos Game field shrinker runner 2026-05-16 14:39:56 -05:00
Allaun Silverfox
30668c6df7 Add 16D Chaos Game Field Shrinker documentation 2026-05-16 14:39:03 -05:00
Allaun Silverfox
aef8bed3f1 Document Semantic Mass route plow runner 2026-05-16 13:51:09 -05:00
Allaun Silverfox
50079eff01 Add example Semantic Mass route plow config 2026-05-16 13:50:19 -05:00
Allaun Silverfox
3646f3dd26 Add Semantic Mass route plow receipt schema 2026-05-16 13:42:25 -05:00
Allaun Silverfox
394f41d0b1 Add Semantic Mass route plow runner 2026-05-16 13:41:51 -05:00
Allaun Silverfox
b4c414f487 Add FAMM Semantic Mass math-forest plow documentation 2026-05-16 13:35:56 -05:00
Allaun Silverfox
a3180826cc Add example Semantic Mass Z accelerator config 2026-05-16 13:27:42 -05:00
Allaun Silverfox
7162473781 Add Semantic Mass Z receipt schema 2026-05-16 13:25:39 -05:00
Allaun Silverfox
d0f6bd085e Add Semantic Mass Z-domain accelerator runner 2026-05-16 13:24:51 -05:00
Allaun Silverfox
881e9b5afe Add Semantic Mass Z-domain accelerator documentation 2026-05-16 13:24:06 -05:00
Allaun Silverfox
d249ef76a6 Document empirical Hessian receipt pass 2026-05-16 13:18:08 -05:00
Allaun Silverfox
ad587f8068 Add example FAMM Hessian receipt config 2026-05-16 13:17:24 -05:00
Allaun Silverfox
c88055f3a1 Add FAMM Hessian curvature receipt schema 2026-05-16 13:16:48 -05:00
Allaun Silverfox
fa6989c31d Add FAMM empirical Hessian receipt runner 2026-05-16 13:14:33 -05:00
Brandon Schneider
7d2180f8e7 feat: eigensolid convergence proof + QC flagging tool + full pass/fail review 
Resolves the convergence_to_fixed_point failure by proving the correct
eigensolid statement: stepExact stabilizes all value components (N_7,
N_8, N_11) in one application. The original theorem was mathematically
false (iteration counter is free-running).

QC cleanup sweep across Physics/ (20 files):
- 3 remaining LOW items fixed: h00/h01 factoring, rD->rd, rdDr1/rdDr2 x100
- 6 of 7 sorry theorems proved; 1 explicitly FAILED (convergence)
- Unused imports removed, naming violations fixed, #eval witnesses added
- 210 -> 144 issues remaining (all WARNING/INFO, zero ERROR)

New tooling:
- scripts/qc-flag/lean_qc_flagger.py implemements 5-point inspection protocol
- Outputs structured JSON + Markdown pass/fail reports

DAG receipts at shared-data/data/stack_solidification/qc_*_dag_2026-05-13.md
 2026-05-14 00:04:08 -05:00
Brandon Schneider
e6818c8029 chore: QC cleanup — create Q16Utils, remove dead code, consolidate proofs 
NEW: Q16Utils.lean — shared scale, absDiff, q16Mul, q16Div removed from 6 files

HIGH (4 fixed):
  H1: absDiff now shared from Q16Utils (was in 4 files)
  H2: scale now shared from Q16Utils (was in 6 files)
  H3: 2 duplicate theorems removed (AdjacentCoprimeClassification)
  H4: dead q16_div removed from DESIModelProjection

MEDIUM (4 fixed):
  M5: dead DESIParam removed from DESIInvariant
  M6: q16Abs kept (Int.abs not available in Lean 4.30)
  M7: 6 dead structures removed from DESIModelProjection
  M8: 40 theorems consolidated into 5 ∧ chains (AdjacentCoprimeClassification)
  M9: q16Div now shared from Q16Utils

LOW (2 fixed):
  L11: SuperpositionalBoundaryLayers now uses shared Q16Utils
  L12: SCALE → scale in SuperpositionalBoundaryLayers

Build: 3530 jobs, zero errors
 2026-05-13 22:18:13 -05:00
Brandon Schneider
3afb6c1c61 chore: QC report — 14 structural/efficiency issues found 
HIGH (4): absDiff 4x duplicated, scale 6x duplicated,
         duplicate theorems, dead q16_div
MEDIUM (5): dead DESIParam, q16Abs=Int.abs, dead structures,
           25 theorems unconsolidated, q16_div duplicated
LOW (5): Hermite helper, Q16.16 consistency, SCALE casing,
         rD field naming, rd precision
 2026-05-13 22:11:16 -05:00
Brandon Schneider
55f6bf6605 chore: cleanup crew — fix 95 inspection issues 
NAMING (79 issues fixed):
  UniversalBridge.lean — 26 theorems + SCALE renamed to camelCase
  DESIInvariant.lean — 20 defs + 5 theorems renamed
  DESIModelProjection.lean — 14 theorems + 2 defs renamed
  H0ValveTest.lean — 6 defs + 4 theorems renamed
  ValveTestSuite.lean — 9 theorems + SCALE renamed
  ClusterBHAnchors.lean — 6 theorems + 3 defs renamed
  AdjacentCoprimeClassification.lean — 25 theorems renamed

STRUCTURAL (16 issues fixed):
  2 unused imports removed (Semantics.FixedPoint)
  13 #eval → #eval! consistency fixes
  3 duplicate theorems removed (fib_cond1, fib_cond2, ex3_cond1)
  1 linter suppression removed (dupNamespace)
  1 namespace dependency fixed (open Semantics removed after import cut)

Build: 3529 jobs, zero errors
 2026-05-13 22:08:38 -05:00
Brandon Schneider
25ed6caa3b feat: create Lean Expert Agent with full inspection protocol 
Agent inspects Lean code for:
1. Structural health (theorem/def/eval/sorry counts)
2. Naming conventions (camelCase/PascalCase per AGENTS.md)
3. Q0_16/Q16_16 compliance
4. Proof quality (native_decide, .isSome guards, tautologies)
5. Dependency analysis (unused imports, circular deps)

First inspection of Physics/ found 95 issues:
  79 naming violations (systematic snake_case)
  2 unused imports (Semantics.FixedPoint)
  4 trivial/tautological proofs
  3 #eval vs #eval! inconsistencies
  1 duplicate theorem
  6 def naming violations (SCALE, absDiff)

Trigger with: /inspect <target>
 2026-05-13 22:01:12 -05:00
Brandon Schneider
80a62524be dag: strip all non-mathematical commentary from Physics/ 
REMOVED (8 narrative-only files):
  BreakPoints.lean, BrokenChains.lean, NewtonWalls.lean — zero theorems
  JupiterMoons.lean, ProtiumProbe.lean — no theorems, torsion speculation
  GWTorsionTest.lean — 1 trivial theorem, rest narrative
  PhotonTorsionProbe.lean — 0 theorems after placeholder removal
  RGManifoldSeams.lean — 2 theorems buried in narrative

STRIPPED (8 files):
  UniversalBridge.lean — removed '16D controller' narrative from header
  DESIInvariant.lean — removed 'horn-fiber' reference
  DESIModelProjection.lean — removed metaphor from theorem docstrings
  H0ValveTest.lean — removed 'horn-fiber' and 'valve' narrative
  ValveTestSuite.lean — removed all interpretation comments
  ClusterBHAnchors.lean — removed FAILURE narrative
  AdjacentCoprimeClassification.lean — removed project language injection
  (4 more files from earlier rip/tear already committed)

KEPT (6 files, math-only):
  UniversalBridge.lean, DESIInvariant.lean, DESIModelProjection.lean,
  H0ValveTest.lean, ValveTestSuite.lean, ClusterBHAnchors.lean,
  AdjacentCoprimeClassification.lean
 2026-05-13 21:57:34 -05:00
Brandon Schneider
105257c04a dag: rip/tear — remove 8 broken/empty/tautological theorems, 3 ornamental files 
REMOVED theorems (8):
  BraidCross.lean — 2 trivial zero-strand witnesses
  FAMM.lean — 2 tautological identities (X = X)
  MengerSpongeFractalAddressing.lean — 3 empty theorem bodies
  NBody.lean — verlet_preserves_energy_approximate references nonexistent lemma

REMOVED files (3):
  CMBTorsion.lean — 0 theorems, invented alpha formula
  CouplingRotation.lean — heuristic w0 projection formula
  TorsionWall.lean — alpha = max|beta|/(4*pi) invented relation

Build: 3529 jobs, zero errors after all removals
 2026-05-13 21:50:09 -05:00
Brandon Schneider
f1b4138049 dag: full-stack assumption audit — 78 files, ~280 assumptions 
Breakdown:
  Physics/Lean:     15 files, 1 green, 4 yellow, 10 red
  Infrastructure:   33 files, ~190 heuristic assumptions
  5-Applications:   30 files, 88 assumptions

Critical action items:
  NBody.lean:1395 — broken theorem, references nonexistent lemma
  MengerSponge:197-208 — 3 empty theorem bodies
  FAMM.lean:141,223 — 2 tautological theorems
  BraidCross.lean:71,78 — trivial zero-strand only

Well-scoped: PIST.lean, buoyancy_added_mass, solids_physics,
  alphafold_probe, CAD harness, finance_manager, review_emitter
 2026-05-13 21:44:53 -05:00
Brandon Schneider
3c65a3c96c dag: trace 7 generations of RG flow assumptions 
Gen 1  SM beta functions      SOLID — standard, validated to 10^-12
Gen 2  omega = |beta|/|g|     CURIOSITY — defined, interpretation weak
Gen 3  alpha = max|beta|/(4π) INVENTED — no Lagrangian, looks like fitting
Gen 4  w0 projection          HEURISTIC — needs QFT derivation, circular with LCDM
Gen 5  wa from SM             HONEST GAP — factor 10, most interesting tension
Gen 6  CMB from omega         BROKEN — Q off by 13x, eta circular
Gen 7  M-sigma sum            CURIOSITY — numerical coincidence

Recommended: delete CMBTorsion, TorsionWall, CouplingRotation
or derive properly. omega=0.05775 is real; the projections are not.
 2026-05-13 21:41:48 -05:00
Brandon Schneider
bca98cf762 dag: fix 3 critical jiggles, document 10 known 
FIXED:
  PhotonTorsionProbe.lean:37 — placeholder theorem (proved 1>0)
  DESIInvariant.lean:208-221 — 4 vacuous sigma-range theorems
  UniversalBridge.lean:261 — missing .isSome for intermittency(3150)

DOCUMENTED (known jiggles):
  Moody chart slopes (heuristic but acceptable)
  wa has no SM derivation (largest open question)
  w0 projection formula (self-acknowledged heuristic)
  alpha = max|beta|/(4*pi) (invented relation)
  CMB Q factor 13 discrepancy (unresolved)
  10 known jiggles total, 69/82 theorems clean (84%)
 2026-05-13 21:40:38 -05:00