LF4 general-N Slice E (bridge): ℝ^{N×2} Gaussian → Exp(1/2)^{⊗N}

Category: 3-Local (ℝ^{N×2} Gaussian → Exp(1/2)^{⊗N}).

The bridge connecting the standard Gaussian on ℝ^{N×2} (indexed by the product Fin N × Fin 2, the real coordinate space behind gaussianHN) to the N-fold product Exp(1/2)^{⊗N} that Slice D (ratioSqNorm_map_expHalf_pi) consumes.

The per-block squared-norm map y ↦ (i ↦ y(i,0)² + y(i,1)²) pushes gaussianReal^{⊗(N×2)} to expHalf^{⊗N}. The proof regroups the product index via map_curryProd_pi (the Cat-1 product-index curry, PiCurry.lean), then applies the per-factor map lemma Measure.pi_map_pi with the single-block fact

(fun w : Fin 2 → ℝ => (w 0)² + (w 1)²)∗ gaussianReal^{⊗2} = expHalf   (E1).

This bypasses Slice C (blockSqNorm_map_gaussianN_pi, which routed through pi (Fin N) gaussian2): currying lands directly on pi (Fin N) (pi (Fin 2) gaussianReal), so the single-block computation is the Fin-2 form of Slice 1, not the gaussian2 explicit-density form. See specs/general-n-dh-plan.md Slice E.

noncomputable def CSD.LF4.gBlock : (Fin 2 → ℝ) → ℝ

The single-block squared-norm map on Fin 2 → ℝ.

Equations

• CSD.LF4.gBlock w = w 0 ^ 2 + w 1 ^ 2

theorem CSD.LF4.measurable_gBlock : Measurable gBlock

theorem CSD.LF4.gBlock_map_pi : MeasureTheory.Measure.map gBlock (MeasureTheory.Measure.pi fun (x : Fin 2) => ProbabilityTheory.gaussianReal 0 1) = expHalf

E1. The single-block squared norm pushes the 2-fold standard Gaussian to Exp(1/2): (fun w => w₀² + w₁²)∗ gaussianReal^{⊗2} = expHalf. The Fin 2 → ℝ form of sqNorm_map_gaussian2 (Slice 1), routed through measurePreserving_piFinTwo and gaussian2_eq_prod.

theorem CSD.LF4.blockSqNormCurry_map_pi {N : ℕ} : MeasureTheory.Measure.map (fun (y : Fin N × Fin 2 → ℝ) (i : Fin N) => y (i, 0) ^ 2 + y (i, 1) ^ 2) (MeasureTheory.Measure.pi fun (x : Fin N × Fin 2) => ProbabilityTheory.gaussianReal 0 1) = MeasureTheory.Measure.pi fun (x : Fin N) => expHalf

E2 (the bridge). The per-block squared-norm map y ↦ (i ↦ y(i,0)² + y(i,1)²) pushes the standard Gaussian on ℝ^{N×2} (gaussianReal^{⊗(N×2)}) to the N-fold product Exp(1/2)^{⊗N}.