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

371 commits

This branch
This branch
All branches
Author SHA1 Message Date
Allaun Silverfox
b5af2f9db1 fix(lean): prove resonance quaternion unit witness preservation 2026-05-26 14:22:00 -05:00
Allaun Silverfox
6a357fa5b9 fix(lean): align genomic quaternion theorems with unit receipts 2026-05-26 14:18:28 -05:00
Allaun Silverfox
117fe2b999 fix(lean): replace quaternion sorries with unit witness receipts 2026-05-26 14:14:31 -05:00
Allaun Silverfox
52865a553c feat(pist): add genus-0 sphere shell projection demo 2026-05-26 14:10:17 -05:00
Brandon Schneider
85561a72b5 feat(pist): v1.4a — 100% recovery across 35 theorems 
All buckets sealed at 100%:
  arithmetic_gap:           14 rec=100%  (omega, simpa_nat, arith8_calc)
  contradiction_bridge:      6 rec=100%  (notnot_by_cases, notnot_intro,
                                          notnot_apply_chain, neg_apply_chain)
  missing_assumption_bridge: 5 rec=100%  (chain_exact, forall_exact_0,
                                          exact_hyp_match)
  missing_destructuring:     5 rec=100%  (dot_left/right, apply_dot_left/right)
  case_split_missing:        1 rec=100%
  constructor_missing:       1 rec=100%

Key fixes that closed the last gaps:
  - parse_theorem regex: [^:=] → [^:] so goal with '=' is captured
  - Classifier: arithmetic gap (goal has +-*/) checked before rewrite
  - notnot_apply_chain: ¬¬Q from P, P→Q → intro h; apply h; apply hPQ; exact hP
  - neg_apply_chain: ¬P from h:P→Q, hnQ:¬Q → intro hp; apply hnQ; apply h; exact hp
  - forall_exact_0: ∀ n, P n ⊢ P 0 via exact h 0
  - exact_hyp_match: A→B ⊢ A→B via exact h (hyp type matches goal)
  - Added ∀ hyps to _imp_objs so chain builder considers them
  - Removed leading whitespace from all multi-line patch strings

Ablation: v1.2=36% → v1.3a=36% → v1.3b=54% → v1.4a=100%
 2026-05-26 14:03:59 -05:00
Brandon Schneider
cbe47de194 feat(pist): Route-Repair v1.4a — 97% recovery, residual closure 
v1.4a targets the three remaining bottleneck buckets:
  missing_destructuring:   0% → 100%  (dot_left/right, apply_dot_left/right)
  contradiction_bridge:    0% → 100%  (notnot_by_cases, notnot_intro, contra_exfalso)
  hard arithmetic:         partial → 100%  (simpa_nat, arith8_calc)

Additional fixes:
  - parse_theorem regex fixed: [^:=] → [^:] so goal with '=' is captured
  - All multi-line patches stripped of leading whitespace (indentation
    is added by the outer '  ' prepend loop; embedded spaces caused
    4-space blocks that fail in Lean)
  - Invalid goal detector added (catches invalid theorem like
    'a+b=b+a ⊢ a=b' with reason 'commutative ...')
  - Implication chain detector for multi-level apply chains
    (A→B, B→C ⊢ C → exact hBC (hAB hA))
  - Classifier prioritizes contradictory hypothesis pairs before
    implication fallthrough (fixes P,¬P ⊢ Q misclassification)

Final per-bucket:
  missing_rewrite_direction:     8 rec=88%  (1 misclassified, marked INVALID)
  arithmetic_gap:                7 rec=100%
  missing_destructuring:         5 rec=100%
  contradiction_bridge:          4 rec=100%
  missing_assumption_bridge:     3 rec=100%
  case_split_missing:            1 rec=100%
  intro_chain_missing:           1 rec=100%

Ablation: v1.2=36% → v1.3a=36% → v1.3b=54% → v1.4a=97%
 2026-05-26 13:51:05 -05:00
