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
Brandon Schneider
fdb33aa08e
fix: braid_search.py QUBO/soliton from float to Q16_16 integer arithmetic
...
AGENTS.md §1.4 compliance: all internal computation now uses Q16_16 integers.
Float only at HiGHS API boundary and display statements.
- Q16_SCALE = 65536, _q16(), _q16_to_float(), _q16_signed()
- bracket_cost, crossing_penalty, build_qubo_matrix: all int
- soliton_search, qubo_optimize: Q16_16 temperature/energy
- 68/68 tests pass
2026-05-28 17:47:40 -05:00
Brandon Schneider
230a8075f3
feat: dense Sidon sets from sum-product conjecture disproof
...
Mian-Chowla sequence replaces powers-of-2 as default:
- 8 slots: max 128 → 45 (65% reduction)
- 16 slots: max 32768 → 252 (99% reduction)
- All constructions verified as valid Sidon sets
Methods: 'powers_of_2' (old), 'greedy_optimal' (Mian-Chowla, default),
'algebraic' (number field construction for large n).
Based on Bloom-Sawin-Schildkraut-Zhelezov (2026) sum-product disproof.
2026-05-28 16:57:35 -05:00
Brandon Schneider
e80ae136b8
feat: HiGHS wired as default QUBO solver in braid_search.py
...
- solve_qubo_highs() tried first, SA fallback on failure
- build_qubo_matrix(): bracket_cost (diagonal) + crossing_penalty (off-diagonal)
- find_optimal_crossing() returns method: 'highs_mip' or 'simulated_annealing'
- Timing: HiGHS 8.4ms vs SA 53.5ms (6.4x speedup)
2026-05-28 16:35:05 -05:00
Brandon Schneider
53e38e4c71
feat: 12 math enhancements — Q16 LUT, braid VCN encoder, FPGA Verilog, FFT, crypto
...
Pipeline:
- q16_lut_vcn.py: Q16_16 LUT generation + VCN frame encoding (8 ops)
- braid_vcn_encoder.py: Delta+RLE → RS ECC → ChaCha20 → VCN → MKV
- braid_search.py: Sidon set slots, soliton search, QUBO optimization
- test_braid_pipeline.py: 67 tests covering full round-trip
WebGPU/Scripts:
- braid_fft.wgsl: Cooley-Tukey radix-2 FFT on phase vectors
- reed_solomon_vcn.py: Reed-Solomon ECC for VCN frame data
- chacha20_braid.py: ChaCha20 encryption + key derivation
- polynomial_commitment.py: KZG scheme for receipt verification
Lean:
- BraidBitwiseODE.lean: XOR crossing, O(1) integration, 2 proved theorems
FPGA (Tang Nano 9K):
- q16_lut_core.v: 8-op arithmetic, 2-stage pipeline, BRAM reciprocal
- braid_crossing_core.v: 4-stage crossing residual, 7 Q16 instances
- Testbenches with edge cases + VCD dumps
2026-05-28 14:49:26 -05:00
