The actual proper-head collapse for R-322

This module connects the first proper step of the paper-order analytic schedule to the existing endpointFiberDetJSum. The first structural issue is essential: the standard primitive kernel can be read from the touching ambient chain only after proving that the first analytic block has no holes. That fact is derived below from the actual selector recursion, rather than assumed as a parallel interface.

A missing interval point was removed at an earlier selector step

def Anderson4D.r322ExtractionTraceAux {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : List (R322ExtractionStep m)

Endpoint/block steps before sorting into paper order.

Equations

• Anderson4D.r322ExtractionTraceAux κ fuel active = (Anderson4D.extractAux κ fuel active).zip (Anderson4D.extractionBlocksAux κ fuel active)

theorem Anderson4D.exists_previous_extractionStep_of_mem_Icc_not_mem {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) (i : Fin m) (hiActive : i ∈ active) (s : R322ExtractionStep m) (hs : s ∈ r322ExtractionTraceAux κ fuel active) (hiIcc : i ∈ Finset.Icc s.1.1 s.1.2) (hiBlock : i ∉ s.2) : ∃ (pre : List (R322ExtractionStep m)) (post : List (R322ExtractionStep m)), r322ExtractionTraceAux κ fuel active = pre ++ s :: post ∧ ∃ earlier ∈ pre, i ∈ earlier.2

If a point starts active, lies between the endpoints of a later selector step, but is absent from that step's concrete trace, then it lies in the concrete block of a strictly earlier selector step.

The first analytic block has no holes

theorem Anderson4D.r322ExtractionTraceAux_pairwise_earlierCompatible {m : ℕ} (κ : PartialPairing (Fin m)) (fuel : ℕ) (active : Finset (Fin m)) : List.Pairwise (fun (s t : R322ExtractionStep m) => EarlierReductionIntervalCompatible s.1 t.1) (r322ExtractionTraceAux κ fuel active)

The unsorted paired extraction trace inherits the directional endpoint geometry of the selector recursion.

theorem Anderson4D.r322AnalyticSchedule_head_block_eq_Icc {m : ℕ} (κ : PartialPairing (Fin m)) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hschedule : r322AnalyticSchedule κ = head :: tail) : head.2 = Finset.Icc head.1.1 head.1.2

The head of the right-endpoint-sorted schedule is a genuine ambient interval. Any hole would have been removed by an earlier selector block strictly nested inside it, hence would have a smaller right endpoint and would have sorted before the alleged head.

Proper-head coordinates are precisely internal coordinates