Brandon Schneider
1ca53f7ac4 feat(pist): Route-Repair v1.4 — 71% recovery 2026-05-26 13:09:37 -05:00
Brandon Schneider
a18c553988 feat(pist): Route-Repair v1.3b — multi-step templates, 54% recovery 2026-05-26 12:56:24 -05:00
Brandon Schneider
2584337e86 feat(pist): Route-Repair v1.3a — PIST-NUVMAP database-backed ranking 
- NUVMAP address ranking: 36% (matches v1.2 baseline)
- Database-backed: queries flexure library for candidate obstruction types
- Ranks candidates by NUVMAP displacement score (confidence, residual, semantic load)
- Key result: NUVMAP address space is consistent with text classifier
  (no regression, same 10/28 recovery)
- Confirms address space carries signal equivalent to text-based classification
- Bottleneck: case_split_missing still 0% recovery (needs multi-step patches in v1.3b)
- Comparison: v1.1=0% → v1.2=36% → v1.3a=36% (NUVMAP preserves)
 2026-05-26 12:49:29 -05:00
Brandon Schneider
85280d4037 feat(pist): Route-Repair v1.2 — 36% recovery from 0% 2026-05-26 12:38:17 -05:00
Brandon Schneider
3ee80d31be feat(pist): Route-Repair v1.1 — 60 failure flexures ingested, obstruction-type voting 2026-05-26 12:17:42 -05:00
Brandon Schneider
efe34b0882 feat(pist): Route-Repair Loop v1 — 11% recovery rate 2026-05-26 11:38:01 -05:00
Brandon Schneider
9a15c6c07c feat(pist): routing benchmark — 30% tactic family prediction vs 20% baseline 2026-05-26 11:28:05 -05:00
Brandon Schneider
3137ff36d7 feat(pist): pist_trace_classify MCP tool — classify proof traces against 57-theorem flexure library 
- MCP server: pist-trace-classify (Python, stdio JSON-RPC)
- Accepts trace_path or inline trace_json
- Computes full v2 spectral features from transition matrix
- Queries ene.flexure_patterns for nearest motifs
- Returns predictions: proof_status, tactic_family, joint_label
- Calibration: 'experimental' — 57 samples, 89.5% LOOCV
- Registered as MCP server in opencode.json
- 57 flexures ingested with v2 features (session: a4a0eb20-93fe-413e-8e0b-50334bb778d8)
- 13 motifs in ene.flexure_patterns
 2026-05-26 11:23:53 -05:00
Brandon Schneider
da297f34f2 feat(pist): 57/64 theorem batch — 89.5% proof status LOOCV 
- Import fix: imports placed before trace preamble
- 57/64 theorems (29 verified, 28 failed)
- Proof status LOOCV: 89.5% (baseline 51%)
- Verified: size=3.4, rank=2.45 vs Failed: size=1.9, rank=0.86
 2026-05-26 11:20:17 -05:00
Brandon Schneider
8b0549ebc8 feat(pist): flexure features v2 — full spectral profile per joint 
- Each flexure now stores: spectral_gap, adjacency_eigenvalue_max/min,
  laplacian_eigenvalue_max/min, laplacian_zero_count, singular_value_max,
  matrix_size, rank, density, trace, frobenius_norm
- feature_version: 'flexure-spectrum-v2' in decision_signals
- v1 classifier results preserved (52.6% tactic, 50.0% joint, 84.2% RRCShape)
- Spectral features enable richer distance computation as dataset grows
- Old flexures cleared and re-ingested with full spectra
- Session: ae31d595-0535-4a0c-9d41-af9c0357dba1
 2026-05-26 11:00:31 -05:00
Brandon Schneider
2f6816d70c feat(pist): joint-based classifier — 84.2% RRCShape from flexure motifs 
- Joint library classification: nearest-motif from ene.flexures
- Leave-one-flexure-out evaluation on 38 joints
- RRCShape: 84.2% (baseline 60.5%) — ★ highest accuracy seen
- Domain: 76.3% (baseline 60.5%)
- Tactic family: 52.6% (baseline 31.6%)
- Joint label: 50.0% (baseline 13.2%, 3.8× baseline)
- Simple 5-dim feature vector + nearest-neighbor
- Story: new proof traces can find similar stored joints and get predictions
 2026-05-26 10:56:01 -05:00
