The actual first proper-block collapse for R-322

This file starts from the existing grouped kernel endpointFiberDetJSum, not from a parallel model integrand. The first checkpoint exposes the spatial coordinates of the first selected extraction block on the inside of the actual endpoint-fibre integral.

Internal coordinates belonging to an ambient extraction block

def Anderson4D.r322InternalCoordinatesOfBlock (q : ℕ) (hq : 1 ≤ q) (B : Finset (Fin (2 * q))) : Finset (Fin (2 * q - 2))

Internal detJ coordinates whose assembled ambient vertices lie in B. For a proper block, every vertex of B occurs in this finset.

Equations

• Anderson4D.r322InternalCoordinatesOfBlock q hq B = {i : Fin (2 * q - 2) | Anderson4D.primitiveInternalIdx q hq i ∈ B}

@[simp]

theorem Anderson4D.mem_r322InternalCoordinatesOfBlock (q : ℕ) (hq : 1 ≤ q) (B : Finset (Fin (2 * q))) (i : Fin (2 * q - 2)) : i ∈ r322InternalCoordinatesOfBlock q hq B ↔ primitiveInternalIdx q hq i ∈ B

The grouped kernel as one actual endpoint-fibre integral

theorem Anderson4D.endpointFiberDetJSum_eq_integral_sum_detJintegrand (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (z : T4) (hint : ∀ (τ : ReductionEndpointFiberAt κ), MeasureTheory.Integrable (fun (v : Fin (2 * q - 2) → T4) => detJintegrand ρ ε q (↑τ) (primitiveAssemble q hq z 0 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * q - 2)) => paperMeasure)) : endpointFiberDetJSum ρ lam ε q (reductionEndpointSignature κ) z = lamEps lam ε ^ (2 * q) * ∫ (v : Fin (2 * q - 2) → T4), ∑ τ : ReductionEndpointFiberAt κ, detJintegrand ρ ε q (↑τ) (primitiveAssemble q hq z 0 v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * q - 2)) => paperMeasure

Move the complete endpoint-fibre sum inside the existing detJ integral. The premise is exactly the section integrability needed for finite-sum linearity; no estimate or absolute value is used.

Actual selected-coordinate Fubini form

