Successive integrated primitive collapses for R-324

This file constructs the analytic stages used by the corrected integrated R-324 reduction. A stage is the actual primitive kernel for a measurable admissible chain-input family; its measurability, class-E property, and Proposition 4.1 majorant are derived rather than postulated.

Measurability of genuine primitive kernels

theorem Anderson4D.measurable_primitiveIntegrand (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), Measurable (G j)) (κ : PartialPairing (Fin (2 * n))) : Measurable (primitiveIntegrand ρ ε n hn G κ)

The Proposition 4.1 integrand is jointly measurable in its complete tuple whenever every chain input is measurable.

theorem Anderson4D.measurable_primitiveIntegrand_assemble_zero (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), Measurable (G j)) (κ : PartialPairing (Fin (2 * n))) : Measurable fun (p : T4 × (Fin (2 * n - 2) → T4)) => primitiveIntegrand ρ ε n hn G κ (primitiveAssemble n hn p.1 0 p.2)

Joint measurability after assembling one free endpoint, one zero endpoint, and the internal primitive tuple.

theorem Anderson4D.measurable_primitiveKernelDiff (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)), Measurable (G j)) : Measurable (primitiveKernelDiff ρ lam ε n hn G)

The genuine primitive kernel supplied to a later collapse is measurable. This closes a condition not included in the bare IsAdmissiblePrimitiveInput predicate.

Proposition 4.1 produces actual analytic stages

noncomputable def Anderson4D.r324PrimitiveAnalyticStage (ρ : SmoothCutoff) (lam ε C supportConstant : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hGmeas : ∀ (j : Fin (2 * n - 1)), Measurable (G j)) (hreg : PrimitiveEstimateRegime n lam ε 1 supportConstant C) (hinput : IsAdmissiblePrimitiveInput n G) (hprop : Prop41BoundPredicate ρ lam ε n hn G 1 supportConstant C) : R322AnalyticStage C lam ε supportConstant

One genuine primitive kernel, with all R322AnalyticStage fields derived from Proposition 4.1.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.exists_r324PrimitiveAnalyticStage_at_truncation (ρ : SmoothCutoff) : ∃ (supportConstant : ℝ) (C : ℝ), 0 < supportConstant ∧ 0 < C ∧ ∀ (lam ε : ℝ) (n : ℕ), 1 ≤ n → ∀ (G : Fin (2 * n - 1) → T4 → ℝ), 0 < lam → 0 < ε → ε ≤ 1 → n ≤ truncOrder ε → (∀ (j : Fin (2 * n - 1)), Measurable (G j)) → IsAdmissiblePrimitiveInput n G → Nonempty (R322AnalyticStage C lam ε supportConstant)

The proved truncation-specialized Proposition 4.1 constructs the stage for any concrete measurable admissible input family.