The first genuine signed block update in R-324

This file connects the stable first-left coordinate of the R-324 within-half fibre to the actual deterministic covariance factor carried by that contraction. In particular, the primitive coordinate exposed by r324FirstLeftReconstruct is proved to be the ordered pairing seen by the original integrand; it is not introduced as an unrelated proxy.

The actual selected spatial tuple

noncomputable def Anderson4D.r324FirstLeftSelectedCoordinateEquiv {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) ≃ { i : Fin (2 * m) // r324FirstLeftSelected e₀ hleft i }

Increasing block coordinates followed by the left-copy embedding give an equivalence with the selected doubled-coordinate subtype.

Equations

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

@[simp]

theorem Anderson4D.r324FirstLeftSelectedCoordinateEquiv_apply_val {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (i : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft))) : ↑((r324FirstLeftSelectedCoordinateEquiv e₀ hleft) i) = leftMomentIndex ↑((residualPrimitiveBlockOrderIso e₀.fst (selectedExtractionBlock e₀.fst Finset.univ hleft) ⋯) i)

noncomputable def Anderson4D.r324FirstLeftSelectedTupleMeasurableEquiv {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : (Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) → T4) ≃ᵐ ({ i : Fin (2 * m) // r324FirstLeftSelected e₀ hleft i } → T4)

Reindex selected doubled-coordinate tuples by their canonical increasing Fin (2n) block coordinate.

Equations

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

@[simp]

theorem Anderson4D.r324FirstLeftSelectedTupleMeasurableEquiv_apply {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (v : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) → T4) (i : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft))) : (r324FirstLeftSelectedTupleMeasurableEquiv e₀ hleft) v ((r324FirstLeftSelectedCoordinateEquiv e₀ hleft) i) = v i