theorem Anderson4D.endpointFiberDetJSum_eq_firstBlockSpatialFubini (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (h : ∃ (a : Fin (2 * q)) (b : Fin (2 * q)), IsRelFullyPaired κ Finset.univ a b) (z : T4) (hint : ∀ (τ : ReductionEndpointFiberAt κ), MeasureTheory.Integrable (fun (v : Fin (2 * q - 2) → T4) => detJintegrand ρ ε q (↑τ) (primitiveAssemble q hq z 0 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * q - 2)) => paperMeasure)) : endpointFiberDetJSum ρ lam ε q (reductionEndpointSignature κ) z = lamEps lam ε ^ (2 * q) * ∫ (vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq (selectedExtractionBlock κ Finset.univ h)) i } → T4), ∫ (vB : { i : Fin (2 * q - 2) // r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq (selectedExtractionBlock κ Finset.univ h)) i } → T4), ∑ τ : ReductionEndpointFiberAt κ, detJintegrand ρ ε q (↑τ) (primitiveAssemble q hq z 0 (r322MergeSelectedFinCoordinates (r322InternalCoordinatesOfBlock q hq (selectedExtractionBlock κ Finset.univ h)) vB vC)) ∂MeasureTheory.Measure.pi fun (x : { i : Fin (2 * q - 2) // r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq (selectedExtractionBlock κ Finset.univ h)) i }) => paperMeasure ∂MeasureTheory.Measure.pi fun (x : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq (selectedExtractionBlock κ Finset.univ h)) i }) => paperMeasure

Exact first-block Fubini form of the actual grouped kernel.

The selected block coordinates are integrated on the inside. The complementary spatial tuple remains the outer parameter, ready for the pairing-complement sum and the replacement-edge identity.

Minimal actual proper-block phase: the nested order-four fibre

def Anderson4D.pairingFinFourNested : PartialPairing (Fin 4)

The order-four nested pairing (0, 3)(1, 2). Its first extracted block is the strict internal interval {1, 2}, while (0, 3) is the terminal residual pair.

Equations

• Anderson4D.pairingFinFourNested = { toFun := Fin.rev, involutive := Anderson4D.pairingFinFourNested._proof_1 }

@[simp]

theorem Anderson4D.pairingFinFourNested_extract : extract pairingFinFourNested = [(1, 2), (0, 3)]

theorem Anderson4D.pairingFinFourNested_mem_nonSplit : pairingFinFourNested ∈ nonSplitPairings 2

theorem Anderson4D.pairingFinFourNested_endpointFiber : {τ ∈ nonSplitPairings 2 | reductionEndpointSignature τ = reductionEndpointSignature pairingFinFourNested} = {pairingFinFourNested}

The realized endpoint fibre of the nested pairing contains exactly that pairing. The crossing pairing has a different extraction endpoint signature.

theorem Anderson4D.pairingFinFourNested_lowerSupport : {i ∈ pairingFinFourNested.pairSupport | i < pairingFinFourNested i} = {0, 1}

The covariance representatives of the nested pairing are 0 and 1, so its two covariance edges are (0, 3) and (1, 2).

theorem Anderson4D.pairingFinFourNested_firstBlock_proper : {1, 2} ≠ Finset.univ

The first block in the extraction list is genuinely proper. The whole interval (0, 3) is retained as the distinct terminal phase.

theorem Anderson4D.detJintegrand_two_pairingFinFourNested (ρ : SmoothCutoff) (ε : ℝ) (x : Fin 4 → T4) : detJintegrand ρ ε 2 pairingFinFourNested x = greenFn (x 0 - x 1) * greenFn (x 1 - x 2) * (greenFn (x 2 - x 3) - greenFn (x 1 - x 3)) * (ρ.etaEpsT4 ε (x 0 - x 3) * ρ.etaEpsT4 ε (x 1 - x 2))

Closed form of the existing detJintegrand on the nested order-four pairing. In particular, the inner (1, 2) factors occur as one complete order-one primitive block.

theorem Anderson4D.endpointFiberDetJSum_nested_two_eq_detJ (ρ : SmoothCutoff) (lam ε : ℝ) (z : T4) : endpointFiberDetJSum ρ lam ε 2 (reductionEndpointSignature pairingFinFourNested) z = detJ ρ lam ε 2 pairingFinFourNested z 0

At the nested endpoint signature the existing grouped sum is a singleton, so no hidden multiplicity remains before the analytic collapse.

theorem Anderson4D.detJintegrand_two_pairingFinFourNested_assembled (ρ : SmoothCutoff) (ε : ℝ) (z : T4) (v : Fin 2 → T4) : detJintegrand ρ ε 2 pairingFinFourNested (primitiveAssemble 2 ⋯ z 0 v) = greenFn (z - v 0) * greenFn (v 0 - v 1) * (greenFn (v 1) - greenFn (v 0)) * (ρ.etaEpsT4 ε z * ρ.etaEpsT4 ε (v 0 - v 1))

The assembled actual order-four integrand, with the proper block coordinates displayed as the two entries of v.

theorem Anderson4D.detJ_two_pairingFinFourNested_eq_prodIntegral (ρ : SmoothCutoff) (lam ε : ℝ) (z : T4) : detJ ρ lam ε 2 pairingFinFourNested z 0 = lamEps lam ε ^ 4 * ∫ (p : T4 × T4), greenFn (z - p.1) * greenFn (p.1 - p.2) * (greenFn p.2 - greenFn p.1) * (ρ.etaEpsT4 ε z * ρ.etaEpsT4 ε (p.1 - p.2)) ∂paperMeasure.prod paperMeasure

Product-measure form of the actual nested detJ. This is only a change of variables from Fin 2 → T4 to T4 × T4; the displayed integrand was proved above by unfolding the project's detJintegrand.

theorem Anderson4D.detJ_two_pairingFinFourNested_eq_firstProperBlockCollapse (ρ : SmoothCutoff) (lam ε : ℝ) (z : T4) : detJ ρ lam ε 2 pairingFinFourNested z 0 = lamEps lam ε ^ 2 * ρ.etaEpsT4 ε z * r322Collapse greenFn (primitiveKernelDiff ρ lam ε 1 ⋯ fun (x : Fin (2 * 1 - 1)) => greenFn) greenFn z

The actual nested order-four kernel is the first genuine proper-block collapse. The factor outside the collapse is precisely the covariance and coupling carried by the terminal residual pair (0, 3).

theorem Anderson4D.endpointFiberDetJSum_nested_two_eq_firstProperBlockReplacement (ρ : SmoothCutoff) (lam ε : ℝ) (z : T4) : endpointFiberDetJSum ρ lam ε 2 (reductionEndpointSignature pairingFinFourNested) z = lamEps lam ε ^ 2 * ρ.etaEpsT4 ε z * r322ReplaceEdge (fun (x : Fin 1) => greenFn) 0 greenFn (primitiveKernelDiff ρ lam ε 1 ⋯ fun (x : Fin (2 * 1 - 1)) => greenFn) greenFn 0 z

Actual first proper-block replacement, minimal nonterminal case.

The left side is the project's existing endpoint-fibre sum. The right side updates one named edge by the complete signed primitive sum over the strict first block {1, 2}. The invocation of selectedPrimitiveInnerIntegral_eq_replacementEdge below is the precise bridge from the selected-coordinate integral to the replacement edge.

Terminal phase kept separate

theorem Anderson4D.endpointFiberDetJSum_terminal_one_eq_primitiveKernelDiff (ρ : SmoothCutoff) (lam ε : ℝ) (z : T4) : endpointFiberDetJSum ρ lam ε 1 (reductionEndpointSignature pairingFinTwo) z = primitiveKernelDiff ρ lam ε 1 ⋯ (fun (x : Fin (2 * 1 - 1)) => greenFn) z

The whole order-two interval is terminal: it is identified directly with the complete primitive kernel and is not represented as a proper-block collapse.