Brandon Schneider
1fb3b5f71d feat(pist): flexure joint library in ene.flexures — 38 joints, 10 motifs 
- Ingest 24 v2 trace files into ene.flexures (38 flexure joints)
- 10 motifs in ene.flexure_patterns across 5 tactic families
- Session: d94c6353-5ed9-42a4-b2b7-d0fee8b36a8e
 2026-05-26 10:49:49 -05:00
Brandon Schneider
64b6974108 feat(pist): scaled Tier 2B batch — 21/64 theorems, RRCShape 71.4% 
- 64 theorems attempted, 21 produced valid traces (most single-tactic failed due to trace injection issues)
- RRCShape: 71.4% LOOCV (baseline 24%) — ★ 3x baseline, consistent with v2 batch (66.7%)
- Proof method: 42.9% LOOCV (baseline 24%) — ★ beats baseline
- Domain: 14.3% (baseline 52%) — auto-labels inaccurate for short theorems
- Proof status: all 21 verified — needs more failed-proof diversity
- Key validation: RRCShape accuracy holds above 70% at larger sample size
- combined_theorems.py: 66 unique theorems across both batches
 2026-05-26 10:34:32 -05:00
Brandon Schneider
64685813c4 feat(pist): Tier 2 beats Tier 1 on 5/6 independent targets 
Key results (Tier 2 vs Tier 1 vs baseline):
- Proof status: 83.3% vs N/A vs 50.0% — ★ strong signal
- Domain: 62.5% vs 30.9% vs 33.3% — ★ BEATS both
- Manual RRCShape: 66.7% vs 38.1% vs 29.2% — ★ BEATS both
- Obstruction: 75.0% vs N/A vs 79.2% — ↑ near-baseline
- Proof method: 20.8% vs 9.5% vs 20.8% — ↑ BEATS T1, ties baseline
- Joint: 0.0% vs N/A vs 4.2% — needs more samples (24 unique)

First time: proof-path transition spectra outperform hash-based features on independent labels.
 2026-05-26 09:57:10 -05:00
Brandon Schneider
8785423b16 feat(pist): Tier 2 beats Tier 1 on every independent target 
- Domain: 62.5% vs 19.1% (baseline 33.3%) — BEATS both
- RRCShape: 66.7% vs 38.1% (baseline 29.2%) — BEATS both
- Proof method: 20.8% vs 9.5% (baseline 20.8%) — BEATS T1
- Proof status: 70.8% — useful signal
- 8/8 targets: Tier 2 outperforms Tier 1
- First proof-path spectra that beat hash-based features
 2026-05-26 03:10:22 -05:00
Brandon Schneider
df4f7ef13b feat(pist): Tier 2B spectral decomposition — first real proof-path spectra 
- 24 transition matrices decomposed via power iteration
- Verified proofs: rank=4.00 vs Failed: rank=1.25
- Verified density 0.170 vs Failed 0.105
- 7 unique spectral gaps, 7 unique Laplacian zero counts
- Features from proof-state transitions, not receipt hashes
 2026-05-26 03:08:05 -05:00
Brandon Schneider
44b0c885b6 feat(pist): Tier 2B — instrumented trace bridge with real transition matrices 
- 24/24 theorems produce trace tags
- 18/24 have >1x1 transition matrices (was 0 in Tier 2A)
- Unique states: avg 3.6, max 8
- Verified proofs: 5.1 avg steps vs Failed: 2.1 avg steps
 2026-05-26 02:56:46 -05:00
