|
|
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 |
|
|
|
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 |
|
