Root integrability for the initial two-half R-324 density

The certified within-half iteration starts from the literal all-Green residual prefixes. This file establishes the root input: joint integrability of the genuine marked physical density on the full five-group product space. Any later passage to endpoint sections must use Fubini and therefore be stated almost everywhere; fixed-endpoint Green sections need not be integrable on exceptional diagonals.

The initial sparse carrier and the standard internal carrier

def Anderson4D.R324WithinHalfResidualPrefix.initialEquivSurviving (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) : Fin m ≃ (initial ρ lam ε pairing).SurvivingCoordinate

Before any within-half block is removed, the sparse carrier is exactly the ordinary internal index type.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.initialPiMeasurableEquiv (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) : ((initial ρ lam ε pairing).SurvivingCoordinate → T4) ≃ᵐ (Fin m → T4)

Measurable reindex from the initial sparse tuple to the standard Fin m tuple.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.measurePreserving_initialPiMeasurableEquiv (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) : MeasureTheory.MeasurePreserving (⇑(initialPiMeasurableEquiv ρ lam ε pairing)) (MeasureTheory.Measure.pi fun (x : (initial ρ lam ε pairing).SurvivingCoordinate) => paperMeasure) (MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure)

The initial carrier reindex preserves product Haar measure.

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.initialPiMeasurableEquiv_apply (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) (v : (initial ρ lam ε pairing).SurvivingCoordinate → T4) (i : Fin m) : (initialPiMeasurableEquiv ρ lam ε pairing) v i = v ((initialEquivSurviving ρ lam ε pairing) i)

theorem Anderson4D.R324WithinHalfResidualPrefix.initial_reconstruct_eq (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) (v : (initial ρ lam ε pairing).SurvivingCoordinate → T4) : (initial ρ lam ε pairing).reconstruct v = (initialPiMeasurableEquiv ρ lam ε pairing) v

The sparse reconstruction is literally the standard tuple at the all-active initial state.

Pointwise form of the initial within-half residual

theorem Anderson4D.R324WithinHalfResidualPrefix.initial_activeEdgeSlots (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) : (initial ρ lam ε pairing).activeEdgeSlots = Finset.univ

Every production edge is active in the all-Green initial state.

theorem Anderson4D.R324WithinHalfResidualPrefix.initial_edgeSuccessor (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) (edge : Fin (m + 1)) : (initial ρ lam ε pairing).edgeSuccessor edge = edge.succ

At the all-active initial state, every production edge has its ordinary adjacent successor.

theorem Anderson4D.R324WithinHalfResidualPrefix.initial_mem_remainingOutgoingSlots_iff (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) (edge : Fin (m + 1)) : edge ∈ (initial ρ lam ε pairing).remainingOutgoingSlots ↔ edge ∈ extractedRightEdges pairing

The initial reserved outgoing slots are precisely the extraction right edges, independently of the analytic reordering.

theorem Anderson4D.R324WithinHalfResidualPrefix.initial_residualChainEdgeFactor_complex_eq (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) (x y : T4) (v : Fin m → T4) (edge : Fin (m + 1)) : ↑((initial ρ lam ε pairing).residualChainEdgeFactor x y v edge) = if edge ∈ extractedRightEdges pairing then 1 else originalGreenEdge (assemble x y v) edge

One initial sparse chain factor is the corresponding ordinary Green edge unless that edge is reserved for an extracted difference.

theorem Anderson4D.R324WithinHalfResidualPrefix.initial_residualChainProduct_complex_eq (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) (x y : T4) (v : Fin m → T4) : ↑((initial ρ lam ε pairing).residualChainProduct x y v) = ∏ edge : Fin (m + 1), if edge ∈ extractedRightEdges pairing then 1 else originalGreenEdge (assemble x y v) edge

The complete initial sparse chain is the ordinary chain part of the renormalized Green skeleton.

theorem Anderson4D.R324WithinHalfResidualPrefix.initial_residualStepDifference_complex_eq (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) (x y : T4) (v : Fin m → T4) (step : R322ExtractionStep m) : ↑((initial ρ lam ε pairing).residualStepDifference x y v step) = originalGreenEdge (assemble x y v) (extractedRightEdge step.1) - ↑(greenFn (assemble x y v (varIdx step.1.1) - assemble x y v (extractedRightEdge step.1).succ))

One initial residual difference is the literal extracted Green difference attached to its endpoint pair.

theorem Anderson4D.R324WithinHalfResidualPrefix.initial_residualDifferenceProduct_complex_eq (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) (x y : T4) (v : Fin m → T4) : ↑((initial ρ lam ε pairing).residualDifferenceProduct x y v) = (List.map (fun (p : Fin m × Fin m) => originalGreenEdge (assemble x y v) (extractedRightEdge p) - ↑(greenFn (assemble x y v (varIdx p.1) - assemble x y v (extractedRightEdge p).succ))) (extract pairing)).prod

The complete initial residual-difference product is the extraction-list factor in the renormalized Green skeleton.

theorem Anderson4D.R324WithinHalfResidualPrefix.initial_remainingBlockIndex_eq_analyticBlockEquiv (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) (j : Fin (r322AnalyticSchedule pairing).length) : (initial ρ lam ε pairing).remainingBlockIndex j = (r322AnalyticBlockEquiv pairing) j

At the initial state, the remaining-block coordinate is the canonical analytic-schedule block coordinate.

theorem Anderson4D.R324WithinHalfResidualPrefix.initial_residualPrimitiveProduct_eq (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) (v : Fin m → T4) : (initial ρ lam ε pairing).residualPrimitiveProduct ρ ε v = ∏ B : ExtractionBlockIndex pairing, r322ExtractionBlockPrimitiveSum ρ ε pairing B v