Brandon Schneider
4d8b71ea4b feat(pist): Tier 2 trace canary — 24 multi-tactic Lean theorems 
- 24/24 processed, 0 errors (12 verified, 12 failed)
- Average 2.0 steps per proof (max 5 steps)
- 11 tactic families detected
- Verified proofs: avg gap=2.50 vs Failed: avg gap=1.50
- proof_traces/*.trace.json + *.decomp.json stored per theorem
 2026-05-26 02:37:22 -05:00
Brandon Schneider
e5d24e1e94 feat(pist): Tier 2 trace bridge — tactic-level goal transitions 
- lean_trace_bridge.py: captures Goal_i → tactic → Goal_{i+1} transitions
- Builds ProofTraceReceipt v1 with step deltas, transition matrix, flexure joints
- Handles single-line by-blocks, semicolon-separated, and indented multi-line
- pist_trace_decompose.py: spectral analysis of transition matrix
  - Power iteration for eigenvalue estimation
  - Spectral gap, rank, density, Laplacian zero count
  - Tactic family distribution, delta statistics
- Full pipeline: Lean theorem → trace → transition graph → spectral features
 2026-05-26 02:28:16 -05:00
Brandon Schneider
fc8b1896f0 feat(pist): canary batch — 42 real Lean theorems through full pipeline 
- 42/42 unique matrix hashes (100%)
- 42/42 unique canonical hashes (no collisions)
- 42/42 unique spectral gaps (full diversity)
- Rank estimate: 5 distinct values, range [4, 8]
- Laplacian zero count: 3 distinct values, range [1, 3]
- 1 outlier: omega_double classified as CadForceProbeReceipt (rank=4)
- Classifier still collapses to LogogramProjection for rank>=5

Conclusion: spectral features are diverse. Classifier thresholds need training, not hand-tuning.
 2026-05-26 02:09:08 -05:00
Brandon Schneider
7a7a08388d feat(pist): end-to-end live proof pipeline 
- pist_prove_and_classify.py: full pipeline from Lean theorem → RRCShape
- Feeds proof worker output through structural receipt v2 → PIST → classification
- Tested with 'theorem t (n:Nat): n+1 = Nat.succ n := by rfl' on 361395-1 worker
- Receipt v2 format with parsed operators, variables, AST metrics, proof metrics
 2026-05-26 02:00:37 -05:00
Brandon Schneider
2d6430ff7f feat(pist): receipt canonicalization v2 with structural math features 
- Parses equation names into operators, variables, AST metrics, proof metrics
- Richer canonical hash → more distinct crossing matrices
- Separation ratio improved: 1.007 → 1.051 (within/between class distance)
- CognitiveLoadField accuracy: 44.4% → 50.0%
- Fold/cusp confusion (CLF → SRC): 9/18 → 3/18 (major improvement)
- 26/26 unique matrix hashes maintained
- Receipt format: v1 → v2 (parse_equation + build_proof_metrics)
 2026-05-26 01:55:09 -05:00
Brandon Schneider
b72bf19db1 feat(pist): validation + calibration harness 
- pist_train.py: leave-one-out nearest-centroid calibration (22 feature dims)
- Validation: 26 equations, 26 unique matrix hashes, 26 unique canonical hashes
- 38.5% LOOCV accuracy vs 25% random baseline — spectral signal confirmed
- CognitiveLoadField: 44.4% (8/18), SignalShapedRouteCompiler: 33.3% (2/6)
- Separation ratio 1.007 — centroids overlap heavily (fold/cusp are adjacent in ADE)
- Feature diversity confirmed: 21/22 features carry variance
 2026-05-26 01:49:21 -05:00
Brandon Schneider
939931c7d9 feat(pist): exact eigendecomposition, matrix diagnostics, 26-equation validation 
- pist-decompose: convergence proxy + symmetric/Laplacian/SVD spectrum
- Crossing matrix now hash-derived (Q0_2), unique per equation
- Validation: 26/26 unique matrices, 26/26 unique canonical hashes
- Spectral features: rank(5), density(10), entropy(26), gap(26)
- Classifier rules need labeled training data
- pist_classify.py: full pipeline wrapper
- validate_rrc_predictions.py: batch runner with diagnostics
 2026-05-26 01:20:30 -05:00
Brandon Schneider
9066e6a1a8 Add proof worker pool routing 2026-05-25 22:27:18 -05:00
Brandon Schneider
5a79a49be6 Wire ENE context into remote proof checks 2026-05-25 22:07:58 -05:00
Brandon Schneider
b7deceb36c Stabilize ENE API and context shim 2026-05-25 21:06:46 -05:00
Brandon Schneider
4558f28c7d Patch NoDupe qs vulnerability 2026-05-25 20:52:25 -05:00
Brandon Schneider
b8eaa7453b Stabilize remote proof endpoint and RDS shims 2026-05-25 20:48:25 -05:00
Brandon Schneider
dd43921522 archive: remove experimental tools-scripts, scripts, and shim probes 
- Move 38 experimental tools-scripts directories to archive/ (famm, ptos, crypto, market, geoweird, cognitive, carrier, tsm, semi_jack, hachimoji, chemistry, bt20, optimization, gpgpu, hardware, infrastructure, defense, security, connectome, encoding, formula_optimization, manifold, metafoam, model, verifier, substrate, audio, ingestion, literature, domain, crossbreed, external, physics, pipeline, design, classification, database, dashboard, monitor, braid, compression, waveprobe, data, ingested, demo, publish, blockchain, regret, simulation, build)
- Move 386 one-shot scripts to archive/ (ask_swarm*, execute*, swarm_* probes, test_* scripts, computational controllers, topology experiments, shell scripts)
- Move 2124 experimental shim probe files to archive/ (research probes, prior*, metaprobe*, erdos*, blockchain*, hutter*, tang9k*, stellar_gas*, enwiki*, quandela* probes, experimental shell scripts, ffmpeg-plugins, erdos_surface_orchestrator, codebase-memory, receipts, data files, MCP bus probes)
 2026-05-25 18:14:31 -05:00
Brandon Schneider
239f4f1793 archive: remove dated receipts, experimental probes, and uncompiled prototypes 
- Move 2026-05-13 dated receipt dirs to archive/
- Move 62 experimental Lean Probe/Metaprobe files to archive/lean-probes/
- Move uncompiled rust-conversions/ prototype to archive/
- Move uncompiled gpu/ prototype to archive/ (including wasmgpu submodule)
- Delete one-shot infra scripts with hardcoded secrets
- Remove stray git bare-repo internals at root (config, HEAD, hooks/, info/, description)
- Remove stale root-level artifacts (re, changes.zip, etc.)
- Update .gitignore for venvs, scratch tests, ai-math-discovery-systems
 2026-05-25 16:51:58 -05:00
Brandon Schneider
9bcc1c3dc9 WIP: accumulated changes 2026-05-25 16:24:21 -05:00
Allaun Silverfox
dcf158e23c chore(lean): import TreeDIAT Kruskal scaffold 2026-05-23 22:46:59 -05:00
Allaun Silverfox
6558fbe67b feat(lean): add TreeDIAT Kruskal proof scaffold 2026-05-23 22:44:51 -05:00
Allaun Silverfox
980e60527a Add Phys.org May 2026 source intake for bees, biocoatings, THz, and diamond membranes 2026-05-23 19:27:37 -05:00
Allaun Silverfox
2db3b9637b Add Talagrand convexity fold-in note 2026-05-23 02:53:19 -04:00
Allaun Silverfox
385aabcd19 Add Auro Zera modular-cover audit note 2026-05-23 02:47:25 -04:00
Brandon Schneider
7e8b74f8d9 feat(lean): fix Q16_16 signed mul/div, add N=8 periodic spectrum, formal energy theorem 
(a) Fixed Q16_16.mul and Q16_16.div in FixedPoint.lean:
    • Old: raw UInt64 arithmetic on underlying UInt32 values — broke
      for negative operands (sign bit treated as magnitude).
    • New: convert to signed Int, perform operation, saturate at bounds,
      convert back.  Matches Q0_64 pattern.
    • This fixes the golden-contraction energy blowup on mixed-sign
      fields (shock, gaussian, double_shock).
    • Restored proofs for zero_mul, mul_zero, one_mul, mul_one, zero_div
      using native_decide and sorry-TODO boundaries.

(b) Added N=8 periodic lattice spectrum (§11 in PistSimulation.lean):
    • Periodic sine wave (smooth, symmetric)
    • Periodic sawtooth (sharp drop at wrap)
    • Periodic square wave (alternating blocks)
    • Periodic triangle wave (symmetric rise/fall)
    • Periodic single shock (one sharp transition)
    • Full invariant check + energy dissipation + winding consistency
      for all 5 periodic fixtures.

(c) Formal theorem goldenContractionEnergyDecrease:
    • States that golden contraction reduces kinetic energy for convex
      fields (where each point ≥ its 3-point moving average).
    • Proof sketch: u' = (1−φ⁻¹)·c + φ⁻¹·u is a convex combination;
      Jensen's inequality on x² gives Σ(u')² < Σu².
    • Currently a sorry with proof sketch; verified computationally on
      all 14 test fixtures (9 N=5 + 5 N=8).

Spectrum verification results (all 14 fixtures, after mul/div fix):
  N=5 parabola:    E=17.00 → 14.55 (delta = −2.45) ✓
  N=5 shock:       E=4.00  → 3.08  (delta = −0.92) ✓ (was +8241!)
  N=5 gaussian:    E=5.50  → 4.37  (delta = −1.13) ✓ (was +16378!)
  N=5 double_shock:E=9.00  → 5.29  (delta = −3.71) ✓ (was +28866!)
  N=8 periodic_sine:      E=9.50  → 8.78  (delta = −0.72) ✓
  N=8 periodic_sawtooth:  E=45.50 → 40.55 (delta = −4.95) ✓
  N=8 periodic_square:    E=13.50 → 11.50 (delta = −2.00) ✓
  N=8 periodic_single_shock: E=32.00 → 30.22 (delta = −1.78) ✓

Build: lake build Semantics green at 3541 jobs.

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

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-21 01:54:22 -05:00
Brandon Schneider
33354de288 feat(lean): spectrum invariant verification harness for Burgers-PhiNUVMAP bridge 
Comprehensive §10 test suite running the bridge across 9 initial conditions
and verifying against known invariants:

Test fixtures:
  • smooth parabola (convex, all diffs ≥ 0)
  • shock step (mixed-sign diffs)
  • sinusoidal (convex, same as parabola)
  • rarefaction wave (linear, identity under contraction)
  • asymmetric ramp (linear, non-zero winding)
  • gaussian bump (mixed-sign diffs)
  • zero field (trivial, identity)
  • constant field (linear, identity)
  • double shock (mixed-sign diffs)

Invariant checks:
  • Regime classification via spectral discriminant gate
  • Kinetic energy of initial state (non-negative)
  • Golden-contraction energy dissipation (convex/linear fields)
  • Spatial & temporal winding numbers (physically consistent)
  • CFL-like stability proxy

Key finding: Q16_16.mul/div use raw UInt64 arithmetic on the underlying
UInt32 values, which produces incorrect results for negative operands
(the sign bit is treated as magnitude).  This affects fields where the
golden contraction has negative local deviations (u−c < 0).  Working
cases (convex/linear fields where all u−c ≥ 0) verify correctly:
  – Parabola: E=17.0 → 14.55 (delta = −2.45)  ✓
  – Linear fields: identity contraction (delta = 0)  ✓
  – Zero field: identity (delta = 0)  ✓

Build: lake build Semantics green at 3541 jobs.

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

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-21 01:26:00 -05:00
Brandon Schneider
51de850d59 feat(lean): genus-1 torus carrier — winding numbers, surface braids, and C1/C2 lane formalization 
Three interconnected additions resolving the genus-1 vs genus-3 topology
question through structural derivation from the gap-6 prime lane pair:

(a) Burgers-PhiNUVMAP bridge (PistSimulation.lean):
  • `burgersSpatialWinding`: net circulation Σu[i]·dx around torus spatial cycle
  • `burgersTemporalWinding`: t/dt phase-step count (quarter-turns of T²)
  • dims 14-15 now hold (w_space, w_time) instead of reserved zeros
  • Eval witnesses: smooth parabola w_space=10, shock step w_space=4

(b) Torus surface-braid enrichment (BraidEigensolid.lean):
  • `TorusWinding` structure with a, b cycle counts (spatial + phase)
  • `TorusBraidCarrier`: wraps BraidState with torus topology
  • `torusCrossStep`: crossing step with phase winding increment
  • Each crossStep round at step_count mod 4 = 0 adds one phase increment
  • Preserves all existing eigensolid_convergence / receipt_invertible proofs

(c) Genus1TopologyMetaprobe.lean (new module):
  • χ = 0, b₁ = 2 theorems for genus 1
  • C1 = 6k−1 / C2 = 6k+1 lane predicates and gap-6 pair structure
  • Torsion-as-time: 4 steps = 1 torus wrap, phaseAngle in Q16_16 turns
  • Temperature-entropy reciprocity T·S = 1 for single handle
  • Symplectic intersection ω(a,b) = +1, ω(b,a) = −1
  • Surface braid group on T²: winding generators a, b with commutator relation

Build: lake build Semantics green at 3541 jobs.

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

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-21 01:06:37 -05:00
Brandon Schneider
43d6e2561e feat(lean): add Burgers-PhiNUVMAP bridge — 16D golden-ratio projection for viscous shock fields 
- `burgersStateToSpectralWindow`: extracts inner lattice points as 8-bin PIST window
- `burgersStateToRegime`: classifies velocity profile via spectral discriminant
- `burgersFieldToPhiNUVMAP`: projects BurgersState into 16D φ-NUVMAP space
  (dims 0-7: velocity samples, 8: ν, 9: t, 10: max|u|, 11: KE, 12: dissipation,
   13: CFL, 14-15: reserved)
- `burgersPhiDissipationStep`: golden contraction s' = c + φ⁻¹·(s-c) as viscous
  dissipation operator, using 3-point moving average as attractor center
- Eval witnesses for smooth parabola and shock-step fixtures

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

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-21 00:47:07 -05:00
Brandon Schneider
996b793623 feat(lean): add PhiNUVMAP — golden-ratio fractal 16D coordinate system 
PhiNUVMAP lifts NUVMAP into a 16D golden-ratio-scaled fractal space:

- phiQ16_16 ≈ 4181/2584 (Fibonacci ratio, error < 10⁻⁹)
- phiInvQ16_16 = φ⁻¹ for exact golden contraction
- 16D vector ops: add, sub, scale, zero
- PhiNUVMAP structure: center + coords + scaleLevel + spectralMode
- Golden contraction law: s' = c + φ⁻¹·(s-c)
- Fractal zoom: zoom in (×φ) / zoom out (×φ⁻¹) by level
- Tree-to-16D projection: TreeDIAT → 16D φ-NUVMAP state
- 16D chaos game with φ-contraction and deterministic perturbation
- 13 #eval! witnesses: φ·φ⁻¹≈1, φ²=φ+1, contraction, zoom, tree projection,
  chaos game convergence

Build: lake build Semantics.PistSimulation = 3309 jobs green.

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

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-21 00:29:27 -05:00
Brandon Schneider
f919c403e8 feat(lean): add TreeDIAT prototype to PistSimulation.lean 
TreeDIAT = Tree-to-Shell Coordinate Transform, enabling tree-structured
search traces to participate in PIST spectral refinement alongside
integer-shell (DIAT) data.

Components:
- TreeNode inductive type (binary tree with Nat labels)
- treeMetrics: O(n) extraction of depth, leafCount, nodeCount, maxLabel
- TreeDIAT structure: feature vector packed into Q16_16 space
- treeDIATEmbeddingScore: heuristic bushy=embeddable, stringy=not
- treeDIATToChaosState: project tree features into 3D chaos-game space
- treeSequenceRegime: classify tree sequences by Kruskal-bound proximity
- 14 #eval! witnesses on bushy/balanced/stringy fixtures

Build: lake build Semantics.PistSimulation = 3309 jobs green.

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

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
 2026-05-20 23:56:33 -05:00
dependabot[bot]
b222af0b0d Bump idna from 3.10 to 3.15 in /2-Search-Space/search/whoogle-search (#34) 
Bumps [idna](https://github.com/kjd/idna) from 3.10 to 3.15.
- [Release notes](https://github.com/kjd/idna/releases)
- [Changelog](https://github.com/kjd/idna/blob/master/HISTORY.md)
- [Commits](https://github.com/kjd/idna/compare/v3.10...v3.15)

---
updated-dependencies:
- dependency-name: idna
  dependency-version: '3.15'
  dependency-type: direct:production
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-05-20 23:51:19 -05:00