Endpoint-first factorization of refined R-324 fibres

This file connects the abstract four-leg Fourier calculation in R324EndpointAggregate to the actual closed deterministic profiles. The first and last chain edges are removed from each renormalized Green skeleton, leaving a core which depends only on the internal variables.

The construction is deliberately pointwise and exact. In particular, a whole refined primitive-pairing/configuration fibre may be placed in the internal core before the four external variables are integrated.

Endpoint-independent chain edges

theorem Anderson4D.zero_not_mem_extractedRightEdges {m : ℕ} (κ : PartialPairing (Fin m)) : 0 ∉ extractedRightEdges κ

theorem Anderson4D.expandedGreenDifferenceFactor_eq_zeroEndpoints {m : ℕ} (κ : PartialPairing (Fin m)) (x y : T4) (v : Fin m → T4) (i : Fin (m + 1)) (hi0 : i ≠ 0) (hilast : i ≠ Fin.last m) : originalGreenEdge (assemble x y v) i - extractedShortcutGreenEdge κ (assemble x y v) i = originalGreenEdge (assemble 0 0 v) i - extractedShortcutGreenEdge κ (assemble 0 0 v) i

A nonendpoint edge of the uniform difference product is independent of both external variables.

noncomputable def Anderson4D.r324RenormalizedInteriorCore {m : ℕ} (κ : PartialPairing (Fin m)) (v : Fin m → T4) : ℂ

Internal difference-product core after deleting the two external chain edges.

Equations

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

Exact first/last edge factorization

noncomputable def Anderson4D.r324IncomingAnchor {m : ℕ} (_hm : 0 < m) (v : Fin m → T4) : T4

Internal anchor of the incoming external leg.

Equations

• Anderson4D.r324IncomingAnchor _hm v = Anderson4D.assemble 0 0 v (Fin.succ 0)

noncomputable def Anderson4D.r324OutgoingAnchor {m : ℕ} (_hm : 0 < m) (v : Fin m → T4) : T4

Ordinary internal anchor of the outgoing external leg.

Equations

• Anderson4D.r324OutgoingAnchor _hm v = Anderson4D.assemble 0 0 v (Fin.last m).castSucc

def Anderson4D.r324OutgoingIsShortcut {m : ℕ} (κ : PartialPairing (Fin m)) : Bool

Whether the final chain edge was replaced by an extracted endpoint difference.

Equations

• Anderson4D.r324OutgoingIsShortcut κ = decide (Fin.last m ∈ Anderson4D.extractedRightEdges κ)

noncomputable def Anderson4D.r324OutgoingShortcutAnchor {m : ℕ} (κ : PartialPairing (Fin m)) (v : Fin m → T4) : T4

The subtraction anchor of the outgoing leg. In the ordinary branch its value is irrelevant and is set to zero.

Equations

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