The initial primitive product contains every extraction block exactly once.

theorem Anderson4D.R324WithinHalfResidualPrefix.initial_residualIntegrand_complex_eq (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) (x y : T4) (v : Fin m → T4) : ↑((initial ρ lam ε pairing).residualIntegrand ρ ε x y v) = renormalizedGreenSkeleton pairing (assemble x y v) * ↑(∏ B : ExtractionBlockIndex pairing, r322ExtractionBlockPrimitiveSum ρ ε pairing B v)

Exact pointwise form of the genuine initial within-half residual: renormalized Green skeleton times all complete primitive block sums.

Bounded covariance factors

theorem Anderson4D.SmoothCutoff.measurable_r322ExtractionBlockPrimitiveSum (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) (B : ExtractionBlockIndex pairing) : Measurable (r322ExtractionBlockPrimitiveSum ρ ε pairing B)

One complete primitive block sum is measurable in the ambient within-half tuple.

theorem Anderson4D.SmoothCutoff.exists_norm_r322ExtractionBlockPrimitiveSum_le (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (pairing : PartialPairing (Fin m)) (B : ExtractionBlockIndex pairing) : ∃ (bound : ℝ), 0 ≤ bound ∧ ∀ (v : Fin m → T4), ‖r322ExtractionBlockPrimitiveSum ρ ε pairing B v‖ ≤ bound

At positive scale, one complete primitive block sum has a uniform pointwise norm bound.

theorem Anderson4D.SmoothCutoff.measurable_r324InitialPrimitiveBlockProduct (ρ : SmoothCutoff) (ε : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) : Measurable fun (v : Fin m → T4) => ∏ B : ExtractionBlockIndex pairing, r322ExtractionBlockPrimitiveSum ρ ε pairing B v

The product of all complete primitive block sums is measurable.

theorem Anderson4D.SmoothCutoff.exists_norm_r324InitialPrimitiveBlockProduct_le (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (pairing : PartialPairing (Fin m)) : ∃ (bound : ℝ), 0 ≤ bound ∧ ∀ (v : Fin m → T4), ‖∏ B : ExtractionBlockIndex pairing, r322ExtractionBlockPrimitiveSum ρ ε pairing B v‖ ≤ bound

The finite product of all complete primitive block sums has a uniform pointwise norm bound.

theorem Anderson4D.SmoothCutoff.measurable_r324ProjectedCovarianceC (ρ : SmoothCutoff) (ε L : ℝ) : Measurable (ρ.r324ProjectedCovarianceC ε L)

The projected covariance series is measurable in its spatial displacement.

noncomputable def Anderson4D.SmoothCutoff.r324CovarianceNormBudget (ρ : SmoothCutoff) (ε : ℝ) : ℝ

Absolute covariance-coefficient mass at one fixed mollification scale.

Equations

• ρ.r324CovarianceNormBudget ε = ∑' (k : Anderson4D.Z4), ‖ρ.covarianceModeCoeff ε k‖

theorem Anderson4D.SmoothCutoff.r324CovarianceNormBudget_nonneg (ρ : SmoothCutoff) (ε : ℝ) : 0 ≤ ρ.r324CovarianceNormBudget ε

theorem Anderson4D.SmoothCutoff.norm_r324ProjectedCovarianceC_le_budget (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (L : ℝ) (z : T4) : ‖ρ.r324ProjectedCovarianceC ε L z‖ ≤ ρ.r324CovarianceNormBudget ε

The high-mode projection is bounded by the full absolutely summable covariance Fourier mass.

theorem Anderson4D.SmoothCutoff.measurable_r324MarkedPairingCovarianceProductOn (ρ : SmoothCutoff) (ε L : ℝ) {n : ℕ} (pairing : PartialPairing (Fin n)) (marked : Fin n) (B : Finset (Fin n)) : Measurable (ρ.r324MarkedPairingCovarianceProductOn ε L pairing marked B)

A marked covariance product on a fixed active carrier is measurable.

theorem Anderson4D.SmoothCutoff.exists_norm_r324MarkedPairingCovarianceProductOn_le (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (L : ℝ) {n : ℕ} (pairing : PartialPairing (Fin n)) (marked : Fin n) (B : Finset (Fin n)) : ∃ (bound : ℝ), 0 ≤ bound ∧ ∀ (v : Fin n → T4), ‖ρ.r324MarkedPairingCovarianceProductOn ε L pairing marked B v‖ ≤ bound

At positive scale, a fixed marked covariance product is uniformly bounded. The estimate is intentionally coarse; only integrability is used at this stage.

The genuine marked root density

noncomputable def Anderson4D.SmoothCutoff.r324InitialTwoHalfMarkedPhysicalCore (ρ : SmoothCutoff) (lam ε : ℝ) {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (L : ℝ) (x y z w : T4) (v : Fin (2 * m) → T4) : ℂ

The uncollapsed two-half physical density at the literal all-Green within-half roots, with exactly the selected residual cross covariance Fourier-projected.

Equations

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

theorem Anderson4D.SmoothCutoff.integrable_r324Flatten_initialTwoHalfMarkedPhysicalCore (ρ : SmoothCutoff) {lam ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (selected : R324ResidualCovarianceSlot κp) (L : ℝ) : MeasureTheory.Integrable (r324Flatten (ρ.r324InitialTwoHalfMarkedPhysicalCore lam ε κp κm π selected L)) (r324PhysicalMeasure m)

The genuine marked initial root density is jointly integrable on the full five-group physical space.