theorem Anderson4D.r322AnalyticProperHead_endpoint_bounds {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : 0 < ↑head.1.1 ∧ ↑head.1.2 < 2 * q - 1

A proper head of a non-splitting schedule meets neither global endpoint.

theorem Anderson4D.r322AnalyticProperHead_block_vertex_bounds {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (i : Fin (2 * q)) (hi : i ∈ head.2) : 0 < ↑i ∧ ↑i < 2 * q - 1

Every vertex of a proper analytic head block is one of the internal coordinates of the ambient detJ.

noncomputable def Anderson4D.r322AnalyticProperHeadInternalCoordinateEquiv {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : { i : Fin (2 * q - 2) // r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } ≃ ↥head.2

Internal ambient coordinates selected by the proper head are equivalent to the concrete head block itself.

Equations

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

noncomputable def Anderson4D.r322AnalyticProperHeadSelectedCoordinateEquiv {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : Fin (2 * residualBlockOrder head.2) ≃ { i : Fin (2 * q - 2) // r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i }

Increasing standard block coordinates are exactly the selected internal ambient coordinates of a proper analytic head.

Equations

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

@[simp]

theorem Anderson4D.r322AnalyticProperHeadSelectedCoordinateEquiv_apply_ambient {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (j : Fin (2 * residualBlockOrder head.2)) : primitiveInternalIdx q hq ↑((r322AnalyticProperHeadSelectedCoordinateEquiv hq κ hκ head tail hschedule hproper) j) = ↑((residualPrimitiveBlockOrderIso κ head.2 ⋯) j)

theorem Anderson4D.r322AnalyticProperHead_endpoint_span {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (_hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (_hproper : head.1 ≠ r322WholeEndpoint q hq) : ↑head.1.2 + 1 - ↑head.1.1 = 2 * residualBlockOrder head.2

The endpoint span of the proper analytic head is exactly twice its residual perturbative order.

theorem Anderson4D.r322AnalyticProperHead_residualOrderIso_apply_val {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (j : Fin (2 * residualBlockOrder head.2)) : ↑↑((residualPrimitiveBlockOrderIso κ head.2 ⋯) j) = ↑head.1.1 + ↑j

The canonical increasing enumeration of the first analytic block is the literal affine interval enumeration a + j.

The exact local chain interval

theorem Anderson4D.r322AnalyticProperHead_activeLocalEdge_iff {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (e : Fin (2 * q - 1)) : ¬R322ChainEdgeOutside head.2 e ∧ ↑e ∉ List.map (fun (s : R322ExtractionStep (2 * q)) => ↑s.1.2) (r322AnalyticSchedule κ) ↔ ↑head.1.1 - 1 ≤ ↑e ∧ ↑e < ↑head.1.2

An ambient chain edge survives in the touching local product of a proper analytic head exactly when its left index lies in [a - 1, b). In particular the incoming edge is a - 1, while the scheduled right edge b is already removed.

theorem Anderson4D.r322AnalyticHead_one_le_residualBlockOrder {q : ℕ} (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) : 1 ≤ residualBlockOrder head.2

Every displayed analytic head carries a positive primitive order.

def Anderson4D.r322AnalyticProperHeadVertex {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (j : Fin (2 * residualBlockOrder head.2)) : Fin (2 * q)

The ambient vertex occupied by standard head-block coordinate j.

Equations

• Anderson4D.r322AnalyticProperHeadVertex hq κ hκ head tail hschedule hproper j = ⟨↑head.1.1 + ↑j, ⋯⟩

@[simp]

theorem Anderson4D.r322AnalyticProperHeadVertex_val {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (j : Fin (2 * residualBlockOrder head.2)) : ↑(r322AnalyticProperHeadVertex hq κ hκ head tail hschedule hproper j) = ↑head.1.1 + ↑j

theorem Anderson4D.r322AnalyticProperHead_residualOrderIso_apply {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (j : Fin (2 * residualBlockOrder head.2)) : ↑((residualPrimitiveBlockOrderIso κ head.2 ⋯) j) = r322AnalyticProperHeadVertex hq κ hκ head tail hschedule hproper j

The affine vertex is the existing canonical residual-block enumeration, not a parallel coordinate convention.

def Anderson4D.r322AnalyticProperHeadStandardTuple {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) : Fin (2 * residualBlockOrder head.2) → T4

The standard head tuple, read in increasing ambient order.

Equations

• Anderson4D.r322AnalyticProperHeadStandardTuple hq κ hκ head tail hschedule hproper x j = x (Anderson4D.r322AnalyticProperHeadVertex hq κ hκ head tail hschedule hproper j)

def Anderson4D.r322AnalyticProperHeadPredecessorEdge {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : Fin (2 * q - 1)

The incoming chain slot immediately preceding a proper head.

Equations

• Anderson4D.r322AnalyticProperHeadPredecessorEdge hq κ hκ head tail hschedule hproper = ⟨↑head.1.1 - 1, ⋯⟩

@[simp]

theorem Anderson4D.r322AnalyticProperHeadPredecessorEdge_val {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : ↑(r322AnalyticProperHeadPredecessorEdge hq κ hκ head tail hschedule hproper) = ↑head.1.1 - 1

def Anderson4D.r322AnalyticProperHeadInternalEdge {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (j : Fin (2 * residualBlockOrder head.2 - 1)) : Fin (2 * q - 1)

Ambient chain slot of the jth internal edge of the proper head.

Equations

• Anderson4D.r322AnalyticProperHeadInternalEdge hq κ hκ head tail hschedule hproper j = ⟨↑head.1.1 + ↑j, ⋯⟩

@[simp]

theorem Anderson4D.r322AnalyticProperHeadInternalEdge_val {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (j : Fin (2 * residualBlockOrder head.2 - 1)) : ↑(r322AnalyticProperHeadInternalEdge hq κ hκ head tail hschedule hproper j) = ↑head.1.1 + ↑j

theorem Anderson4D.r322AnalyticProperHeadLocalChainProductWith_eq {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (G : Fin (2 * q - 1) → T4 → ℝ) (x : Fin (2 * q) → T4) : r322AnalyticHeadLocalChainProductWith G κ head x = jChainEdgeWith G x (r322AnalyticProperHeadPredecessorEdge hq κ hκ head tail hschedule hproper) * primitiveChainProduct (residualBlockOrder head.2) ⋯ (fun (j : Fin (2 * residualBlockOrder head.2 - 1)) => G (r322AnalyticProperHeadInternalEdge hq κ hκ head tail hschedule hproper j)) (r322AnalyticProperHeadStandardTuple hq κ hκ head tail hschedule hproper x)

The touching analytic chain at a proper head is exactly its incoming predecessor edge followed by the standard primitive chain on the head tuple. This is the structural recognition needed before detJWith can be used; it is false for a sparse block with holes.

Recognition of the head covariance coordinate

theorem Anderson4D.r322AnalyticHeadPrimitiveSum_eq_standardTuple {q : ℕ} (hq : 1 ≤ q) (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (x : Fin (2 * q) → T4) : r322ExtractionBlockPrimitiveSum ρ ε κ (r322AnalyticHeadBlockIndex κ hschedule) x = ∑ σ : ↥(primitiveFullPairings (residualBlockOrder head.2)), primitiveCovarianceProduct ρ ε (residualBlockOrder head.2) (↑σ) (r322AnalyticProperHeadStandardTuple hq κ hκ head tail hschedule hproper x)

The actual primitive covariance sum assigned to the analytic head is the standard complete primitive sum evaluated on the standard head tuple.

Exact standard-block proper collapse

theorem Anderson4D.lamEps_pow_integral_standardCompletePrimitive_eq_replacementEdge {ι : Type u_1} [DecidableEq ι] (edges : ι → T4 → ℝ) (slot : ι) (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (Gp Gr : T4 → ℝ) (u : T4) (hstandard : MeasureTheory.Integrable (fun (t : Fin (2 * n) → T4) => (Gp (u - t ⟨0, ⋯⟩) * ∑ κB : ↥(primitiveFullPairings n), detJclosedIntegrandWith ρ ε (2 * n) (↑κB) G t) * (Gr (t (primitiveLast n hn)) - Gr (t ⟨0, ⋯⟩))) (MeasureTheory.Measure.pi fun (x : Fin (2 * n)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings n)), MeasureTheory.Integrable (fun (v : Fin (2 * n - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * n) (↑κB) G (primitiveAssemble n hn p.1 p.2 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure)) : (lamEps lam ε ^ (2 * n) * ∫ (t : Fin (2 * n) → T4), (Gp (u - t ⟨0, ⋯⟩) * ∑ κB : ↥(primitiveFullPairings n), detJclosedIntegrandWith ρ ε (2 * n) (↑κB) G t) * (Gr (t (primitiveLast n hn)) - Gr (t ⟨0, ⋯⟩)) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n)) => paperMeasure) = r322ReplaceEdge edges slot Gp (primitiveKernelDiff ρ lam ε n hn G) Gr slot u

A complete standard primitive block, with an incoming endpoint kernel and the signed outgoing endpoint difference, integrates exactly to the named predecessor-edge replacement. Integrability of the internal primitive section is required only for product-Haar almost every endpoint pair, which is precisely what joint integrability and Fubini provide.

The actual selected-coordinate reconstruction

noncomputable def Anderson4D.r322AnalyticProperHeadSelectedTuple {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (t : Fin (2 * residualBlockOrder head.2) → T4) : { i : Fin (2 * q - 2) // r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4

Plain-function form of the selected-coordinate reindex.

Equations

• Anderson4D.r322AnalyticProperHeadSelectedTuple hq κ hκ head tail hschedule hproper t i = t ((Anderson4D.r322AnalyticProperHeadSelectedCoordinateEquiv hq κ hκ head tail hschedule hproper).symm i)

@[simp]

theorem Anderson4D.r322AnalyticProperHeadSelectedTuple_apply {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (t : Fin (2 * residualBlockOrder head.2) → T4) (j : Fin (2 * residualBlockOrder head.2)) : r322AnalyticProperHeadSelectedTuple hq κ hκ head tail hschedule hproper t ((r322AnalyticProperHeadSelectedCoordinateEquiv hq κ hκ head tail hschedule hproper) j) = t j

noncomputable def Anderson4D.r322AnalyticProperHeadReconstruct {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (z : T4) (vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4) (t : Fin (2 * residualBlockOrder head.2) → T4) : Fin (2 * q) → T4

Reconstruct the ambient detJ tuple from a standard proper-head tuple and the fixed complementary internal coordinates.

Equations

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

theorem Anderson4D.r322AnalyticProperHeadStandardTuple_reconstruct {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (z : T4) (vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4) (t : Fin (2 * residualBlockOrder head.2) → T4) : r322AnalyticProperHeadStandardTuple hq κ hκ head tail hschedule hproper (r322AnalyticProperHeadReconstruct hq κ hκ head tail hschedule hproper z vC t) = t

Reading the reconstructed ambient tuple on the head interval returns the supplied standard head tuple literally.

theorem Anderson4D.r322AnalyticProperHeadReconstruct_eq_of_not_mem {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (z : T4) (vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4) (s t : Fin (2 * residualBlockOrder head.2) → T4) (i : Fin (2 * q)) (hi : i ∉ head.2) : r322AnalyticProperHeadReconstruct hq κ hκ head tail hschedule hproper z vC s i = r322AnalyticProperHeadReconstruct hq κ hκ head tail hschedule hproper z vC t i

Changing the standard head tuple leaves every ambient coordinate outside the concrete head block unchanged.

Proper-head endpoint geometry in reconstructed coordinates

theorem Anderson4D.r322AnalyticProperHeadVertex_zero {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : r322AnalyticProperHeadVertex hq κ hκ head tail hschedule hproper ⟨0, ⋯⟩ = head.1.1

The first standard head vertex is the selected left endpoint.

theorem Anderson4D.r322AnalyticProperHeadVertex_last {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : r322AnalyticProperHeadVertex hq κ hκ head tail hschedule hproper (primitiveLast (residualBlockOrder head.2) ⋯) = head.1.2

The last standard head vertex is the selected right endpoint.

def Anderson4D.r322AnalyticProperHeadSuccessorVertex {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : Fin (2 * q)

Ambient vertex immediately to the right of a proper head.

Equations

• Anderson4D.r322AnalyticProperHeadSuccessorVertex hq κ hκ head tail hschedule hproper = ⟨↑head.1.2 + 1, ⋯⟩

theorem Anderson4D.r322AnalyticProperHeadPredecessorEdge_right {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : r322JChainEdgeRight (r322AnalyticProperHeadPredecessorEdge hq κ hκ head tail hschedule hproper) = head.1.1

The predecessor edge enters the head at its left endpoint.

theorem Anderson4D.r322AnalyticProperHeadPredecessorVertex_not_mem {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : r322JChainEdgeLeft (r322AnalyticProperHeadPredecessorEdge hq κ hκ head tail hschedule hproper) ∉ head.2

The predecessor coordinate is outside the head block.

theorem Anderson4D.r322AnalyticProperHeadSuccessorVertex_not_mem {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : r322AnalyticProperHeadSuccessorVertex hq κ hκ head tail hschedule hproper ∉ head.2

The successor coordinate is outside the head block.

noncomputable def Anderson4D.r322AnalyticProperHeadReferenceTuple {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (z : T4) (vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4) : Fin (2 * q) → T4

Fixed complementary reference tuple used to name the predecessor and successor values during the head integration.

Equations

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

noncomputable def Anderson4D.r322AnalyticProperHeadPredecessorPoint {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (z : T4) (vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4) : T4

Fixed predecessor coordinate feeding the proper head.

Equations

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

noncomputable def Anderson4D.r322AnalyticProperHeadSuccessorPoint {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (z : T4) (vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4) : T4

Fixed successor coordinate used by the signed outgoing difference.

Equations

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

noncomputable def Anderson4D.r322AnalyticProperHeadOutgoingKernel {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (z : T4) (vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4) : T4 → ℝ

Outgoing endpoint kernel with the fixed successor coordinate inserted.

Equations

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

theorem Anderson4D.r322AnalyticHeadLocalIntegrandFactor_reconstruct_eq_standard {q : ℕ} (hq : 1 ≤ q) (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (z : T4) (vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4) (t : Fin (2 * residualBlockOrder head.2) → T4) : r322AnalyticHeadLocalIntegrandFactor ρ ε κ head tail hschedule (r322AnalyticProperHeadReconstruct hq κ hκ head tail hschedule hproper z vC t) = (greenFn (r322AnalyticProperHeadPredecessorPoint hq κ hκ head tail hschedule hproper z vC - t ⟨0, ⋯⟩) * ∑ κB : ↥(primitiveFullPairings (residualBlockOrder head.2)), detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (fun (x : Fin (2 * residualBlockOrder head.2 - 1)) => greenFn) t) * (r322AnalyticProperHeadOutgoingKernel hq κ hκ head tail hschedule hproper z vC (t (primitiveLast (residualBlockOrder head.2) ⋯)) - r322AnalyticProperHeadOutgoingKernel hq κ hκ head tail hschedule hproper z vC (t ⟨0, ⋯⟩))

The actual local endpoint-fibre factor on reconstructed selected coordinates is the complete standard primitive-collapse integrand.

Measure-preserving selected-tuple reindex

noncomputable def Anderson4D.r322AnalyticProperHeadSelectedTupleMeasurableEquiv {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : (Fin (2 * residualBlockOrder head.2) → T4) ≃ᵐ ({ i : Fin (2 * q - 2) // r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4)

Reindex the selected ambient internal coordinates by the increasing standard coordinates of the head block.

Equations

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

@[simp]

theorem Anderson4D.r322AnalyticProperHeadSelectedTupleMeasurableEquiv_apply {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (u : Fin (2 * residualBlockOrder head.2) → T4) (j : Fin (2 * residualBlockOrder head.2)) : (r322AnalyticProperHeadSelectedTupleMeasurableEquiv hq κ hκ head tail hschedule hproper) u ((r322AnalyticProperHeadSelectedCoordinateEquiv hq κ hκ head tail hschedule hproper) j) = u j

theorem Anderson4D.measurePreserving_r322AnalyticProperHeadSelectedTupleMeasurableEquiv {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) : MeasureTheory.MeasurePreserving (⇑(r322AnalyticProperHeadSelectedTupleMeasurableEquiv hq κ hκ head tail hschedule hproper)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure) (MeasureTheory.Measure.pi fun (x : { i : Fin (2 * q - 2) // r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i }) => paperMeasure)

The selected-tuple reindex preserves the exact paper product measure.

theorem Anderson4D.integral_r322AnalyticProperHeadSelected_eq_standardBlock {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f : ({ i : Fin (2 * q - 2) // r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4) → E) : (∫ (vB : { i : Fin (2 * q - 2) // r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4), f vB ∂MeasureTheory.Measure.pi fun (x : { i : Fin (2 * q - 2) // r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i }) => paperMeasure) = ∫ (u : Fin (2 * residualBlockOrder head.2) → T4), f ((r322AnalyticProperHeadSelectedTupleMeasurableEquiv hq κ hκ head tail hschedule hproper) u) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure

Exact Bochner integral reindex from the selected ambient tuple to the standard increasing head-block tuple.

Actual proper-head integral collapse

theorem Anderson4D.r322AnalyticProperHeadSelectedTupleMeasurableEquiv_eq_plain {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (t : Fin (2 * residualBlockOrder head.2) → T4) : (r322AnalyticProperHeadSelectedTupleMeasurableEquiv hq κ hκ head tail hschedule hproper) t = r322AnalyticProperHeadSelectedTuple hq κ hκ head tail hschedule hproper t

The measurable selected-tuple reindex has the same underlying function as the explicit reconstruction reindex used above.

noncomputable def Anderson4D.r322AnalyticProperHeadStandardClosedIntegrand {q : ℕ} (hq : 1 ≤ q) (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (z : T4) (vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4) (t : Fin (2 * residualBlockOrder head.2) → T4) : ℝ

Standard closed-integrand form of the actual proper head.

Equations

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

theorem Anderson4D.r322AnalyticHeadLocalIntegrandFactor_reconstruct_eq_closed {q : ℕ} (hq : 1 ≤ q) (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (z : T4) (vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4) (t : Fin (2 * residualBlockOrder head.2) → T4) : r322AnalyticHeadLocalIntegrandFactor ρ ε κ head tail hschedule (r322AnalyticProperHeadReconstruct hq κ hκ head tail hschedule hproper z vC t) = r322AnalyticProperHeadStandardClosedIntegrand hq ρ ε κ hκ head tail hschedule hproper z vC t

Pointwise recognition packaged only as a definitional abbreviation.

theorem Anderson4D.lamEps_pow_integral_r322AnalyticProperHeadLocal_eq_replacementEdge {q : ℕ} (hq : 1 ≤ q) (ρ : SmoothCutoff) (lam ε : ℝ) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (z : T4) (vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4) (hstandard : MeasureTheory.Integrable (r322AnalyticProperHeadStandardClosedIntegrand hq ρ ε κ hκ head tail hschedule hproper z vC) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (fun (x : Fin (2 * residualBlockOrder head.2 - 1)) => greenFn) (primitiveAssemble (residualBlockOrder head.2) ⋯ p.1 p.2 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) : (lamEps lam ε ^ (2 * residualBlockOrder head.2) * ∫ (t : Fin (2 * residualBlockOrder head.2) → T4), r322AnalyticHeadLocalIntegrandFactor ρ ε κ head tail hschedule (r322AnalyticProperHeadReconstruct hq κ hκ head tail hschedule hproper z vC t) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure) = r322ReplaceEdge (fun (x : Fin (2 * q - 1)) => greenFn) (r322AnalyticProperHeadPredecessorEdge hq κ hκ head tail hschedule hproper) greenFn (primitiveKernelDiff ρ lam ε (residualBlockOrder head.2) ⋯ fun (x : Fin (2 * residualBlockOrder head.2 - 1)) => greenFn) (r322AnalyticProperHeadOutgoingKernel hq κ hκ head tail hschedule hproper z vC) (r322AnalyticProperHeadPredecessorEdge hq κ hκ head tail hschedule hproper) (r322AnalyticProperHeadPredecessorPoint hq κ hκ head tail hschedule hproper z vC)

Integrating the actual local proper-head factor writes the collapsed kernel into the predecessor slot a - 1.

theorem Anderson4D.lamEps_pow_integral_r322AnalyticProperHeadSelected_eq_replacementEdge {q : ℕ} (hq : 1 ≤ q) (ρ : SmoothCutoff) (lam ε : ℝ) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (z : T4) (vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4) (hstandard : MeasureTheory.Integrable (r322AnalyticProperHeadStandardClosedIntegrand hq ρ ε κ hκ head tail hschedule hproper z vC) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (fun (x : Fin (2 * residualBlockOrder head.2 - 1)) => greenFn) (primitiveAssemble (residualBlockOrder head.2) ⋯ p.1 p.2 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) : (lamEps lam ε ^ (2 * residualBlockOrder head.2) * ∫ (vB : { i : Fin (2 * q - 2) // r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4), r322AnalyticHeadLocalIntegrandFactor ρ ε κ head tail hschedule (primitiveAssemble q hq z 0 (r322MergeSelectedFinCoordinates (r322InternalCoordinatesOfBlock q hq head.2) vB vC)) ∂MeasureTheory.Measure.pi fun (x : { i : Fin (2 * q - 2) // r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i }) => paperMeasure) = r322ReplaceEdge (fun (x : Fin (2 * q - 1)) => greenFn) (r322AnalyticProperHeadPredecessorEdge hq κ hκ head tail hschedule hproper) greenFn (primitiveKernelDiff ρ lam ε (residualBlockOrder head.2) ⋯ fun (x : Fin (2 * residualBlockOrder head.2 - 1)) => greenFn) (r322AnalyticProperHeadOutgoingKernel hq κ hκ head tail hschedule hproper z vC) (r322AnalyticProperHeadPredecessorEdge hq κ hκ head tail hschedule hproper) (r322AnalyticProperHeadPredecessorPoint hq κ hκ head tail hschedule hproper z vC)

Selected-coordinate form consumed directly by the spatial Fubini identity for endpointFiberDetJSum.

theorem Anderson4D.lamEps_pow_integral_sum_endpointFiber_detJintegrand_properHead_eq {q : ℕ} (hq : 1 ≤ q) (ρ : SmoothCutoff) (lam ε : ℝ) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (z : T4) (vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4) (hstandard : MeasureTheory.Integrable (r322AnalyticProperHeadStandardClosedIntegrand hq ρ ε κ hκ head tail hschedule hproper z vC) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (fun (x : Fin (2 * residualBlockOrder head.2 - 1)) => greenFn) (primitiveAssemble (residualBlockOrder head.2) ⋯ p.1 p.2 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) : (lamEps lam ε ^ (2 * residualBlockOrder head.2) * ∫ (t : Fin (2 * residualBlockOrder head.2) → T4), ∑ τ : ReductionEndpointFiberAt κ, detJintegrand ρ ε q (↑τ) (r322AnalyticProperHeadReconstruct hq κ hκ head tail hschedule hproper z vC t) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure) = r322ReplaceEdge (fun (x : Fin (2 * q - 1)) => greenFn) (r322AnalyticProperHeadPredecessorEdge hq κ hκ head tail hschedule hproper) greenFn (primitiveKernelDiff ρ lam ε (residualBlockOrder head.2) ⋯ fun (x : Fin (2 * residualBlockOrder head.2 - 1)) => greenFn) (r322AnalyticProperHeadOutgoingKernel hq κ hκ head tail hschedule hproper z vC) (r322AnalyticProperHeadPredecessorEdge hq κ hκ head tail hschedule hproper) (r322AnalyticProperHeadPredecessorPoint hq κ hκ head tail hschedule hproper z vC) * r322AnalyticHeadOuterIntegrandFactor ρ ε κ head tail hschedule (r322AnalyticProperHeadReferenceTuple hq κ hκ head tail hschedule hproper z vC)

Standard-coordinate inner integral of the actual endpoint-fibre sum: one proper head is replaced at slot a - 1, and the complete outer factor is left unchanged.

theorem Anderson4D.lamEps_pow_integral_selected_sum_endpointFiber_detJintegrand_properHead_eq {q : ℕ} (hq : 1 ≤ q) (ρ : SmoothCutoff) (lam ε : ℝ) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (z : T4) (vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4) (hstandard : MeasureTheory.Integrable (r322AnalyticProperHeadStandardClosedIntegrand hq ρ ε κ hκ head tail hschedule hproper z vC) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (fun (x : Fin (2 * residualBlockOrder head.2 - 1)) => greenFn) (primitiveAssemble (residualBlockOrder head.2) ⋯ p.1 p.2 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) : (lamEps lam ε ^ (2 * residualBlockOrder head.2) * ∫ (vB : { i : Fin (2 * q - 2) // r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i } → T4), ∑ τ : ReductionEndpointFiberAt κ, detJintegrand ρ ε q (↑τ) (primitiveAssemble q hq z 0 (r322MergeSelectedFinCoordinates (r322InternalCoordinatesOfBlock q hq head.2) vB vC)) ∂MeasureTheory.Measure.pi fun (x : { i : Fin (2 * q - 2) // r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq head.2) i }) => paperMeasure) = r322ReplaceEdge (fun (x : Fin (2 * q - 1)) => greenFn) (r322AnalyticProperHeadPredecessorEdge hq κ hκ head tail hschedule hproper) greenFn (primitiveKernelDiff ρ lam ε (residualBlockOrder head.2) ⋯ fun (x : Fin (2 * residualBlockOrder head.2 - 1)) => greenFn) (r322AnalyticProperHeadOutgoingKernel hq κ hκ head tail hschedule hproper z vC) (r322AnalyticProperHeadPredecessorEdge hq κ hκ head tail hschedule hproper) (r322AnalyticProperHeadPredecessorPoint hq κ hκ head tail hschedule hproper z vC) * r322AnalyticHeadOuterIntegrandFactor ρ ε κ head tail hschedule (r322AnalyticProperHeadReferenceTuple hq κ hκ head tail hschedule hproper z vC)

Selected-coordinate version of the actual endpoint-fibre proper-head collapse, matching the inner integral produced by endpointFiberDetJSum_eq_analyticStepSpatialFubini.