theorem Anderson4D.expandedGreenDifferenceFactor_zero {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (x y : T4) (v : Fin m → T4) : originalGreenEdge (assemble x y v) 0 - extractedShortcutGreenEdge κ (assemble x y v) 0 = r324IncomingEndpointKernel (r324IncomingAnchor hm v) (r324IncomingAnchor hm v) false x

theorem Anderson4D.expandedGreenDifferenceFactor_last {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (x y : T4) (v : Fin m → T4) : originalGreenEdge (assemble x y v) (Fin.last m) - extractedShortcutGreenEdge κ (assemble x y v) (Fin.last m) = r324OutgoingEndpointKernel (r324OutgoingAnchor hm v) (r324OutgoingShortcutAnchor κ v) (r324OutgoingIsShortcut κ) y

theorem Anderson4D.renormalizedGreenSkeleton_eq_endpointKernels_mul_core {m : ℕ} (hm : 0 < m) (κ : PartialPairing (Fin m)) (x y : T4) (v : Fin m → T4) : renormalizedGreenSkeleton κ (assemble x y v) = r324IncomingEndpointKernel (r324IncomingAnchor hm v) (r324IncomingAnchor hm v) false x * r324OutgoingEndpointKernel (r324OutgoingAnchor hm v) (r324OutgoingShortcutAnchor κ v) (r324OutgoingIsShortcut κ) y * r324RenormalizedInteriorCore κ v

Exact product decomposition of a renormalized profile into its two external legs and an endpoint-independent internal core.

A whole refined fibre as one endpoint-separated integrand

noncomputable def Anderson4D.r324ContractionEndpointAnchors {m : ℕ} (hm : 0 < m) (e : MomentContraction m) (v : Fin (2 * m) → T4) : R324EndpointAnchors

The four concrete pairs of endpoint anchors attached to a contraction representative, in (x,y,z,w) order.

Equations

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

def Anderson4D.r324ContractionEndpointFlags {m : ℕ} (e : MomentContraction m) : R324EndpointFlags

Only the outgoing endpoint of either copy can be replaced by an extracted difference.

Equations

• Anderson4D.r324ContractionEndpointFlags e = ![false, Anderson4D.r324OutgoingIsShortcut e.fst, false, Anderson4D.r324OutgoingIsShortcut e.snd.fst]

@[simp]

theorem Anderson4D.r324ContractionEndpointAnchors_zero {m : ℕ} (hm : 0 < m) (e : MomentContraction m) (v : Fin (2 * m) → T4) : r324ContractionEndpointAnchors hm e v 0 = (r324IncomingAnchor hm fun (i : Fin m) => v (leftMomentIndex i), r324IncomingAnchor hm fun (i : Fin m) => v (leftMomentIndex i))

@[simp]

theorem Anderson4D.r324ContractionEndpointAnchors_one {m : ℕ} (hm : 0 < m) (e : MomentContraction m) (v : Fin (2 * m) → T4) : r324ContractionEndpointAnchors hm e v 1 = (r324OutgoingAnchor hm fun (i : Fin m) => v (leftMomentIndex i), r324OutgoingShortcutAnchor e.fst fun (i : Fin m) => v (leftMomentIndex i))

@[simp]

theorem Anderson4D.r324ContractionEndpointAnchors_two {m : ℕ} (hm : 0 < m) (e : MomentContraction m) (v : Fin (2 * m) → T4) : r324ContractionEndpointAnchors hm e v 2 = (r324IncomingAnchor hm fun (i : Fin m) => v (rightMomentIndex i), r324IncomingAnchor hm fun (i : Fin m) => v (rightMomentIndex i))

@[simp]

theorem Anderson4D.r324ContractionEndpointAnchors_three {m : ℕ} (hm : 0 < m) (e : MomentContraction m) (v : Fin (2 * m) → T4) : r324ContractionEndpointAnchors hm e v 3 = (r324OutgoingAnchor hm fun (i : Fin m) => v (rightMomentIndex i), r324OutgoingShortcutAnchor e.snd.fst fun (i : Fin m) => v (rightMomentIndex i))

@[simp]

theorem Anderson4D.r324ContractionEndpointFlags_zero {m : ℕ} (e : MomentContraction m) : r324ContractionEndpointFlags e 0 = false

@[simp]

theorem Anderson4D.r324ContractionEndpointFlags_one {m : ℕ} (e : MomentContraction m) : r324ContractionEndpointFlags e 1 = r324OutgoingIsShortcut e.fst

@[simp]

theorem Anderson4D.r324ContractionEndpointFlags_two {m : ℕ} (e : MomentContraction m) : r324ContractionEndpointFlags e 2 = false

@[simp]

theorem Anderson4D.r324ContractionEndpointFlags_three {m : ℕ} (e : MomentContraction m) : r324ContractionEndpointFlags e 3 = r324OutgoingIsShortcut e.snd.fst

noncomputable def Anderson4D.r324RefinedEndpointCore (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (e₀ : MomentContraction m) (v : Fin (2 * m) → T4) : ℂ

Internal core of one refined fibre. Crucially, the complete primitive-pairing fibre sum remains inside this core.

Equations

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

theorem Anderson4D.momentRefinedPhysicalIntegrand_eq_endpointSeparated (ρ : SmoothCutoff) (ε : ℝ) (m : ℕ) (hm : 0 < m) (α β : Z4) (s r : Finset (Fin (2 * m)) × Finset (Fin (2 * m))) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentContractionFiber m s) (x y z w : T4) (v : Fin (2 * m) → T4) : momentRefinedPhysicalIntegrand ρ ε m α β s r x y z w v = r324EndpointSeparatedIntegrand α β (r324ContractionEndpointAnchors hm e₀ v) (r324ContractionEndpointFlags e₀) (r324RefinedEndpointCore ρ ε m s r e₀ v) x y z w

Exact endpoint-separated form of an entire residual-refined physical fibre. The finite primitive-pairing sum is formed before any endpoint Fourier integration or norm.