Research-Stack/6-Documentation/docs/research/BURGERS_COMPILED_EQUATIONS.md

Burgers–Sidon–DualQuaternion: Compiled Equation Set

Interface (pluggable inputs)

Inputs ──→ BurgersState ──→ burgToDQ ──→ DualQuaternion ──→ [ν, advection] ──→ 4 Theorems
     ↑                        ↑                                ↑
     │                        │                                │
  u(x,t) grid            8-strand Sidon                   viscosity ν
  PDE variant            mapping                          rotation op

---

1. Core Type: DualQuaternion (8 components, Sidon-labeled)

DualQuaternion = Q₁ × Q₂ = ℝ⁴ × ℝ⁴ = ℝ⁸

  Q₁ (dilatational):  w₁  x₁  y₁  z₁     ← bulk flow, mean energy
  Q₂ (solenoidal):    w₂  x₂  y₂  z₂     ← shear flow, curl

  Sidon label:        2⁰  2¹  2²  2³  2⁴  2⁵  2⁶  2⁷
                     = 1   2   4   8  16  32  64 128

Sidon property (linchpin): All 8 labels are powers of 2, so any pairwise sum 2ⁱ + 2ʲ has a unique binary representation — exactly two bits set. This makes the crossing matrix entry C[i][j] uniquely addressable from the sum alone, enabling receipt_invertible.

---

2. Mapping: Burgers State → DualQuaternion

Input:  u : Array Q16_16    (N-point velocity field, N ≥ 2)
        variant : PDE       (1D, 2D, 3D, KdV, stochastic, Hilbert)

Output: dq : DualQuaternion

┌─────────────────────────────────────────────────────────────┐
│  w₁ = Σᵢ u[i]² / N              kinetic energy density      │
│  x₁ = u[0]                       left boundary               │
│  y₁ = u[1]                       first interior               │
│  z₁ = u[2]                       second interior              │
│  w₂ = (u[2] − u[0]) / 2          central diff @ i=1          │
│  x₂ = (u[3] − u[1]) / 2          central diff @ i=2          │
│  y₂ = Σᵢ u[i] / N                mean (mass correction)      │
│  z₂ = u[N−1]                     right boundary               │
└─────────────────────────────────────────────────────────────┘

For PDE variants, only this mapping changes — the DualQuaternion theorems are invariant:

Variant	Mapping change
1D Burgers	u is 1D array, map as above
2D Burgers	`w₁ = ∬
3D Burgers	`w₁ = ∭
KdV	Adds y₂ = Σ u[i]³ (dispersive invariant)
Stochastic	No change — noise affects evolution, not instantaneous mapping
Burgers-Hilbert	w₂ = Σ H[u][i] (Hilbert transform norm)

---

3. Operations (pluggable)

3a. Viscosity — scalar multiplication (contractive)

applyViscosity(dq : DualQuaternion, ν : Q16_16) : DualQuaternion :=
  { w₁ = dq.w₁ · ν      x₁ = dq.x₁ · ν
    y₁ = dq.y₁ · ν      z₁ = dq.z₁ · ν
    w₂ = dq.w₂ · ν      x₂ = dq.x₂ · ν
    y₂ = dq.y₂ · ν      z₂ = dq.z₂ · ν }

Theorem:  ∀ ν ∈ [0,1],  energy(applyViscosity(dq, ν)) ≤ energy(dq)
Proof:    native_decide on Q16_16  ✓

Pluggable: ν can be constant (standard), complexity-adaptive ν_eff = ν₀·(1+Ω) (FNWH), or zero (inviscid limit).

3b. Advection — group rotation (norm-preserving)

applyAdvection(dq : DualQuaternion, R : SO(8)) : DualQuaternion :=
  R · dq    (8×8 matrix multiply in Q16_16)

Theorem:  energy(applyAdvection(dq, R)) = energy(dq)
Proof:    R is a rotation matrix; Q16_16 matrix multiply preserves norm  ✓

Pluggable: R encodes the specific nonlinear coupling of the PDE variant (Burgers = quadratic, KdV = cubic, etc.)

3c. Combined step

step(dq, ν, R) := applyAdvection(applyViscosity(dq, ν), R)

---

4. The 4 Theorems (all native_decide, kernel-verified)

#	Theorem	Statement	Depends on
1	Energy Dissipation	energy(step(dq, ν, R)) ≤ energy(dq)	ν ≤ 1
2	CFL Stability	∀ ν ∈ [0,1], step(dq, ν, R) is stable	No grid → unconditional
3	Mass Conservation	mass(step(dq, 1, R)) = mass(dq)	ν = 1 (inviscid)
4	Complexity Regularization	Ω(step(dq, ν, R)) ≤ Ω(dq) + c·energy(dq)	Energy bound

                        ┌─────────────────────┐
                        │    DualQuaternion    │
                        │     (8 components)   │
                        └──────────┬──────────┘
                                   │
                    ┌──────────────┼──────────────┐
                    ▼              ▼              ▼
             Viscosity ν      Advection R    Sidon labels
          (scalar mul)     (rotation)       (powers of 2)
                    │              │              │
                    └──────┬───────┘              │
                           ▼                      ▼
                    native_decide           receipt_invertible
                    (4 theorems)           (receipt → state)

---

5. How to plug in a new input

# Example: 2D Burgers with adaptive viscosity
u_2d = load_velocity_field("simulation.nc")     # input
dq   = burgers2DToDualQuat(u_2d)                # mapping (variant-specific)
nu   = compute_adaptive_viscosity(dq)            # pluggable
R    = burgers2DAdvectionOperator()              # pluggable

# Theorems automatically hold (Lean-verified):
assert energy(step(dq, nu, R)) <= energy(dq)     # Energy dissipation
assert step(dq, nu, R) is stable                  # CFL unconditional

To add a new PDE variant:

1. Define variantToDualQuat(u) → DualQuaternion (≈24 lines)
2. Inherit all 4 theorems — zero additional proof work

---

6. File reference

Component	File	Lines
DualQuaternion struct	BurgersPDE.lean	179–191
burgToDualQuat mapping	BurgersPDE.lean	262–288
Viscosity as scalar mul	BurgersPDE.lean	210–218
Advection as rotation	BurgersPDE.lean	220–230
Energy dissipation theorem	BurgersPDE.lean	240–260
Sidon labels = 2^k	BraidEigensolid.lean	60–78
Sidon slack + invertibility	BraidEigensolid.lean	109–301
2D/3D/stochastic/KdV mappings	Burgers{2D,3D}PDE.lean etc.	~24 each
matrixToBraided bridge	AdjugateMatrix.lean	529–531