The R-324 alternating driver

The phased construction transports the incoming residual density along ordinary heads (nonzero sparse predecessor slot) and collapses the first exceptional head at the refined physical root through two steps:

1. General-state exceptional integral collapse. At an arbitrary reachable residual prefix whose literal head is fed by slot zero, the phased density integral collapses its retained head block: the perturbative power drops by twice the head block order, the phase re-anchors after the head with one paper second-order decay, and the primitive Step-4 defect of the head is absorbed into the coefficient. Unlike the root-anchored seam, no measured parameter is present and the collapse holds at arbitrary Fourier-evaluated endpoints; the incoming Fourier decay of the root has already been extracted once and for all, so the interior collapse contributes exactly one decay, not two.

2. The alternating driver. By strong induction on the remaining list, every reachable residual prefix transports to a terminal prefix with empty remaining list: the longest ordinary run is consumed by the certified stop-before-step trace, the slot-zero-fed head at the run boundary is collapsed by the general-state exceptional step, and the strictly shorter after-head suffix recurses. All per-head Proposition 4.1 charge data is consumed from the stored edge certificates; no external charge hypothesis is taken.

Scalar linearity of the phased density

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingPhasedResidualDensity_const_mul {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (a coefficient : ℂ) (k : Z4) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (v : res.SurvivingCoordinate → T4) : res.incomingPhasedResidualDensity (a * coefficient) k ρ' ε' x y v = a * res.incomingPhasedResidualDensity coefficient k ρ' ε' x y v

The incoming phased residual density is linear in its coefficient.

The outgoing Fourier section of an arbitrary head

theorem Anderson4D.R324WithinHalfResidualPrefix.integrable_char_mul_headOutgoing_sub {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (k : Z4) (a : T4) : MeasureTheory.Integrable (fun (q : T4) => charT4 k q * ↑(res.state.edges (res.headContext head tail hremaining).outgoingSlot (q - a))) paperMeasure

The outgoing edge of the literal remaining head is still the free Green function, so its Fourier section against the head character is integrable at every translation.

The internal collapse of the phased density at fixed gap and first

theorem Anderson4D.R324WithinHalfResidualPrefix.lamEps_pow_integral_incomingPhasedResidualDensity_internal_eq_of_eq_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head = 0) (coefficient : ℂ) (k : Z4) (x y : T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) (gap first : T4) (hint : ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (res.headContext head tail hremaining).internalEdges (primitiveAssemble (residualBlockOrder head.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) (hG : ∀ (j : Fin (2 * residualBlockOrder (res.headContext head tail hremaining).step.2 - 1)), MemEClassT4 ((res.headContext head tail hremaining).internalEdges j)) : (↑(lamEps lam ε) ^ (2 * residualBlockOrder head.2) * ∫ (r : Fin (2 * residualBlockOrder head.2 - 2) → T4), res.incomingPhasedResidualDensity coefficient k ρ ε x y ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (primitiveAssemble (residualBlockOrder head.2) ⋯ first (first + gap) r, v)) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure) = charT4 k first * ↑(primitiveKernelDiff ρ lam ε (residualBlockOrder head.2) ⋯ (res.headContext head tail hremaining).internalEdges gap) * ↑(res.state.edges (res.headContext head tail hremaining).outgoingSlot (first + gap - res.headSuccessorPoint head tail hremaining x y v) - res.state.edges (res.headContext head tail hremaining).outgoingSlot (first - res.headSuccessorPoint head tail hremaining x y v)) * (coefficient * ↑(res.headOuterFactor head tail hremaining ρ ε x y v))

Fixed after-head coordinates, fixed gap, and fixed first endpoint: the phased density at a slot-zero-fed head integrates in its internal primitive coordinates to the ordinary primitiveKernelDiff, with the head character and the outgoing edge difference still exact.

The reindexed head collapse to transported mode and defect

theorem Anderson4D.R324WithinHalfResidualPrefix.integral_gap_first_lamEps_pow_incomingPhasedResidualDensity_eq_transportedMode_mul_defect {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head = 0) (coefficient : ℂ) (k : Z4) (x y : T4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) (hint : ∀ (gap first : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (res.headContext head tail hremaining).internalEdges (primitiveAssemble (residualBlockOrder head.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) (hG : ∀ (j : Fin (2 * residualBlockOrder (res.headContext head tail hremaining).step.2 - 1)), MemEClassT4 ((res.headContext head tail hremaining).internalEdges j)) : ∫ (gap : T4), ∫ (first : T4), ↑(lamEps lam ε) ^ (2 * residualBlockOrder head.2) * ∫ (r : Fin (2 * residualBlockOrder head.2 - 2) → T4), res.incomingPhasedResidualDensity coefficient k ρ ε x y ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (primitiveAssemble (residualBlockOrder head.2) ⋯ first (first + gap) r, v)) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure ∂paperMeasure ∂paperMeasure = incomingExceptionalTransportedMode k (res.headSuccessorPoint head tail hremaining x y v) (res.state.edges (res.headContext head tail hremaining).outgoingSlot) * incomingExceptionalPrimitiveDefect ρ lam ε (residualBlockOrder head.2) ⋯ (res.headContext head tail hremaining).internalEdges k * (coefficient * ↑(res.headOuterFactor head tail hremaining ρ ε x y v))

The reindexed (gap, first, internal) double integral of the phased density collapses to the transported outgoing Fourier mode times the single ordinary primitive defect, with the coefficient and the head outer factor untouched.

The general-state collapsed-head coefficient

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.incomingExceptionalHeadCollapseFactor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (k : Z4) : ℂ

The scalar produced by collapsing one slot-zero-fed head of the phased density: one paper second-order decay from the transported outgoing Green mode and the primitive Step-4 defect of the head internal edges. The second decay of the root-anchored collapse came from the incoming Fourier evaluation of the root, which happens only once; the general-state interior collapse contributes exactly this factor.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.incomingExceptionalGeneralPostCoefficient {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (k : Z4) (postCoefficient : ((res.afterHead head tail hremaining).SurvivingCoordinate → T4) → ℂ) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : ℂ

General-state analogue of the seam-2 post coefficient: the collapsed head factor times a genuinely coordinate-dependent after-head coefficient.

Equations

• res.incomingExceptionalGeneralPostCoefficient head tail hremaining k postCoefficient v = res.incomingExceptionalHeadCollapseFactor head tail hremaining k * postCoefficient v

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.incomingExceptionalGeneralAfterHeadPhasedIntegrand {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (k : Z4) (x y : T4) (postCoefficient : ((res.afterHead head tail hremaining).SurvivingCoordinate → T4) → ℂ) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) : ℂ

General-state analogue of the seam-2 after-head phased integrand: the after-head phased residual density carrying the collapsed head as its coordinate-dependent coefficient, at arbitrary endpoints.

Equations

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

The head-section collapse at fixed after-head coordinates

theorem Anderson4D.R324WithinHalfResidualPrefix.lamEps_pow_integral_incomingPhasedResidualDensity_head_section_eq_afterHead_of_eq_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head = 0) (x y : T4) (postCoefficient : ((res.afterHead head tail hremaining).SurvivingCoordinate → T4) → ℂ) (k : Z4) (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) (hhead : MeasureTheory.Integrable (fun (t : Fin (2 * residualBlockOrder head.2) → T4) => res.incomingPhasedResidualDensity (postCoefficient v) k ρ ε x y ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v))) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure)) (hint : ∀ (gap first : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (res.headContext head tail hremaining).internalEdges (primitiveAssemble (residualBlockOrder head.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) (hG : ∀ (j : Fin (2 * residualBlockOrder (res.headContext head tail hremaining).step.2 - 1)), MemEClassT4 ((res.headContext head tail hremaining).internalEdges j)) : (↑(lamEps lam ε) ^ (2 * residualBlockOrder head.2) * ∫ (t : Fin (2 * residualBlockOrder head.2) → T4), res.incomingPhasedResidualDensity (postCoefficient v) k ρ ε x y ((res.splitSurvivingPiMeasurableEquiv head tail hremaining).symm (t, v)) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure) = res.incomingExceptionalGeneralAfterHeadPhasedIntegrand head tail hremaining k x y postCoefficient v

Fixed after-head coordinates: integrating the retained head tuple of the phased density at a slot-zero-fed head produces exactly the after-head phased density with the collapsed-head coefficient.

The general-state exceptional collapse at the integral level

theorem Anderson4D.R324WithinHalfResidualPrefix.lamEps_pow_integral_incomingPhasedResidualDensity_eq_afterHead_of_eq_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head = 0) (x y : T4) (postCoefficient : ((res.afterHead head tail hremaining).SurvivingCoordinate → T4) → ℂ) (k : Z4) (hfull : MeasureTheory.Integrable (fun (w : res.SurvivingCoordinate → T4) => res.incomingPhasedResidualDensity (postCoefficient ((res.splitSurvivingPiMeasurableEquiv head tail hremaining) w).2) k ρ ε x y w) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) (hint : ∀ (gap first : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (res.headContext head tail hremaining).internalEdges (primitiveAssemble (residualBlockOrder head.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) (hG : ∀ (j : Fin (2 * residualBlockOrder (res.headContext head tail hremaining).step.2 - 1)), MemEClassT4 ((res.headContext head tail hremaining).internalEdges j)) : (↑(lamEps lam ε) ^ (2 * res.remainingOrder) * ∫ (w : res.SurvivingCoordinate → T4), res.incomingPhasedResidualDensity (postCoefficient ((res.splitSurvivingPiMeasurableEquiv head tail hremaining) w).2) k ρ ε x y w ∂MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) = ↑(lamEps lam ε) ^ (2 * (res.afterHead head tail hremaining).remainingOrder) * ∫ (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4), res.incomingExceptionalGeneralAfterHeadPhasedIntegrand head tail hremaining k x y postCoefficient v ∂MeasureTheory.Measure.pi fun (x : (res.afterHead head tail hremaining).SurvivingCoordinate) => paperMeasure

General-state exceptional head absorption. At a slot-zero-fed head the weighted phased density integral collapses its retained head tuple: the perturbative power drops by twice the head block order and the integrand becomes exactly the after-head phased density with the collapsed-head coefficient, at arbitrary endpoints.

theorem Anderson4D.R324WithinHalfResidualPrefix.integrable_afterHead_incomingPhasedResidualDensity_of_eq_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head = 0) (x y : T4) (postCoefficient : ((res.afterHead head tail hremaining).SurvivingCoordinate → T4) → ℂ) (k : Z4) (hfull : MeasureTheory.Integrable (fun (w : res.SurvivingCoordinate → T4) => res.incomingPhasedResidualDensity (postCoefficient ((res.splitSurvivingPiMeasurableEquiv head tail hremaining) w).2) k ρ ε x y w) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) (hint : ∀ (gap first : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (res.headContext head tail hremaining).internalEdges (primitiveAssemble (residualBlockOrder head.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) (hG : ∀ (j : Fin (2 * residualBlockOrder (res.headContext head tail hremaining).step.2 - 1)), MemEClassT4 ((res.headContext head tail hremaining).internalEdges j)) : MeasureTheory.Integrable (fun (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) => res.incomingExceptionalGeneralAfterHeadPhasedIntegrand head tail hremaining k x y postCoefficient v) (MeasureTheory.Measure.pi fun (x : (res.afterHead head tail hremaining).SurvivingCoordinate) => paperMeasure)

General-state integrability handover. The after-head phased density with the collapsed-head coefficient is integrable over the after-head coordinates. This is the recursion seam feeding the next ordinary run of the alternating driver.

Parameter-carrying exceptional head

theorem Anderson4D.R324WithinHalfResidualPrefix.integrable_joint_afterHead_incomingPhasedResidualDensity_of_eq_zero {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {Y : Type u_1} [MeasurableSpace Y] (ν : MeasureTheory.Measure Y) [MeasureTheory.SFinite ν] (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (hpred : r324WithinHalfPredecessorSlot res.state head = 0) (x y : Y → T4) (postCoefficient : Y → ((res.afterHead head tail hremaining).SurvivingCoordinate → T4) → ℂ) (k : Z4) (hfull : MeasureTheory.Integrable (fun (p : Y × (res.SurvivingCoordinate → T4)) => res.incomingPhasedResidualDensity (postCoefficient p.1 ((res.splitSurvivingPiMeasurableEquiv head tail hremaining) p.2).2) k ρ ε (x p.1) (y p.1) p.2) (ν.prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))) (hint : ∀ (gap first : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (res.headContext head tail hremaining).internalEdges (primitiveAssemble (residualBlockOrder head.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)) (hG : ∀ (j : Fin (2 * residualBlockOrder (res.headContext head tail hremaining).step.2 - 1)), MemEClassT4 ((res.headContext head tail hremaining).internalEdges j)) : MeasureTheory.Integrable (fun (p : Y × ((res.afterHead head tail hremaining).SurvivingCoordinate → T4)) => res.incomingExceptionalGeneralAfterHeadPhasedIntegrand head tail hremaining k (x p.1) (y p.1) (postCoefficient p.1) p.2) (ν.prod (MeasureTheory.Measure.pi fun (x : (res.afterHead head tail hremaining).SurvivingCoordinate) => paperMeasure))

Joint integrability crosses one slot-zero-fed head while all external endpoint parameters remain outside the signed head integral.

The two-phase combinator at the packaged next exceptional stop

One ordinary run followed by one exceptional head collapse, with every Proposition 4.1 charge consumed from the edge certificate stored in the certified stop-before-step trace.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfNextExceptionalStop.stopCertificate_hint {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (data : res.R324WithinHalfNextExceptionalStop scale) (hε : 0 < ε) (hε1 : ε ≤ 1) (gap first : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder data.terminal.2))) : MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder data.terminal.2) (↑κB) (data.trace.stopPrefix.headContext data.terminal data.suffix ⋯).internalEdges (primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure)

The detJ charges of the retained head are supplied pointwise by the stop certificate transported along the consumed ordinary run.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfNextExceptionalStop.stopCertificate_memE {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (data : res.R324WithinHalfNextExceptionalStop scale) (j : Fin (2 * residualBlockOrder (data.trace.stopPrefix.headContext data.terminal data.suffix ⋯).step.2 - 1)) : MemEClassT4 ((data.trace.stopPrefix.headContext data.terminal data.suffix ⋯).internalEdges j)

The internal edges of the retained head lie in the paper's symmetry class, again by the transported stop certificate.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfNextExceptionalStop.lamEps_pow_integral_incomingPhasedResidualDensity_eq_afterHead {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (data : res.R324WithinHalfNextExceptionalStop scale) (hε : 0 < ε) (hε1 : ε ≤ 1) (x y : T4) (postCoefficient : ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ) (k : Z4) (hfull : MeasureTheory.Integrable (fun (w : res.SurvivingCoordinate → T4) => res.incomingPhasedResidualDensity (postCoefficient ((data.trace.stopPrefix.splitSurvivingPiMeasurableEquiv data.terminal data.suffix ⋯) (data.trace.stopProjection w)).2) k ρ ε x y w) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) : (↑(lamEps lam ε) ^ (2 * res.remainingOrder) * ∫ (w : res.SurvivingCoordinate → T4), res.incomingPhasedResidualDensity (postCoefficient ((data.trace.stopPrefix.splitSurvivingPiMeasurableEquiv data.terminal data.suffix ⋯) (data.trace.stopProjection w)).2) k ρ ε x y w ∂MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) = ↑(lamEps lam ε) ^ (2 * (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).remainingOrder) * ∫ (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4), data.trace.stopPrefix.incomingExceptionalGeneralAfterHeadPhasedIntegrand data.terminal data.suffix ⋯ k x y postCoefficient v ∂MeasureTheory.Measure.pi fun (x : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate) => paperMeasure

Two-phase combinator. The ordinary run is consumed by the phased stop transport and the slot-zero-fed head at the run boundary is collapsed by the general-state exceptional step: the weighted phased integral at the starting prefix equals the weighted after-head phased integral with the collapsed-head coefficient. All charges come from the stored certificate.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfNextExceptionalStop.integrable_afterHead_incomingPhasedResidualDensity {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (data : res.R324WithinHalfNextExceptionalStop scale) (hε : 0 < ε) (hε1 : ε ≤ 1) (x y : T4) (postCoefficient : ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ) (k : Z4) (hfull : MeasureTheory.Integrable (fun (w : res.SurvivingCoordinate → T4) => res.incomingPhasedResidualDensity (postCoefficient ((data.trace.stopPrefix.splitSurvivingPiMeasurableEquiv data.terminal data.suffix ⋯) (data.trace.stopProjection w)).2) k ρ ε x y w) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) : MeasureTheory.Integrable (fun (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) => data.trace.stopPrefix.incomingExceptionalGeneralAfterHeadPhasedIntegrand data.terminal data.suffix ⋯ k x y postCoefficient v) (MeasureTheory.Measure.pi fun (x : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate) => paperMeasure)

Integrability handover of the two-phase combinator: the after-head phased density with the collapsed-head coefficient is integrable.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfNextExceptionalStop.integrable_joint_afterHead_incomingPhasedResidualDensity {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} {Y : Type u_1} [MeasurableSpace Y] (ν : MeasureTheory.Measure Y) [MeasureTheory.SFinite ν] (data : res.R324WithinHalfNextExceptionalStop scale) (hε : 0 < ε) (hε1 : ε ≤ 1) (x y : Y → T4) (postCoefficient : Y → ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ) (k : Z4) (hfull : MeasureTheory.Integrable (fun (p : Y × (res.SurvivingCoordinate → T4)) => res.incomingPhasedResidualDensity (postCoefficient p.1 ((data.trace.stopPrefix.splitSurvivingPiMeasurableEquiv data.terminal data.suffix ⋯) (data.trace.stopProjection p.2)).2) k ρ ε (x p.1) (y p.1) p.2) (ν.prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))) : MeasureTheory.Integrable (fun (p : Y × ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)) => data.trace.stopPrefix.incomingExceptionalGeneralAfterHeadPhasedIntegrand data.terminal data.suffix ⋯ k (x p.1) (y p.1) (postCoefficient p.1) p.2) (ν.prod (MeasureTheory.Measure.pi fun (x : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate) => paperMeasure))

Joint version of the ordinary-run-plus-exceptional-head handover. The external parameter represents the untouched opposite half in paper Step 4(A); it is never normed or summed during the signed elimination.

The alternating transport package

structure Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfAlternatingTransport {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : Type

Complete phased transport from a reachable residual prefix to a terminal prefix with empty remaining list. The multiplier accumulates one collapsed-head factor per exceptional stop crossed by the alternation; the projection restricts a surviving tuple along the value-preserving coordinate embedding. The transport and integrability fields hold at every pair of Fourier-evaluated endpoints, every incoming mode, and every terminal-coordinate-dependent coefficient.

• final : R324WithinHalfResidualPrefix ρ lam ε pairing
• final_remaining : self.final.remaining = []
• embedding : self.final.SurvivingCoordinate → res.SurvivingCoordinate
• embedding_val (i : self.final.SurvivingCoordinate) : ↑(self.embedding i) = ↑i
• projection : (res.SurvivingCoordinate → T4) → self.final.SurvivingCoordinate → T4
• projection_apply (v : res.SurvivingCoordinate → T4) (i : self.final.SurvivingCoordinate) : self.projection v i = v (self.embedding i)
• multiplier : Z4 → ℂ
• transport (x y : T4) (k : Z4) (coefficient : (self.final.SurvivingCoordinate → T4) → ℂ) : MeasureTheory.Integrable (fun (w : res.SurvivingCoordinate → T4) => res.incomingPhasedResidualDensity (coefficient (self.projection w)) k ρ ε x y w) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) → (↑(lamEps lam ε) ^ (2 * res.remainingOrder) * ∫ (w : res.SurvivingCoordinate → T4), res.incomingPhasedResidualDensity (coefficient (self.projection w)) k ρ ε x y w ∂MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) = ∫ (u : self.final.SurvivingCoordinate → T4), self.final.incomingPhasedResidualDensity (self.multiplier k * coefficient u) k ρ ε x y u ∂MeasureTheory.Measure.pi fun (x : self.final.SurvivingCoordinate) => paperMeasure
• integrable (x y : T4) (k : Z4) (coefficient : (self.final.SurvivingCoordinate → T4) → ℂ) : MeasureTheory.Integrable (fun (w : res.SurvivingCoordinate → T4) => res.incomingPhasedResidualDensity (coefficient (self.projection w)) k ρ ε x y w) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) → MeasureTheory.Integrable (fun (u : self.final.SurvivingCoordinate → T4) => self.final.incomingPhasedResidualDensity (self.multiplier k * coefficient u) k ρ ε x y u) (MeasureTheory.Measure.pi fun (x : self.final.SurvivingCoordinate) => paperMeasure)
• integrable_joint {Y : Type} [MeasurableSpace Y] (ν : MeasureTheory.Measure Y) [MeasureTheory.SFinite ν] (x y : Y → T4) (k : Z4) (coefficient : Y → (self.final.SurvivingCoordinate → T4) → ℂ) : MeasureTheory.Integrable (fun (p : Y × (res.SurvivingCoordinate → T4)) => res.incomingPhasedResidualDensity (coefficient p.1 (self.projection p.2)) k ρ ε (x p.1) (y p.1) p.2) (ν.prod (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) → MeasureTheory.Integrable (fun (p : Y × (self.final.SurvivingCoordinate → T4)) => self.final.incomingPhasedResidualDensity (self.multiplier k * coefficient p.1 p.2) k ρ ε (x p.1) (y p.1) p.2) (ν.prod (MeasureTheory.Measure.pi fun (x : self.final.SurvivingCoordinate) => paperMeasure))

  Parameter-carrying integrability required by the paper's delayed Fubini step. No absolute value is taken before both halves are eliminated.

Base case: the all-ordinary run

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.alternatingTransport {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : res.R324WithinHalfCertifiedAnalyticTrace scale) (hordinary : trace.OrdinaryAlong) : res.R324WithinHalfAlternatingTransport

A certified analytic trace ordinary along its whole remaining list is already a complete alternating transport, with trivial multiplier.

Equations

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

Recursion step: one exceptional stop, then an arbitrary transport

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfNextExceptionalStop.alternatingTransport {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (data : res.R324WithinHalfNextExceptionalStop scale) (hε : 0 < ε) (hε1 : ε ≤ 1) (sub : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) : res.R324WithinHalfAlternatingTransport

A packaged next exceptional stop composed with an alternating transport of its after-head prefix is an alternating transport of the starting prefix. The multiplier gains the collapsed-head factor of the retained head.

Equations

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

The alternating driver

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfNextExceptionalStop.suffix_length_lt {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (data : res.R324WithinHalfNextExceptionalStop scale) : data.suffix.length < res.remaining.length

The order ledger of the alternation: the retained suffix past the next exceptional stop is strictly shorter than the remaining list, because the consumed ordinary run and the retained head are genuinely dropped.

@[irreducible]

def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfAlternatingTransport.of_localBlockProvider {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {C K : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K pairing) (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (scale : Fin (m + 1) → ℝ) (certificate : R324WithinHalfEdgeCertificate res.state scale) : res.R324WithinHalfAlternatingTransport

The alternating driver. By strong induction on the remaining list: the longest ordinary run either exhausts the remaining list and the certified analytic trace finishes the transport, or it stops at a slot-zero-fed head, which the general-state exceptional collapse absorbs before the strictly shorter after-head suffix recurses. Every ordinary Fubini charge and every exceptional Proposition 4.1 charge is consumed from the certificates produced by the local block provider; no external charge hypothesis is taken.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfAlternatingTransport.lamEps_pow_integral_incomingPhasedResidualDensity_eq_multiplier_mul_final {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} (t : res.R324WithinHalfAlternatingTransport) (x y : T4) (k : Z4) (coefficient : (t.final.SurvivingCoordinate → T4) → ℂ) (hfull : MeasureTheory.Integrable (fun (w : res.SurvivingCoordinate → T4) => res.incomingPhasedResidualDensity (coefficient (t.projection w)) k ρ ε x y w) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)) : (↑(lamEps lam ε) ^ (2 * res.remainingOrder) * ∫ (w : res.SurvivingCoordinate → T4), res.incomingPhasedResidualDensity (coefficient (t.projection w)) k ρ ε x y w ∂MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) = t.multiplier k * ∫ (u : t.final.SurvivingCoordinate → T4), t.final.incomingPhasedResidualDensity (coefficient u) k ρ ε x y u ∂MeasureTheory.Measure.pi fun (x : t.final.SurvivingCoordinate) => paperMeasure

Consumer form of the driver transport with the accumulated multiplier outside the terminal integral.