theorem Anderson4D.measurePreserving_r324FirstLeftSelectedTupleMeasurableEquiv {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) : MeasureTheory.MeasurePreserving (⇑(r324FirstLeftSelectedTupleMeasurableEquiv e₀ hleft)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft))) => paperMeasure) (MeasureTheory.Measure.pi fun (x : { i : Fin (2 * m) // r324FirstLeftSelected e₀ hleft i }) => paperMeasure)

The selected-coordinate reindex preserves exactly the product of paper measures.

theorem Anderson4D.integral_r324FirstLeftSelected_eq_standardBlock {m : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (f : ({ i : Fin (2 * m) // r324FirstLeftSelected e₀ hleft i } → T4) → E) : (∫ (vB : { i : Fin (2 * m) // r324FirstLeftSelected e₀ hleft i } → T4), f vB ∂MeasureTheory.Measure.pi fun (x : { i : Fin (2 * m) // r324FirstLeftSelected e₀ hleft i }) => paperMeasure) = ∫ (u : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) → T4), f ((r324FirstLeftSelectedTupleMeasurableEquiv e₀ hleft) u) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft))) => paperMeasure

Bochner-integral form of the concrete selected-tuple reindex.

Endpoints and internal coordinates of the primitive block

noncomputable def Anderson4D.r324PrimitiveBlockTupleMeasurableEquiv (n : ℕ) (hn : 1 ≤ n) : (Fin (2 * n) → T4) ≃ᵐ (T4 × T4) × (Fin (2 * n - 2) → T4)

Split a positive-order standard block tuple into its two endpoints and its internal primitive coordinates.

Equations

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

@[simp]

theorem Anderson4D.r324PrimitiveBlockTupleMeasurableEquiv_symm_apply (n : ℕ) (hn : 1 ≤ n) (p : T4 × T4) (u : Fin (2 * n - 2) → T4) : (r324PrimitiveBlockTupleMeasurableEquiv n hn).symm (p, u) = primitiveAssemble n hn p.1 p.2 u

theorem Anderson4D.measurePreserving_r324PrimitiveBlockTupleMeasurableEquiv (n : ℕ) (hn : 1 ≤ n) : MeasureTheory.MeasurePreserving (⇑(r324PrimitiveBlockTupleMeasurableEquiv n hn)) (MeasureTheory.Measure.pi fun (x : Fin (2 * n)) => paperMeasure) ((paperMeasure.prod paperMeasure).prod (MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure))

The endpoint/internal split preserves the full paper product measure.

theorem Anderson4D.integral_standardBlock_eq_integral_endpoints_internal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (n : ℕ) (hn : 1 ≤ n) (f : (Fin (2 * n) → T4) → E) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : Fin (2 * n)) => paperMeasure)) : (∫ (t : Fin (2 * n) → T4), f t ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n)) => paperMeasure) = ∫ (p : T4 × T4), ∫ (u : Fin (2 * n - 2) → T4), f (primitiveAssemble n hn p.1 p.2 u) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure ∂paperMeasure.prod paperMeasure

Bochner integral over a positive standard block, with the endpoint pair outermost and all internal primitive coordinates innermost.

Translation of generalized primitive kernels

theorem Anderson4D.jChainEdgeWith_add_const {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (x : Fin n → T4) (a : T4) (e : Fin (n - 1)) : jChainEdgeWith G (fun (i : Fin n) => x i + a) e = jChainEdgeWith G x e

theorem Anderson4D.diffFactorJWith_add_const {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (x : Fin n → T4) (a : T4) (p : Fin n × Fin n) : diffFactorJWith G (fun (i : Fin n) => x i + a) p = diffFactorJWith G x p

theorem Anderson4D.jReplacementList_add_const {n : ℕ} (G : Fin (n - 1) → T4 → ℝ) (x : Fin n → T4) (a : T4) (ps : List (Fin n × Fin n)) : jReplacementList G (fun (i : Fin n) => x i + a) ps = jReplacementList G x ps

theorem Anderson4D.detJclosedIntegrandWith_add_const (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (σ : PartialPairing (Fin n)) (G : Fin (n - 1) → T4 → ℝ) (x : Fin n → T4) (a : T4) : (detJclosedIntegrandWith ρ ε n σ G fun (i : Fin n) => x i + a) = detJclosedIntegrandWith ρ ε n σ G x

The generalized closed primitive integrand contains only spatial differences, so simultaneous translation of all its vertices is exact.

theorem Anderson4D.primitiveAssemble_add_const (n : ℕ) (hn : 1 ≤ n) (z w a : T4) (u : Fin (2 * n - 2) → T4) : (primitiveAssemble n hn (z + a) (w + a) fun (i : Fin (2 * n - 2)) => u i + a) = fun (j : Fin (2 * n)) => primitiveAssemble n hn z w u j + a

theorem Anderson4D.detJWith_add_const (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (σ : PartialPairing (Fin (2 * n))) (z w a : T4) : detJWith ρ lam ε n hn G σ (z + a) (w + a) = detJWith ρ lam ε n hn G σ z w

Simultaneous endpoint translation leaves the generalized selected primitive kernel unchanged.

theorem Anderson4D.detJWith_eq_diff (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (σ : PartialPairing (Fin (2 * n))) (z w : T4) : detJWith ρ lam ε n hn G σ z w = detJWith ρ lam ε n hn G σ (z - w) 0

Difference form used literally by r322CollapseIntegrand.

The reconstructed contraction really carries the exposed pairing

@[simp]

theorem Anderson4D.r324FirstLeftReconstruct_leftPairing {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (κB : R324FirstLeftBlockCoordinate e₀ hleft) : (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).fst = ↑((reductionEndpointFiberEquivBlockComplement e₀.fst hleft).symm (κB, ω.fst))

@[simp]

theorem Anderson4D.r324FirstLeftReconstruct_rightPairing {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (κB : R324FirstLeftBlockCoordinate e₀ hleft) : (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).snd.fst = ↑ω.snd.fst

theorem Anderson4D.r324FirstLeftEndpointFiber_blockCoordinate {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (κB : R324FirstLeftBlockCoordinate e₀ hleft) : ((reductionEndpointFiberEquivBlockComplement e₀.fst hleft) ((reductionEndpointFiberEquivBlockComplement e₀.fst hleft).symm (κB, ω.fst))).1 = κB

The endpoint-fibre member used by the actual reconstruction has first block coordinate exactly κB.

Actual selected covariance factor

theorem Anderson4D.r324FirstLeftReconstruct_selectedCovariance_eq_primitiveCoordinate {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (κB : R324FirstLeftBlockCoordinate e₀ hleft) (v : Fin (2 * m) → T4) : (pairingCovarianceProductOn ρ ε (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).fst (selectedExtractionBlock e₀.fst Finset.univ hleft) fun (i : Fin m) => v (leftMomentIndex i)) = primitiveCovarianceProduct ρ ε (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) ↑κB fun (i : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft))) => v (leftMomentIndex ↑((residualPrimitiveBlockOrderIso e₀.fst (selectedExtractionBlock e₀.fst Finset.univ hleft) ⋯) i))

On the selected tuple, the covariance factor of the actual reconstructed contraction is exactly the standard primitive covariance factor indexed by κB.

theorem Anderson4D.r324FirstLeftReconstruct_complementCovariance_eq_reference {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (κB : R324FirstLeftBlockCoordinate e₀ hleft) (v : Fin (2 * m) → T4) : (pairingCovarianceProductOn ρ ε (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).fst (Finset.univ \ selectedExtractionBlock e₀.fst Finset.univ hleft) fun (i : Fin m) => v (leftMomentIndex i)) = pairingCovarianceProductOn ρ ε (↑(firstBlockReferenceEndpointFiber e₀.fst hleft ω.fst)) (Finset.univ \ selectedExtractionBlock e₀.fst Finset.univ hleft) fun (i : Fin m) => v (leftMomentIndex i)

The complementary within-left covariance factor is genuinely independent of the exposed primitive coordinate.

theorem Anderson4D.r324FirstLeftReconstruct_leftCovariance_eq_primitive_mul_reference {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (κB : R324FirstLeftBlockCoordinate e₀ hleft) (v : Fin (2 * m) → T4) : (pairingCovarianceProductOn ρ ε (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).fst Finset.univ fun (i : Fin m) => v (leftMomentIndex i)) = (primitiveCovarianceProduct ρ ε (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) ↑κB fun (i : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft))) => v (leftMomentIndex ↑((residualPrimitiveBlockOrderIso e₀.fst (selectedExtractionBlock e₀.fst Finset.univ hleft) ⋯) i))) * pairingCovarianceProductOn ρ ε (↑(firstBlockReferenceEndpointFiber e₀.fst hleft ω.fst)) (Finset.univ \ selectedExtractionBlock e₀.fst Finset.univ hleft) fun (i : Fin m) => v (leftMomentIndex i)

Exact selected-block/complement factorization of the actual reconstructed within-left covariance product.

The stabilized cross coordinate is analytically unchanged

theorem Anderson4D.momentCrossCovarianceProduct_transport_leftSingles {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κp κp' κm : PartialPairing (Fin m)) (hsingles : κp.singles = κp'.singles) (π : ↥κp'.singles ≃ ↥κm.singles) (v : Fin (2 * m) → T4) : momentCrossCovarianceProduct ρ ε m κp κm ((finsetSubtypeEquivOfEq hsingles).trans π) v = momentCrossCovarianceProduct ρ ε m κp' κm π v

Value-preserving transport of the subtype of left singles does not change the actual cross-covariance product.

theorem Anderson4D.r324FirstLeftReconstruct_crossCovariance_eq_reference {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (κB : R324FirstLeftBlockCoordinate e₀ hleft) (v : Fin (2 * m) → T4) : momentCrossCovarianceProduct ρ ε m (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).fst (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).snd.fst (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).snd.snd v = momentCrossCovarianceProduct ρ ε m (↑(firstBlockReferenceEndpointFiber e₀.fst hleft ω.fst)) (↑ω.snd.fst) ω.snd.snd v

The cross-covariance factor of the reconstructed contraction is independent of κB; the transport used in r324FirstLeftReconstruct preserves every ambient endpoint.

All remaining factors are a genuine outer coordinate

theorem Anderson4D.pairingCovarianceProductOn_univ_eq_pairSupport {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin m)) (v : Fin m → T4) : pairingCovarianceProductOn ρ ε κ Finset.univ v = ∏ i ∈ κ.pairSupport with i < κ i, ρ.etaEpsT4 ε (v i - v (κ i))

Generic whole-carrier form of the within-copy covariance product.

theorem Anderson4D.r324FirstLeftReconstruct_greenSkeleton_eq_reference {m : ℕ} (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (κB : R324FirstLeftBlockCoordinate e₀ hleft) : renormalizedGreenSkeleton (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).fst = renormalizedGreenSkeleton ↑(firstBlockReferenceEndpointFiber e₀.fst hleft ω.fst)

The signed left Green skeleton of the actual reconstructed contraction is the reference skeleton stored by the outer coordinate.

noncomputable def Anderson4D.r324FirstLeftOuterFactor {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (α β : Z4) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (x y z w : T4) (v : Fin (2 * m) → T4) : ℂ

Every factor other than the selected primitive covariance coordinate. This is built from the actual reference contraction carried by ω, not from an arbitrary replacement integrand.

Equations

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

theorem Anderson4D.deterministicMomentIntegrand_r324FirstLeftReconstruct_eq {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (α β : Z4) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (κB : R324FirstLeftBlockCoordinate e₀ hleft) (x y z w : T4) (v : Fin (2 * m) → T4) : deterministicMomentIntegrand ρ ε m α β (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).fst (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).snd.fst (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).snd.snd x y z w v = r324FirstLeftOuterFactor ρ ε α β e₀ hleft ω x y z w v * ↑(primitiveCovarianceProduct ρ ε (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) ↑κB fun (i : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft))) => v (leftMomentIndex ↑((residualPrimitiveBlockOrderIso e₀.fst (selectedExtractionBlock e₀.fst Finset.univ hleft) ⋯) i)))

Actual pointwise first-left identification.

The original deterministic moment integrand evaluated at the contraction reconstructed from (ω, κB) is the κB-independent outer factor times the standard primitive covariance factor on the selected spatial tuple.

theorem Anderson4D.sum_deterministicMomentIntegrand_r324FirstLeftReconstruct_eq {m : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (α β : Z4) (e₀ : MomentContraction m) (hleft : ∃ (a : Fin m) (b : Fin m), IsRelFullyPaired e₀.fst Finset.univ a b) (ω : R324FirstLeftOuterCoordinate e₀ hleft) (x y z w : T4) (v : Fin (2 * m) → T4) : ∑ κB : R324FirstLeftBlockCoordinate e₀ hleft, deterministicMomentIntegrand ρ ε m α β (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).fst (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).snd.fst (↑(r324FirstLeftReconstruct e₀ hleft ω κB)).snd.snd x y z w v = r324FirstLeftOuterFactor ρ ε α β e₀ hleft ω x y z w v * ∑ κB : R324FirstLeftBlockCoordinate e₀ hleft, ↑(primitiveCovarianceProduct ρ ε (residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft)) ↑κB fun (i : Fin (2 * residualBlockOrder (selectedExtractionBlock e₀.fst Finset.univ hleft))) => v (leftMomentIndex ↑((residualPrimitiveBlockOrderIso e₀.fst (selectedExtractionBlock e₀.fst Finset.univ hleft) ⋯) i)))

Summing the actual reconstructed integrands over the complete primitive coordinate therefore forms the signed primitive covariance sum before any norm is taken.