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

19 commits

Author SHA1 Message Date
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
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
Allaun Silverfox
1f7e38dfbc Add Phys.org May 2026 source intake for bees, biocoatings, THz, and diamond membranes 2026-05-23 19:27:37 -05:00
Brandon Schneider
546783faaf docs: add external research import maps 2026-05-20 18:41:21 -05:00
Brandon Schneider
b58c1201ac Remove legacy Python prototypes superseded by Lean formalization 
Deleted 58 Python files (~31K lines) that were experimental prototypes
and bootstrapping scripts now superseded by the Lean source of truth:

0-Core-Formalism/core/ (2 files):
  - field_solver_emulator.py
  - formalize_mass_number.py

0-Core-Formalism/lean/LeanGPT/ (17 files):
  - All LLM bootstrapping scripts (algorithm_bootstrap, automated_conviction_loop,
    classify_algorithms, external_model_bridge, genetic_hypothesis_generator,
    group_algorithms_by_domain, hutter_prize_full_test, hutter_prize_test,
    hypothesis_generator, mathematical_law_conviction, otom_pipeline,
    performance_profiler, refine_algorithms_by_domain, skeptical_agent_concern_fix,
    skeptical_agent_swarm, wgsl_hypothesis_runner)

0-Core-Formalism/lean/Semantics/ (1 file):
  - expand_domains.py

0-Core-Formalism/otom/ (4 files):
  - scripts/validate_routing.py
  - tools/ene/ene_artifact_salvage_extractor.py
  - tools/genetics/emit_selection_receipt.py
  - tools/genetics/selection_metrics.py

2-Search-Space/ (14 files):
  - FAMM/solve_famm_sorry.py
  - GhostPivot/gist_pivot_poc.py
  - PIST/hybrid_tsm_pist_torus.py, pist_sweep.py
  - SVQF/microgrid_voxel_emulation.py
  - manifold/ (9 files: api/server, collapse_editor, particle_interaction,
    projection_engine, relativity_adapter, self_typing_engine, soliton_search,
    substrate_bridge)
  - search/generate_lut.py, ingest_pd.py, sweep_manifold.py

3-Mathematical-Models/ (20 files):
  - dna_benchmark/compressors/ (5 files)
  - pist_biological_polymorphic_shifter_v3*.py (5 files)
  - fiber_optic_vibrational_tensor/fiber_optic_tensor_network.py
  - manifold_compression/src/ (2 files)
  - fix_kwargs_meta.py, fix_metadata.py, fix_remaining.py, fix_sbox.py
  - genetics/Allelica/Allelica.py

These prototypes expressed formal concepts in Python that are now
formalized in Lean (747+ Lean modules). Per AGENTS.md, Lean is the
source of truth for formal claims.

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

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-19 15:34:17 +00:00
Brandon Schneider
0cf775c80e collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 
- Prover-Integrated Orchestration Layers (L0-L3): Goedel-Prover-V2 watchdog, BFS-Prover-V2 swarm consensus, bf4prover topology adaptation
- FAMM Verilator benchmark: uniform vs preshaped delay comparison (4.4x speedup)
- Swarm topological device prober: 11 agents probing traces, caps, delays, errors, vias, PDN
- Spec sheet puller: 10 components with key params and topological relevance
- Virtual FPGA system tests: 6/6 passed, 134K ops/s throughput
- Fixed merge conflicts in AI-Newton test_experiment.ipynb
 2026-05-06 23:42:01 -05:00
Brandon Schneider
0709b298b3 Consolidate research stack updates 2026-05-05 21:09:48 -05:00
Allaun Silverfox
3a8e4c2881 Add selection metrics receipt emitter 2026-05-05 13:23:10 -05:00
Allaun Silverfox
4e48f49752 Add selection metrics synthetic fixture 2026-05-05 13:22:32 -05:00
Allaun Silverfox
dbb3e35359 Add q-desic and van der Waals gap DOIs to Consensus collection 2026-05-05 07:39:43 -05:00
Allaun Silverfox
a70bc86fdb Add frozen-in gravitational fields DOI to Consensus collection 2026-05-05 02:22:12 -05:00
Allaun Silverfox
a7a2af5f19 Add genetics selection metrics scaffold 2026-05-05 02:07:28 -05:00
Allaun Silverfox
d38e3e6db1 Add genetics information substrate boundary 2026-05-05 02:01:27 -05:00
Allaun Silverfox
3c4e7ff90c Add de-anthropocentric Mass Number revision 2026-05-04 21:17:45 -05:00
Allaun Silverfox
670b3601bb Register visual primitive witness entry points 2026-05-04 19:10:11 -05:00
Allaun Silverfox
9159780fa7 Add visual primitives goxel witness research note 2026-05-04 19:08:47 -05:00
Allaun Silverfox
883adc29a8 Wire visual primitive formalism into constitution 2026-05-04 19:08:12 -05:00
Allaun Silverfox
eb448df619 Add visual primitive witness formalism 2026-05-04 19:07:01 -05:00
Brandon Schneider
5f88abf618 initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00