The full-pairing half in incoming-first paper order

For the zero conserved-shift part of paper Section 4.2 Step 4(A), a complete half is most efficiently evaluated from the exceptional incoming block. This is not a new analytic argument: the certified incoming-stop Fubini seam and the alternating driver already perform all interval removals in the required order. The small adapters below identify their generic initial source with the existing complete endpoint-fibre sum.

No norm is taken in this file before the whole half has reached the empty terminal carrier.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.fullHalfOutgoingPostOuter {rho : SmoothCutoff} {C lam eps K : ℝ} {q : ℕ} {kappa : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly kappa initialScale) (beta : Z4) (y : T4) (_v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) : ℂ

The untouched outgoing endpoint character of one complete half.

Equations

• data.fullHalfOutgoingPostOuter beta y _v = Anderson4D.charT4 beta y

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integrable_fullHalfIncomingInitialSource {rho : SmoothCutoff} {C lam eps K : ℝ} {q : ℕ} {kappa : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly kappa initialScale) (heps : 0 < eps) (heps1 : eps ≤ 1) (alpha beta : Z4) : MeasureTheory.Integrable (data.incomingExceptionalInitialSourceDensity alpha (fun (y : T4) => y) (data.fullHalfOutgoingPostOuter beta)) ((paperMeasure.prod paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappa).SurvivingCoordinate) => paperMeasure))

Joint integrability of the literal complete-half source. This is just the already-proved joint L1 theorem for the initial residual, multiplied by two unimodular endpoint characters.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_sum_deterministicFullHalfIntegral_eq_fullHalfIncomingSource {rho : SmoothCutoff} {C lam eps K : ℝ} {q : ℕ} {kappa : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly kappa initialScale) (hkappa : kappa.IsFull) (heps : 0 < eps) (heps1 : eps ≤ 1) (alpha beta : Z4) : ↑(lamEps lam eps) ^ (2 * q) * ∑ tau : ReductionEndpointFiberAt kappa, deterministicFullHalfIntegral rho eps (2 * q) alpha beta ↑tau = ↑(lamEps lam eps) ^ (2 * q) * ∫ (p : (T4 × T4) × ((initial rho lam eps kappa).SurvivingCoordinate → T4)), data.incomingExceptionalInitialSourceDensity alpha (fun (y : T4) => y) (data.fullHalfOutgoingPostOuter beta) p ∂(paperMeasure.prod paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappa).SurvivingCoordinate) => paperMeasure)

The generic exceptional-stop initial source is exactly the weighted complete endpoint-fibre half. The only work is the standard initial sparse-carrier reindex and product reassociation.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.fullHalfIncomingCoefficient {rho : SmoothCutoff} {C lam eps K : ℝ} {q : ℕ} {kappa : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly kappa initialScale) (alpha beta : Z4) (y : T4) : ℂ

The incoming head coefficient of a complete half. The outgoing character is the only dependence on the outer endpoint, and there is no dependence on any surviving internal coordinate.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalPostCoefficient_fullHalf {rho : SmoothCutoff} {C lam eps K : ℝ} {q : ℕ} {kappa : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly kappa initialScale) (alpha beta : Z4) (y : T4) (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) : data.incomingExceptionalPostCoefficient alpha (data.fullHalfOutgoingPostOuter beta) y v = data.fullHalfIncomingCoefficient alpha beta y

Specialization of the generic post coefficient to a complete half.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integrable_fullHalfIncomingStopSource {rho : SmoothCutoff} {C lam eps K : ℝ} {q : ℕ} {kappa : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly kappa initialScale) (heps : 0 < eps) (heps1 : eps ≤ 1) (alpha beta : Z4) : MeasureTheory.Integrable (data.incomingExceptionalStopSourceDensity alpha (fun (y : T4) => y) (data.fullHalfOutgoingPostOuter beta)) ((paperMeasure.prod paperMeasure).prod (MeasureTheory.Measure.pi fun (x : data.trace.stopPrefix.SurvivingCoordinate) => paperMeasure))

