R324PermCross: the factorial minorant of the pure-cross fibre

The summed pure-cross density of the full permutation fibre is bounded below by g₀^{2(m+1)} · m! · (2π)^{4(m+4)}: the two plain Green chains are at least g₀^{2(m+1)} almost everywhere (the Green floor), and each of the m! bijection entities contributes exactly one full covariance mass (2π)^{4(m+4)} — the periodized covariance has total mass one at every scale, and the m cross legs pair the 2m internal coordinates bijectively.

The bijection count m! survives because of injectivity: it is the exact cardinality of the pure-cross fibre.

The exact covariance mass

theorem Anderson4D.r324PermCross_integral_eta_eq_one (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) : ∫ (z : T4), ρ.etaEpsT4 ε z ∂paperMeasure = 1

Unit covariance mass. The periodized mollified covariance integrates to exactly ‖ρ̂(0)‖² = 1 at every scale 0 < ε.

theorem Anderson4D.r324PermCross_integral_eta_sub_eq_one (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (c : T4) : ∫ (w : T4), ρ.etaEpsT4 ε (c - w) ∂paperMeasure = 1

Shifted unit mass: ∫ η_ε(c - w) dw = 1 for every center c.

Bounded integrability on finite measures

theorem Anderson4D.r324PermCross_integrable_of_bounded {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {f : α → ℝ} {B : ℝ} (hmeas : Measurable f) (h0 : ∀ (x : α), 0 ≤ f x) (hB : ∀ (x : α), f x ≤ B) : MeasureTheory.Integrable f μ

instance Anderson4D.r324PermCross_instFiniteMeasurePi (n : ℕ) : MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.pi fun (x : Fin n) => paperMeasure)

instance Anderson4D.r324PermCross_instFiniteMeasurePhysical (m : ℕ) : MeasureTheory.IsFiniteMeasure (r324PhysicalMeasure m)

The pairing reindex of the internal coordinates

def Anderson4D.r324PermCrossPairEquiv (m : ℕ) : Fin m ⊕ Fin m ≃ Fin (2 * m)

The explicit left/right decomposition of the doubled carrier.

Equations

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

@[simp]

theorem Anderson4D.r324PermCrossPairEquiv_inl (m : ℕ) (i : Fin m) : (r324PermCrossPairEquiv m) (Sum.inl i) = leftMomentIndex i

@[simp]

theorem Anderson4D.r324PermCrossPairEquiv_inr (m : ℕ) (i : Fin m) : (r324PermCrossPairEquiv m) (Sum.inr i) = rightMomentIndex i

noncomputable def Anderson4D.r324PermCrossSplitEquiv (m : ℕ) : (Fin m → T4) × (Fin m → T4) ≃ᵐ (Fin (2 * m) → T4)

The measurable split of the doubled internal coordinates into the left and right halves.

Equations

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

theorem Anderson4D.r324PermCrossSplitEquiv_apply_left (m : ℕ) (a b : Fin m → T4) (i : Fin m) : (r324PermCrossSplitEquiv m) (a, b) (leftMomentIndex i) = a i

theorem Anderson4D.r324PermCrossSplitEquiv_apply_right (m : ℕ) (a b : Fin m → T4) (i : Fin m) : (r324PermCrossSplitEquiv m) (a, b) (rightMomentIndex i) = b i

theorem Anderson4D.r324PermCross_measurePreserving_splitEquiv (m : ℕ) : MeasureTheory.MeasurePreserving (⇑(r324PermCrossSplitEquiv m)) ((MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure).prod (MeasureTheory.Measure.pi fun (x : Fin m) => paperMeasure)) (MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure)

The split preserves the product Haar measure.

One covariance mass per pure-cross entity

theorem Anderson4D.r324PermCross_id_singles (m : ℕ) : PartialPairing.id.singles = Finset.univ

The identity pairing leaves every index single.

theorem Anderson4D.r324PermCross_card_id_singles (m : ℕ) : Fintype.card ↥PartialPairing.id.singles = m

Cardinality of the single set of the identity pairing.

theorem Anderson4D.r324PermCross_integral_crossProd_pi (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (m : ℕ) (π : ↥PartialPairing.id.singles ≃ ↥PartialPairing.id.singles) : (∫ (v : Fin (2 * m) → T4), momentCrossCovarianceProduct ρ ε m PartialPairing.id PartialPairing.id π v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure) = ((2 * Real.pi) ^ dim) ^ m

Exact covariance mass of one pure-cross entity: the physical v-integral of its cross-covariance product is one paper volume per internal coordinate pair.

Peeling the four external variables

theorem Anderson4D.r324PermCross_map_internal (m : ℕ) : MeasureTheory.Measure.map (fun (p : R324PhysicalPoint m) => p.2.2.2.2) (r324PhysicalMeasure m) = paperMeasure Set.univ ^ 4 • MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure

Pushforward of the physical measure onto the internal coordinates: four paper volumes times the internal product measure.

theorem Anderson4D.r324PermCross_integral_internal (m : ℕ) {F : (Fin (2 * m) → T4) → ℝ} (hF : Measurable F) : ∫ (p : R324PhysicalPoint m), F p.2.2.2.2 ∂r324PhysicalMeasure m = ((2 * Real.pi) ^ dim) ^ 4 * ∫ (v : Fin (2 * m) → T4), F v ∂MeasureTheory.Measure.pi fun (x : Fin (2 * m)) => paperMeasure

Integrals of internal-coordinate observables against the physical measure carry four paper volumes.

theorem Anderson4D.r324PermCross_integral_crossProd_physical (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (m : ℕ) (π : ↥PartialPairing.id.singles ≃ ↥PartialPairing.id.singles) : ∫ (p : R324PhysicalPoint m), momentCrossCovarianceProduct ρ ε m PartialPairing.id PartialPairing.id π p.2.2.2.2 ∂r324PhysicalMeasure m = ((2 * Real.pi) ^ dim) ^ (m + 4)

Physical covariance mass of one pure-cross entity.

Null diagonals on the physical space

theorem Anderson4D.r324PermCross_measurableSet_ne {A : Type u_1} [MeasurableSpace A] {f g : A → T4} (hf : Measurable f) (hg : Measurable g) : MeasurableSet {a : A | f a ≠ g a}

theorem Anderson4D.r324PermCross_ae_snd {A : Type u_1} {B : Type u_2} [MeasurableSpace A] [MeasurableSpace B] {μ : MeasureTheory.Measure A} {ν : MeasureTheory.Measure B} [MeasureTheory.SFinite ν] {P : B → Prop} (hP : MeasurableSet {b : B | P b}) (h : ∀ᵐ (b : B) ∂ν, P b) : ∀ᵐ (p : A × B) ∂μ.prod ν, P p.2

theorem Anderson4D.r324PermCross_ae_ne_x (m : ℕ) (j : Fin (2 * m)) : ∀ᵐ (p : R324PhysicalPoint m) ∂r324PhysicalMeasure m, p.1 ≠ p.2.2.2.2 j

The external x avoids every internal coordinate a.s.

theorem Anderson4D.r324PermCross_ae_ne_y (m : ℕ) (j : Fin (2 * m)) : ∀ᵐ (p : R324PhysicalPoint m) ∂r324PhysicalMeasure m, p.2.1 ≠ p.2.2.2.2 j

The external y avoids every internal coordinate a.s.

theorem Anderson4D.r324PermCross_ae_ne_z (m : ℕ) (j : Fin (2 * m)) : ∀ᵐ (p : R324PhysicalPoint m) ∂r324PhysicalMeasure m, p.2.2.1 ≠ p.2.2.2.2 j

The external z avoids every internal coordinate a.s.

theorem Anderson4D.r324PermCross_ae_ne_w (m : ℕ) (j : Fin (2 * m)) : ∀ᵐ (p : R324PhysicalPoint m) ∂r324PhysicalMeasure m, p.2.2.2.1 ≠ p.2.2.2.2 j

The external w avoids every internal coordinate a.s.

theorem Anderson4D.r324PermCross_ae_ne_vv (m : ℕ) {j j' : Fin (2 * m)} (hjj : j ≠ j') : ∀ᵐ (p : R324PhysicalPoint m) ∂r324PhysicalMeasure m, p.2.2.2.2 j ≠ p.2.2.2.2 j'

Distinct internal coordinates are a.s. distinct.

The almost-everywhere chain floor

theorem Anderson4D.r324PermCross_assemble_mid {m : ℕ} (x y : T4) (w : Fin m → T4) (j : Fin (m + 2)) (h0 : ↑j ≠ 0) (h1 : ↑j ≠ m + 1) : assemble x y w j = w ⟨↑j - 1, ⋯⟩

Interior slots of the assembled tuple.

theorem Anderson4D.r324PermCross_ae_assembled_edges (m : ℕ) (hm : 1 ≤ m) (emb : Fin m → Fin (2 * m)) (hemb : Function.Injective emb) (X Y : R324PhysicalPoint m → T4) (hX : ∀ (j : Fin (2 * m)), ∀ᵐ (p : R324PhysicalPoint m) ∂r324PhysicalMeasure m, X p ≠ p.2.2.2.2 j) (hY : ∀ (j : Fin (2 * m)), ∀ᵐ (p : R324PhysicalPoint m) ∂r324PhysicalMeasure m, Y p ≠ p.2.2.2.2 j) : ∀ᵐ (p : R324PhysicalPoint m) ∂r324PhysicalMeasure m, ∀ (e : Fin (m + 1)), assemble (X p) (Y p) (fun (i : Fin m) => p.2.2.2.2 (emb i)) e.castSucc ≠ assemble (X p) (Y p) (fun (i : Fin m) => p.2.2.2.2 (emb i)) e.succ

Almost every physical point has all edges of an assembled chain off the diagonal. Stated for either half through the index embedding emb (left or right copy) and external slots X, Y.

theorem Anderson4D.r324PermCross_leftMomentIndex_injective (m : ℕ) : Function.Injective leftMomentIndex

theorem Anderson4D.r324PermCross_rightMomentIndex_injective (m : ℕ) : Function.Injective rightMomentIndex

theorem Anderson4D.r324PermCross_ae_chains_floor (m : ℕ) (hm : 1 ≤ m) : ∀ᵐ (p : R324PhysicalPoint m) ∂r324PhysicalMeasure m, r324PermCrossGreenFloorConst ^ (2 * m + 2) ≤ r324LedgerThreeLeftChain m p * r324LedgerThreeRightChain m p

Almost everywhere both plain chains sit above the Green floor.

Integrability of the fibre summands

theorem Anderson4D.r324PermCross_integrable_summand (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (π : ↥PartialPairing.id.singles ≃ ↥PartialPairing.id.singles) : MeasureTheory.Integrable (fun (p : R324PhysicalPoint m) => r324LedgerThreeLeftChain m p * r324LedgerThreeRightChain m p * momentCrossCovarianceProduct ρ ε m PartialPairing.id PartialPairing.id π p.2.2.2.2) (r324PhysicalMeasure m)

One pure-cross summand of the density is integrable: it is the real part of the proved integrable flat contraction term at trivial external modes.

theorem Anderson4D.r324PermCross_integrable_crossProd_physical (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (π : ↥PartialPairing.id.singles ≃ ↥PartialPairing.id.singles) : MeasureTheory.Integrable (fun (p : R324PhysicalPoint m) => momentCrossCovarianceProduct ρ ε m PartialPairing.id PartialPairing.id π p.2.2.2.2) (r324PhysicalMeasure m)

One cross-covariance product is integrable on the physical space.

The factorial minorant

theorem Anderson4D.r324PermCross_card_equiv (m : ℕ) : Fintype.card (↥PartialPairing.id.singles ≃ ↥PartialPairing.id.singles) = m.factorial

Number of pure-cross permutation entities.

theorem Anderson4D.r324PermCross_integral_crossDensity_ge (ρ : SmoothCutoff) {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) {m : ℕ} (hm : 1 ≤ m) : r324PermCrossGreenFloorConst ^ (2 * m + 2) * (↑m.factorial * ((2 * Real.pi) ^ dim) ^ (m + 4)) ≤ ∫ (p : R324PhysicalPoint m), r324LedgerThreeCrossDensity ρ ε m (r324LedgerThreePermEntities m) p ∂r324PhysicalMeasure m

The factorial minorant of the summed pure-cross fibre: the physical integral of the full permutation-fibre density is at least g₀^{2m+2} · m! · (2π)^{4(m+4)}.