The initial source license transported to the certified stop.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_sum_deterministicFullHalfIntegral_eq_fullHalfAfterHead {rho : SmoothCutoff} {C lam eps K : ℝ} {q : ℕ} {kappa : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly kappa initialScale) (hkappa : kappa.IsFull) (hq : 1 ≤ q) (heps : 0 < eps) (heps1 : eps ≤ 1) (hG : ∀ (j : Fin (2 * residualBlockOrder data.stopContext.step.2 - 1)), MemEClassT4 (data.stopContext.internalEdges j)) (hint : ∀ (gap first : T4) (kappaB : ↥(primitiveFullPairings (residualBlockOrder data.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4) => detJclosedIntegrandWith rho eps (2 * residualBlockOrder data.terminal.2) (↑kappaB) data.stopContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure)) (alpha beta : Z4) : ↑(lamEps lam eps) ^ (2 * q) * ∑ tau : ReductionEndpointFiberAt kappa, deterministicFullHalfIntegral rho eps (2 * q) alpha beta ↑tau = ↑(lamEps lam eps) ^ (2 * (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).remainingOrder) * ∫ (p : T4 × ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)), data.incomingExceptionalAfterHeadPhasedIntegrand alpha (fun (y : T4) => y) (data.fullHalfOutgoingPostOuter beta) p ∂paperMeasure.prod (MeasureTheory.Measure.pi fun (x : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate) => paperMeasure)

Exact paper-ordered collapse of the incoming exceptional head of a complete half. All prefix removals and the head Fourier calculation are finished before the displayed primitive defect appears.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_sum_deterministicFullHalfIntegral_eq_fullHalfDriverTerminal {rho : SmoothCutoff} {C lam eps K : ℝ} {q : ℕ} {kappa : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly kappa initialScale) (transport : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) (hkappa : kappa.IsFull) (hq : 1 ≤ q) (heps : 0 < eps) (heps1 : eps ≤ 1) (hG : ∀ (j : Fin (2 * residualBlockOrder data.stopContext.step.2 - 1)), MemEClassT4 (data.stopContext.internalEdges j)) (hint : ∀ (gap first : T4) (kappaB : ↥(primitiveFullPairings (residualBlockOrder data.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4) => detJclosedIntegrandWith rho eps (2 * residualBlockOrder data.terminal.2) (↑kappaB) data.stopContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure)) (alpha beta : Z4) : ↑(lamEps lam eps) ^ (2 * q) * ∑ tau : ReductionEndpointFiberAt kappa, deterministicFullHalfIntegral rho eps (2 * q) alpha beta ↑tau = ∫ (y : T4), transport.multiplier alpha * ∫ (u : transport.final.SurvivingCoordinate → T4), transport.final.incomingPhasedResidualDensity (data.fullHalfIncomingCoefficient alpha beta y) alpha rho eps 0 y u ∂MeasureTheory.Measure.pi fun (x : transport.final.SurvivingCoordinate) => paperMeasure ∂paperMeasure

The remaining suffix is consumed by the already-proved alternating driver. The norm is still not taken: the result is an exact integral over the outgoing endpoint and the terminal carrier.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_sum_deterministicFullHalfIntegral_eq_fullHalfZeroShift {rho : SmoothCutoff} {C lam eps K : ℝ} {q : ℕ} {kappa : PartialPairing (Fin (2 * q))} {initialScale : Fin (2 * q + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly kappa initialScale) (transport : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) (hkappa : kappa.IsFull) (hq : 1 ≤ q) (heps : 0 < eps) (heps1 : eps ≤ 1) (hG : ∀ (j : Fin (2 * residualBlockOrder data.stopContext.step.2 - 1)), MemEClassT4 (data.stopContext.internalEdges j)) (hint : ∀ (gap first : T4) (kappaB : ↥(primitiveFullPairings (residualBlockOrder data.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4) => detJclosedIntegrandWith rho eps (2 * residualBlockOrder data.terminal.2) (↑kappaB) data.stopContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure)) (alpha beta : Z4) (hshift : alpha + beta = 0) : ↑(lamEps lam eps) ^ (2 * q) * ∑ tau : ReductionEndpointFiberAt kappa, deterministicFullHalfIntegral rho eps (2 * q) alpha beta ↑tau = transport.multiplier alpha * (↑r324PaperTorusMass * (↑(paperSecondOrderModeDecay alpha) ^ 2 * incomingExceptionalPrimitiveDefect rho lam eps (residualBlockOrder data.terminal.2) ⋯ data.stopContext.internalEdges alpha))

On a full pairing the driver terminal carrier is empty. At zero conserved shift its remaining endpoint integral is exactly the paper torus mass. Thus one complete half contributes the fourth-order incoming-mode factor before any absolute value is taken.