The common weighted-majorant exit for the EE x EE endpoint branch

The signed endpoint calculation is branch-dependent, but its numerical exit is not. Once the two endpoint operations have produced a density on the completed two-half carrier, the grouped Step 3 majorant, the complete run, and the ambient-order scale absorption are exactly the same for all sixteen endpoint patterns.

This file packages that common exit before specializing it to the literal EE x EE signed density. In particular, no endpoint norm is introduced here: the caller supplies the pointwise estimate obtained only after its four signed endpoint operations are complete.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.r324ResidualPrimitiveSumProduct_eq_rightEndpointStopProjection {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} (left : R324WithinHalfResidualPrefix rho lam eps kappaP) {right : R324WithinHalfResidualPrefix rho lam eps kappaM} {terminal : R322ExtractionStep m} (endpoint : R324WithinHalfEndpointStopAtTerminal terminal right) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (u : left.SurvivingCoordinate → T4) (v : right.SurvivingCoordinate → T4) : r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi (r324TwoHalfRootDoubledReconstruct left right (u, v)) = r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi (r324TwoHalfRootDoubledReconstruct left endpoint.stop (u, endpoint.projection v))

Projecting a right residual carrier to an endpoint stop does not change the cross primitive factor. This is the endpoint-stop analogue of the alternating-transport projection lemma already used by the ED branch.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.r324ResidualPrimitiveSumProduct_eq_rightOutgoingTerminalPost {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (left : R324WithinHalfResidualPrefix rho lam eps kappaP) (data : R324IncomingExceptionalStopTraceAssembly kappaM initialScale) (outgoing : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324PaperOutgoingEndpointTerminal) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (u : left.SurvivingCoordinate → T4) (v : outgoing.endpoint.stop.SurvivingCoordinate → T4) : r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi (r324TwoHalfRootDoubledReconstruct left outgoing.endpoint.stop (u, v)) = r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi (r324TwoHalfRootDoubledReconstruct left outgoing.terminalPost (u, ((outgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv outgoing.terminalData.terminal [] ⋯) v).2))

Right-half mirror of r324ResidualPrimitiveSumProduct_eq_leftOutgoingTerminalPost. Consuming the retained right terminal leaves the cross-cut primitive factor unchanged, because that factor sees only residual singles and all of those coordinates survive in terminalPost.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.r324ResidualPrimitiveSumProduct_eq_rightIncomingOutgoingPost {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (left : R324WithinHalfResidualPrefix rho lam eps kappaP) (data : R324IncomingExceptionalStopTraceAssembly kappaM initialScale) (outgoing : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324PaperOutgoingEndpointTerminal) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (u : left.SurvivingCoordinate → T4) (v : (initial rho lam eps kappaM).SurvivingCoordinate → T4) : r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi (r324TwoHalfRootDoubledReconstruct left (initial rho lam eps kappaM) (u, v)) = r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi (r324TwoHalfRootDoubledReconstruct left outgoing.terminalPost (u, ((outgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv outgoing.terminalData.terminal [] ⋯) (outgoing.endpoint.projection ((data.trace.stopPrefix.splitSurvivingPiMeasurableEquiv data.terminal data.suffix ⋯) (data.trace.stopProjection v)).2)).2))

Complete right-half projection from the initial residual carrier through its exceptional incoming stop and the retained outgoing terminal. It is the coordinate identity needed when the completed left EE half is used as the untouched parameter of the right parameterized EE theorem.

The last Fubini move in the EE x EE branch. It swaps the left free outgoing variable past the completed right residual carrier, after all four signed endpoint operations have already been performed.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.r324EEEEEndpointRegroupMeasurableEquiv (L : Type u_1) (R : Type u_2) [MeasurableSpace L] [MeasurableSpace R] : ((L × T4) × R) × T4 ≃ᵐ (L × R) × T4 × T4

(((left, firstLeft), right), firstRight) regrouped as ((left, right), (firstLeft, firstRight)).

Equations

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

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.r324EEEEEndpointRegroupMeasurableEquiv_apply {L : Type u_1} {R : Type u_2} [MeasurableSpace L] [MeasurableSpace R] (q : ((L × T4) × R) × T4) : (r324EEEEEndpointRegroupMeasurableEquiv L R) q = ((q.1.1.1, q.1.2), q.1.1.2, q.2)

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.r324EEEEEndpointRegroupMeasurableEquiv_symm_apply {L : Type u_1} {R : Type u_2} [MeasurableSpace L] [MeasurableSpace R] (q : (L × R) × T4 × T4) : (r324EEEEEndpointRegroupMeasurableEquiv L R).symm q = (((q.1.1, q.2.1), q.1.2), q.2.2)

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.measurePreserving_r324EEEEEndpointRegroupMeasurableEquiv {L : Type u_1} {R : Type u_2} [MeasurableSpace L] [MeasurableSpace R] (muL : MeasureTheory.Measure L) (muR : MeasureTheory.Measure R) [MeasureTheory.SFinite muL] [MeasureTheory.SFinite muR] : MeasureTheory.MeasurePreserving (⇑(r324EEEEEndpointRegroupMeasurableEquiv L R)) (((muL.prod paperMeasure).prod muR).prod paperMeasure) ((muL.prod muR).prod (paperMeasure.prod paperMeasure))

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integral_eeeeEndpoint_regroup {L : Type u_1} {R : Type u_2} [MeasurableSpace L] [MeasurableSpace R] (muL : MeasureTheory.Measure L) (muR : MeasureTheory.Measure R) [MeasureTheory.SFinite muL] [MeasureTheory.SFinite muR] (F : ((L × T4) × R) × T4 → ℂ) (hF : MeasureTheory.Integrable F (((muL.prod paperMeasure).prod muR).prod paperMeasure)) : ∫ (u : L × T4), ∫ (v : R), ∫ (first : T4), F ((u, v), first) ∂paperMeasure ∂muR ∂muL.prod paperMeasure = ∫ (p : L × R), ∫ (firstLeft : T4), ∫ (firstRight : T4), F (((p.1, firstLeft), p.2), firstRight) ∂paperMeasure ∂paperMeasure ∂muL.prod muR

Fubini in the only order used by the EE x EE branch. The hypothesis is joint integrability of the already completed signed four-endpoint density, so this swap occurs strictly after all interval removals.

The first exceptional charge in the outgoing-stop budget

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.R324IncomingExceptionalBudgetedStopTraceAssembly.firstExceptionalScale_mul_K_le_afterHeadBudgetScale {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP : PartialPairing (Fin m)} {A : ℝ} (pack : R324IncomingExceptionalBudgetedStopTraceAssembly kappaP) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hK : 0 ≤ K) (hA : 1 ≤ A) : pack.firstExceptionalScale * K ≤ pack.afterHeadBudgetScale 0

The complete after-head budget contains the first exceptional scale together with its local block constant. This is the exact scalar form needed when the retained outgoing endpoint is estimated after the signed incoming collapse.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.R324IncomingExceptionalBudgetedStopTraceAssembly.norm_multiplier_mul_squaredDecay_defect_le_stopBudget {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP : PartialPairing (Fin m)} {A : ℝ} {terminal : R322ExtractionStep m} {mode : Z4} (pack : R324IncomingExceptionalBudgetedStopTraceAssembly kappaP) (endpoint : R324BudgetedEndpointStopAtTerminal terminal (pack.data.trace.stopPrefix.afterHead pack.data.terminal pack.data.suffix ⋯) pack.afterHeadBudgetScale mode) (headBudget : R324WithinHalfInsertedExceptionalHeadBudget rho C lam eps K kappaP mode) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hK : 0 ≤ K) (hA : 1 ≤ A) : ‖endpoint.endpoint.multiplier mode * (↑(paperSecondOrderModeDecay mode) ^ 2 * incomingExceptionalPrimitiveDefect rho lam eps (residualBlockOrder pack.data.terminal.2) ⋯ pack.data.stopContext.internalEdges mode)‖ ≤ paperSecondOrderModeDecay mode * endpoint.stopBudgetScale 0

After the first signed exceptional collapse, the one remaining Fourier decay is explicit and the complete endpoint-stop budget pays the multiplier and the primitive defect.

The literal signed EE x EE carrier

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.eeeeLeftEndpointFactor {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP : PartialPairing (Fin m)} {leftScale : Fin (m + 1) → ℝ} (leftData : R324IncomingExceptionalStopTraceAssembly kappaP leftScale) (leftOutgoing : (leftData.trace.stopPrefix.afterHead leftData.terminal leftData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (alpha beta : Z4) (v : leftOutgoing.terminalPost.SurvivingCoordinate → T4) (first : T4) : ℂ

Everything produced by the completed left EE endpoint operation except the untouched right residual core and the cross primitive factor. The outgoing primitive and its external Fourier variable are still kept as one signed density; no norm occurs in this definition.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.eeeeRightPostCoefficient {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftScale : Fin (m + 1) → ℝ} {rightResidual : R324WithinHalfResidualPrefix rho lam eps kappaM} (leftData : R324IncomingExceptionalStopTraceAssembly kappaP leftScale) (leftOutgoing : (leftData.trace.stopPrefix.afterHead leftData.terminal leftData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (rightOutgoing : rightResidual.R324PaperOutgoingEndpointTerminal) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (alpha beta : Z4) (u : (leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4) (v : rightOutgoing.terminalPost.SurvivingCoordinate → T4) : ℂ

Coefficient left untouched while the right EE endpoint operation is performed. Its only dependence on the right post-terminal coordinates is the complete grouped cross primitive factor.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.eeeeRightInitialSourceDensity {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftData : R324IncomingExceptionalStopTraceAssembly kappaP leftScale) (leftOutgoing : (leftData.trace.stopPrefix.afterHead leftData.terminal leftData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (rightData : R324IncomingExceptionalStopTraceAssembly kappaM rightScale) (rightOutgoing : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (alpha beta : Z4) : (T4 × T4 × (leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4) × ((initial rho lam eps kappaM).SurvivingCoordinate → T4) → ℂ

The exact right initial-source density after the completed left EE carrier has been moved into the parameter slot.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.eeeeRightStopSourceDensity {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftData : R324IncomingExceptionalStopTraceAssembly kappaP leftScale) (leftOutgoing : (leftData.trace.stopPrefix.afterHead leftData.terminal leftData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (rightData : R324IncomingExceptionalStopTraceAssembly kappaM rightScale) (rightOutgoing : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (alpha beta : Z4) : (T4 × T4 × (leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4) × (rightData.trace.stopPrefix.SurvivingCoordinate → T4) → ℂ

The corresponding right stop-source density. It differs from the previous definition only by the residual carrier on which the signed trace is evaluated.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.eeeeRightEndpointIntegrand {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftData : R324IncomingExceptionalStopTraceAssembly kappaP leftScale) (leftOutgoing : (leftData.trace.stopPrefix.afterHead leftData.terminal leftData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (rightData : R324IncomingExceptionalStopTraceAssembly kappaM rightScale) (rightOutgoing : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (alpha beta : Z4) : (T4 × (leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4) × (rightOutgoing.endpoint.stop.SurvivingCoordinate → T4) → ℂ

Signed right endpoint-stop density after the right exceptional head and all proper-prefix intervals have been removed.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.eeeeFinalRawEndpointDensity {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftData : R324IncomingExceptionalStopTraceAssembly kappaP leftScale) (leftOutgoing : (leftData.trace.stopPrefix.afterHead leftData.terminal leftData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (rightData : R324IncomingExceptionalStopTraceAssembly kappaM rightScale) (rightOutgoing : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (alpha beta : Z4) (u : (leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4) (v : rightOutgoing.terminalPost.SurvivingCoordinate → T4) (first : T4) : ℂ

Literal signed terminal density after all four exceptional endpoint operations. The two free outgoing variables are still integrated outside this function; no absolute value has been taken.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.eeeeTerminalData {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftData : R324IncomingExceptionalStopTraceAssembly kappaP leftScale) (leftOutgoing : (leftData.trace.stopPrefix.afterHead leftData.terminal leftData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (rightData : R324IncomingExceptionalStopTraceAssembly kappaM rightScale) (rightOutgoing : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).R324PaperOutgoingEndpointTerminal) : R324TwoHalfTerminalData rho lam eps kappaP kappaM

The literal completed two-half carrier produced by the two retained outgoing exceptional terminals.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.eeeeFinalRawEndpointMeasure {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftData : R324IncomingExceptionalStopTraceAssembly kappaP leftScale) (leftOutgoing : (leftData.trace.stopPrefix.afterHead leftData.terminal leftData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (rightData : R324IncomingExceptionalStopTraceAssembly kappaM rightScale) (rightOutgoing : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).R324PaperOutgoingEndpointTerminal) : MeasureTheory.Measure ((((leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4) × (rightOutgoing.terminalPost.SurvivingCoordinate → T4)) × T4)

Joint product measure for the already completed four-endpoint signed density, in paper order left post, left free endpoint, right post, right free endpoint.

Equations

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

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.eeeeNestedEndpointDensity {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftData : R324IncomingExceptionalStopTraceAssembly kappaP leftScale) (leftOutgoing : (leftData.trace.stopPrefix.afterHead leftData.terminal leftData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (rightData : R324IncomingExceptionalStopTraceAssembly kappaM rightScale) (rightOutgoing : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (alpha beta : Z4) (v : (leftData.eeeeTerminalData leftOutgoing rightData rightOutgoing).NestedCoordinate pi → T4) : ℂ

The four signed endpoint operations, with their two free outgoing variables integrated, reindexed onto the literal initial nested carrier.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integral_eeeeFinalRaw_eq_integral_nestedEndpointDensity {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftData : R324IncomingExceptionalStopTraceAssembly kappaP leftScale) (leftOutgoing : (leftData.trace.stopPrefix.afterHead leftData.terminal leftData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (rightData : R324IncomingExceptionalStopTraceAssembly kappaM rightScale) (rightOutgoing : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (alpha beta : Z4) (hraw : MeasureTheory.Integrable (fun (q : (((leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4) × (rightOutgoing.terminalPost.SurvivingCoordinate → T4)) × T4) => leftData.eeeeFinalRawEndpointDensity leftOutgoing rightData rightOutgoing pi alpha beta q.1.1 q.1.2 q.2) (leftData.eeeeFinalRawEndpointMeasure leftOutgoing rightData rightOutgoing)) : ∫ (u : (leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4), ∫ (v : rightOutgoing.terminalPost.SurvivingCoordinate → T4), ∫ (first : T4), leftData.eeeeFinalRawEndpointDensity leftOutgoing rightData rightOutgoing pi alpha beta u v first ∂paperMeasure ∂MeasureTheory.Measure.pi fun (x : rightOutgoing.terminalPost.SurvivingCoordinate) => paperMeasure ∂(MeasureTheory.Measure.pi fun (x : leftOutgoing.terminalPost.SurvivingCoordinate) => paperMeasure).prod paperMeasure = ∫ (v : (leftData.eeeeTerminalData leftOutgoing rightData rightOutgoing).NestedCoordinate pi → T4), leftData.eeeeNestedEndpointDensity leftOutgoing rightData rightOutgoing pi alpha beta v ∂MeasureTheory.Measure.pi fun (x : (leftData.eeeeTerminalData leftOutgoing rightData rightOutgoing).NestedCoordinate pi) => paperMeasure

Exact final Fubini/reindexing bridge from the parameterized right EE output to the nested endpoint carrier consumed by the grouped Step 3 majorant.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.outgoingEndpointDefectDensity_eq_rightExceptionalInitialSource {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftData : R324IncomingExceptionalStopTraceAssembly kappaP leftScale) (leftOutgoing : (leftData.trace.stopPrefix.afterHead leftData.terminal leftData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (rightData : R324IncomingExceptionalStopTraceAssembly kappaM rightScale) (rightOutgoing : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (alpha beta : Z4) (s : (T4 × T4) × ((initial rho lam eps kappaM).SurvivingCoordinate → T4)) (v : leftOutgoing.terminalPost.SurvivingCoordinate → T4) (first : T4) : leftOutgoing.outgoingEndpointDefectDensity (leftData.incomingExceptionalRefinedRootOutgoingPostCoefficient leftOutgoing alpha beta pi s) alpha beta 0 v first = rightData.incomingExceptionalInitialSourceDensity (-alpha) (fun (omega : T4 × (leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4) => omega.1) (fun (omega : T4 × (leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4) (post : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).SurvivingCoordinate → T4) => charT4 (-beta) omega.1 * leftData.eeeeRightPostCoefficient leftOutgoing rightOutgoing pi alpha beta omega.2 ((rightOutgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv rightOutgoing.terminalData.terminal [] ⋯) (rightOutgoing.endpoint.projection post)).2) ((s.1.1, s.1.2, v, first), s.2)

After the left EE operation, reassociating ((right endpoints, right initial coordinates), left post, left first) produces exactly the initial-source density consumed by the parameterized right EE theorem. The cross factor is moved to the right post-terminal carrier only by the two exact projection lemmas above.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integrable_and_integral_leftExceptional_eq_rightExceptionalInitialSource {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftData : R324IncomingExceptionalStopTraceAssembly kappaP leftScale) (leftOutgoing : (leftData.trace.stopPrefix.afterHead leftData.terminal leftData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (rightData : R324IncomingExceptionalStopTraceAssembly kappaM rightScale) (rightOutgoing : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (alpha beta : Z4) (hleftIntegrable : MeasureTheory.Integrable (fun (q : ((T4 × T4) × ((initial rho lam eps kappaM).SurvivingCoordinate → T4)) × (leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4) => leftOutgoing.outgoingEndpointDefectDensity (leftData.incomingExceptionalRefinedRootOutgoingPostCoefficient leftOutgoing alpha beta pi q.1) alpha beta 0 q.2.1 q.2.2) (((paperMeasure.prod paperMeasure).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaM).SurvivingCoordinate) => paperMeasure)).prod ((MeasureTheory.Measure.pi fun (x : leftOutgoing.terminalPost.SurvivingCoordinate) => paperMeasure).prod paperMeasure))) : have muLeft := MeasureTheory.Measure.pi fun (x : leftOutgoing.terminalPost.SurvivingCoordinate) => paperMeasure; have muU := muLeft.prod paperMeasure; have muRight := MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaM).SurvivingCoordinate) => paperMeasure; MeasureTheory.Integrable (rightData.incomingExceptionalInitialSourceDensity (-alpha) (fun (omega : T4 × (leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4) => omega.1) fun (omega : T4 × (leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4) (post : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).SurvivingCoordinate → T4) => charT4 (-beta) omega.1 * leftData.eeeeRightPostCoefficient leftOutgoing rightOutgoing pi alpha beta omega.2 ((rightOutgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv rightOutgoing.terminalData.terminal [] ⋯) (rightOutgoing.endpoint.projection post)).2) ((paperMeasure.prod (paperMeasure.prod muU)).prod muRight) ∧ ∫ (s : (T4 × T4) × ((initial rho lam eps kappaM).SurvivingCoordinate → T4)), ∫ (v : leftOutgoing.terminalPost.SurvivingCoordinate → T4), ∫ (first : T4), leftOutgoing.outgoingEndpointDefectDensity (leftData.incomingExceptionalRefinedRootOutgoingPostCoefficient leftOutgoing alpha beta pi s) alpha beta 0 v first ∂paperMeasure ∂muLeft ∂(paperMeasure.prod paperMeasure).prod muRight = ∫ (p : (T4 × T4 × (leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4) × ((initial rho lam eps kappaM).SurvivingCoordinate → T4)), rightData.incomingExceptionalInitialSourceDensity (-alpha) (fun (omega : T4 × (leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4) => omega.1) (fun (omega : T4 × (leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4) (post : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).SurvivingCoordinate → T4) => charT4 (-beta) omega.1 * leftData.eeeeRightPostCoefficient leftOutgoing rightOutgoing pi alpha beta omega.2 ((rightOutgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv rightOutgoing.terminalData.terminal [] ⋯) (rightOutgoing.endpoint.projection post)).2) p ∂(paperMeasure.prod (paperMeasure.prod muU)).prod muRight

The completed left exceptional endpoint carrier is exactly the untouched parameter carrier required by the right parameterized EE theorem. This is only a reassociation of product measure, followed by the pointwise signed identity above; in particular, it takes no norm and loses no cancellation.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_twoHalfPhysical_eq_eeeeFinalRaw_of_regroupedCollapse {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftData : R324IncomingExceptionalStopTraceAssembly kappaP leftScale) (leftOutgoing : (leftData.trace.stopPrefix.afterHead leftData.terminal leftData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (rightData : R324IncomingExceptionalStopTraceAssembly kappaM rightScale) (rightOutgoing : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (alpha beta : Z4) (physical : ℂ) (hm : 0 < m) (hG : ∀ (j : Fin (2 * residualBlockOrder rightData.stopContext.step.2 - 1)), MemEClassT4 (rightData.stopContext.internalEdges j)) (hincoming : ∀ (gap first : T4) (kappaB : ↥(primitiveFullPairings (residualBlockOrder rightData.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder rightData.terminal.2 - 2) → T4) => detJclosedIntegrandWith rho eps (2 * residualBlockOrder rightData.terminal.2) (↑kappaB) rightData.stopContext.internalEdges (primitiveAssemble (residualBlockOrder rightData.terminal.2) ⋯ first (first + gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder rightData.terminal.2 - 2)) => paperMeasure)) (hcurrent : MeasureTheory.Integrable (leftData.eeeeRightInitialSourceDensity leftOutgoing rightData rightOutgoing pi alpha beta) ((paperMeasure.prod (paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : leftOutgoing.terminalPost.SurvivingCoordinate) => paperMeasure).prod paperMeasure))).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaM).SurvivingCoordinate) => paperMeasure))) (hsource : MeasureTheory.Integrable (leftData.eeeeRightStopSourceDensity leftOutgoing rightData rightOutgoing pi alpha beta) ((paperMeasure.prod (paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : leftOutgoing.terminalPost.SurvivingCoordinate) => paperMeasure).prod paperMeasure))).prod (MeasureTheory.Measure.pi fun (x : rightData.trace.stopPrefix.SurvivingCoordinate) => paperMeasure))) (hpred : r324WithinHalfPredecessorSlot rightOutgoing.endpoint.stop.state rightOutgoing.terminalData.terminal ≠ 0) (hactive : rightOutgoing.terminalPost.state.active.Nonempty) (hendpoint : MeasureTheory.Integrable (leftData.eeeeRightEndpointIntegrand leftOutgoing rightData rightOutgoing pi alpha beta) ((paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : leftOutgoing.terminalPost.SurvivingCoordinate) => paperMeasure).prod paperMeasure)).prod (MeasureTheory.Measure.pi fun (x : rightOutgoing.endpoint.stop.SurvivingCoordinate) => paperMeasure))) (houtgoing : ∀ (gap first : T4) (kappaB : ↥(primitiveFullPairings (residualBlockOrder rightOutgoing.terminalData.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder rightOutgoing.terminalData.terminal.2 - 2) → T4) => detJclosedIntegrandWith rho eps (2 * residualBlockOrder rightOutgoing.terminalData.terminal.2) (↑kappaB) rightOutgoing.terminalContext.internalEdges (primitiveAssemble (residualBlockOrder rightOutgoing.terminalData.terminal.2) ⋯ first (first - gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder rightOutgoing.terminalData.terminal.2 - 2)) => paperMeasure)) (hleftCollapse : ↑(lamEps lam eps) ^ (2 * (initial rho lam eps kappaP).remainingOrder) * physical = ∫ (p : (T4 × T4 × (leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4) × ((initial rho lam eps kappaM).SurvivingCoordinate → T4)), leftData.eeeeRightInitialSourceDensity leftOutgoing rightData rightOutgoing pi alpha beta p ∂(paperMeasure.prod (paperMeasure.prod ((MeasureTheory.Measure.pi fun (x : leftOutgoing.terminalPost.SurvivingCoordinate) => paperMeasure).prod paperMeasure))).prod (MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaM).SurvivingCoordinate) => paperMeasure)) : ↑(lamEps lam eps) ^ (2 * ((initial rho lam eps kappaP).remainingOrder + (initial rho lam eps kappaM).remainingOrder)) * physical = ∫ (u : (leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4), ∫ (v : rightOutgoing.terminalPost.SurvivingCoordinate → T4), ∫ (first : T4), leftData.eeeeFinalRawEndpointDensity leftOutgoing rightData rightOutgoing pi alpha beta u v first ∂paperMeasure ∂MeasureTheory.Measure.pi fun (x : rightOutgoing.terminalPost.SurvivingCoordinate) => paperMeasure ∂(MeasureTheory.Measure.pi fun (x : leftOutgoing.terminalPost.SurvivingCoordinate) => paperMeasure).prod paperMeasure

Second half of the exact EE x EE splice. The first-half collapse and the product-measure reassociation are summarized by hleftCollapse; the right parameterized EE theorem is then applied literally with modes -alpha,-beta. This is the paper's four signed endpoint operations, with the norm still postponed.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_twoHalfPhysical_eq_eeeeNested_of_raw {rho : SmoothCutoff} {C lam eps K : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftScale rightScale : Fin (m + 1) → ℝ} (leftData : R324IncomingExceptionalStopTraceAssembly kappaP leftScale) (leftOutgoing : (leftData.trace.stopPrefix.afterHead leftData.terminal leftData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (rightData : R324IncomingExceptionalStopTraceAssembly kappaM rightScale) (rightOutgoing : (rightData.trace.stopPrefix.afterHead rightData.terminal rightData.suffix ⋯).R324PaperOutgoingEndpointTerminal) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (alpha beta : Z4) (physical : ℂ) (hrawCollapse : ↑(lamEps lam eps) ^ (2 * ((initial rho lam eps kappaP).remainingOrder + (initial rho lam eps kappaM).remainingOrder)) * physical = ∫ (u : (leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4), ∫ (v : rightOutgoing.terminalPost.SurvivingCoordinate → T4), ∫ (first : T4), leftData.eeeeFinalRawEndpointDensity leftOutgoing rightData rightOutgoing pi alpha beta u v first ∂paperMeasure ∂MeasureTheory.Measure.pi fun (x : rightOutgoing.terminalPost.SurvivingCoordinate) => paperMeasure ∂(MeasureTheory.Measure.pi fun (x : leftOutgoing.terminalPost.SurvivingCoordinate) => paperMeasure).prod paperMeasure) (hraw : MeasureTheory.Integrable (fun (q : (((leftOutgoing.terminalPost.SurvivingCoordinate → T4) × T4) × (rightOutgoing.terminalPost.SurvivingCoordinate → T4)) × T4) => leftData.eeeeFinalRawEndpointDensity leftOutgoing rightData rightOutgoing pi alpha beta q.1.1 q.1.2 q.2) (leftData.eeeeFinalRawEndpointMeasure leftOutgoing rightData rightOutgoing)) : ↑(lamEps lam eps) ^ (2 * ((initial rho lam eps kappaP).remainingOrder + (initial rho lam eps kappaM).remainingOrder)) * physical = ∫ (v : (leftData.eeeeTerminalData leftOutgoing rightData rightOutgoing).NestedCoordinate pi → T4), leftData.eeeeNestedEndpointDensity leftOutgoing rightData rightOutgoing pi alpha beta v ∂MeasureTheory.Measure.pi fun (x : (leftData.eeeeTerminalData leftOutgoing rightData rightOutgoing).NestedCoordinate pi) => paperMeasure

Package the exact four-endpoint output on the nested carrier expected by the common weighted-majorant exit.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalExceptionalRoute.terminalPost_active_of_singles {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalExceptionalRoute providers) (hsingles : pairing.singles.Nonempty) : data.outgoing.terminalPost.state.active.Nonempty

A surviving single is the literal post-terminal interior of an EE half. This just exposes the geometric fact already used by the route constructor.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalExceptionalRoute.predecessor_ne_zero_of_singles {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalExceptionalRoute providers) (hsingles : pairing.singles.Nonempty) : r324WithinHalfPredecessorSlot data.outgoing.endpoint.stop.state data.outgoing.terminalData.terminal ≠ 0

The retained outgoing exceptional block has a genuine internal predecessor whenever the half has a surviving single.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalExceptionalRoute.stopBudgetCertificate {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalExceptionalRoute providers) : R324WithinHalfEdgeCertificate data.outgoing.terminalContext.state data.endpoint.stopBudgetScale

The synchronized pre-terminal budget is the certificate used by the retained exceptional outgoing estimate.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalExceptionalRoute.outgoingProp41 {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalExceptionalRoute providers) (H : Fin (2 * residualBlockOrder data.outgoing.terminalData.terminal.2 - 1) → T4 → ℝ) : IsAdmissiblePrimitiveInput (residualBlockOrder data.outgoing.terminalData.terminal.2) H → MemEClassT4 (primitiveKernelDiff rho lam eps (residualBlockOrder data.outgoing.terminalData.terminal.2) ⋯ H) ∧ MemEClassT4 (primitiveKernelInsertedDiff rho lam eps (residualBlockOrder data.outgoing.terminalData.terminal.2) ⋯ H) ∧ PrimitiveKernelBounds rho lam eps (residualBlockOrder data.outgoing.terminalData.terminal.2) ⋯ H providers.supportConstant C

Proposition 4.1 specialized to the retained outgoing block of an exceptional/exceptional half.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalExceptionalRoute.incomingErasedHeadOuterFactor_eq_terminalPost_endpointErasedSignedChain {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalExceptionalRoute providers) (hpred : r324WithinHalfPredecessorSlot data.outgoing.endpoint.stop.state data.outgoing.terminalData.terminal ≠ 0) (hactive : data.outgoing.terminalPost.state.active.Nonempty) (x y : T4) (v : data.outgoing.terminalPost.SurvivingCoordinate → T4) : data.outgoing.endpoint.stop.incomingErasedHeadOuterFactor data.outgoing.terminalData.terminal [] ⋯ rho eps x y v = data.outgoing.terminalPost.endpointErasedSignedChain hactive x y (data.outgoing.terminalPost.reconstruct v)

On the completed EE half, the outer chain left by the retained terminal is exactly the endpoint-erased post-terminal chain.

def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalExceptionalRoute.postBudgetScale {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalExceptionalRoute providers) : Fin (m + 1) → ℝ

The literal complete-budget scale after consuming the retained outgoing terminal.

Equations

• data.postBudgetScale = data.endpoint.endpoint.stop.budgetUpdatedEdgeScale data.terminalData.terminal [] ⋯ data.endpoint.stopBudgetScale C lam K

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalExceptionalRoute.postBudgetReachable {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalExceptionalRoute providers) : R324WithinHalfBudgetScaleReachable pairing rho C lam eps K A data.outgoing.terminalPost.state data.postBudgetScale

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalExceptionalRoute.postBudgetCertificate {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalExceptionalRoute providers) : R324WithinHalfEdgeCertificate data.outgoing.terminalPost.state data.postBudgetScale

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalExceptionalRoute.postBudget_activeProduct_eq_route {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalExceptionalRoute providers) : ∏ edge ∈ data.outgoing.terminalPost.activeEdgeSlots, data.postBudgetScale edge = ∏ edge ∈ data.outgoing.terminalPost.activeEdgeSlots, data.route.terminalScale edge

Any completed route scale and the literal outgoing update have the same active product, since both are complete budget histories on the same final paper state.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalExceptionalRoute.postBudgetScale_zero_eq_stopBudget {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalExceptionalRoute providers) (hpred : r324WithinHalfPredecessorSlot data.outgoing.endpoint.stop.state data.outgoing.terminalData.terminal ≠ 0) : data.postBudgetScale 0 = data.endpoint.stopBudgetScale 0

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalExceptionalRoute.outgoingBudgetCore_le_postBudget_outgoingScale {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalExceptionalRoute providers) (hpred : r324WithinHalfPredecessorSlot data.outgoing.endpoint.stop.state data.outgoing.terminalData.terminal ≠ 0) (hactive : data.outgoing.terminalPost.state.active.Nonempty) : data.endpoint.stopBudgetScale (r324WithinHalfPredecessorSlot data.outgoing.terminalContext.state data.outgoing.terminalContext.step) * r324WithinHalfInternalEdgeScaleProduct data.outgoing.terminalContext data.endpoint.stopBudgetScale * (C * lam) ^ (2 * residualBlockOrder data.outgoing.terminalData.terminal.2) * K ≤ data.postBudgetScale (data.outgoing.terminalPost.terminalOutgoingEdgeSlot hactive)

The outgoing local block charge is one boundary scale of the completed post-terminal budget.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalExceptionalRoute.boundaryCore_mul_endpointErasedScale_le_routeActiveProduct {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalExceptionalRoute providers) (hpred : r324WithinHalfPredecessorSlot data.outgoing.endpoint.stop.state data.outgoing.terminalData.terminal ≠ 0) (hactive : data.outgoing.terminalPost.state.active.Nonempty) : data.endpoint.stopBudgetScale 0 * (data.endpoint.stopBudgetScale (r324WithinHalfPredecessorSlot data.outgoing.terminalContext.state data.outgoing.terminalContext.step) * r324WithinHalfInternalEdgeScaleProduct data.outgoing.terminalContext data.endpoint.stopBudgetScale * (C * lam) ^ (2 * residualBlockOrder data.outgoing.terminalData.terminal.2) * K) * data.outgoing.terminalPost.endpointErasedScaleProduct hactive data.postBudgetScale ≤ ∏ edge ∈ data.outgoing.terminalPost.activeEdgeSlots, data.route.terminalScale edge

The two boundary charges and the erased post chain fit inside the full completed route scale product.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalExceptionalRoute.norm_terminalSplitOuter_le_postBudgetMajorant {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalExceptionalRoute providers) (hpred : r324WithinHalfPredecessorSlot data.outgoing.endpoint.stop.state data.outgoing.terminalData.terminal ≠ 0) (hactive : data.outgoing.terminalPost.state.active.Nonempty) (coefficient : (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ) (x : T4) (v : data.outgoing.terminalPost.SurvivingCoordinate → T4) (hne : ∀ edge ∈ data.outgoing.terminalPost.endpointErasedActiveEdgeSlots hactive, data.outgoing.terminalPost.edgeDisplacement 0 0 (data.outgoing.terminalPost.reconstruct v) edge ≠ 0) : ‖data.outgoing.terminalSplitOuter coefficient incomingMode x v‖ ≤ ‖coefficient v‖ * (data.outgoing.terminalPost.endpointErasedScaleProduct hactive data.postBudgetScale * data.outgoing.terminalPost.endpointErasedInvSqChainProduct hactive v)

The post-terminal erased chain is bounded by the literal updated budget scale on every off-diagonal configuration.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalExceptionalRoute.norm_integral_outgoingEndpointDefectDensity_le_inserted {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalExceptionalRoute providers) (coefficient : (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ) (outgoingMode : Z4) (x : T4) (v : data.outgoing.terminalPost.SurvivingCoordinate → T4) : ‖∫ (first : T4), data.outgoing.outgoingEndpointDefectDensity coefficient incomingMode outgoingMode x v first ∂paperMeasure‖ ≤ data.endpoint.stopBudgetScale (r324WithinHalfPredecessorSlot data.outgoing.terminalContext.state data.outgoing.terminalContext.step) * invSqKerMass * paperSecondOrderModeDecay outgoingMode * (2 * r324WithinHalfInternalEdgeScaleProduct data.outgoing.terminalContext data.endpoint.stopBudgetScale * (SmoothCutoff.r324EndpointPrimitiveSacrifice eps SmoothCutoff.R324EndpointReductionCase.insertedSacrifice * ∫ (gap : T4), primitiveInsertedMajorant C lam eps providers.supportConstant (residualBlockOrder data.outgoing.terminalData.terminal.2) gap ∂paperMeasure)) * ‖data.outgoing.terminalSplitOuter coefficient incomingMode x v‖

Literal exceptional outgoing estimate, still in the pre-terminal budget currency and with exactly one endpoint sacrifice.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalExceptionalRoute.norm_integral_outgoingEndpointDefectDensity_le_budgeted {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalExceptionalRoute providers) (coefficient : (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ) (outgoingMode : Z4) (x : T4) (v : data.outgoing.terminalPost.SurvivingCoordinate → T4) : ‖∫ (first : T4), data.outgoing.outgoingEndpointDefectDensity coefficient incomingMode outgoingMode x v first ∂paperMeasure‖ ≤ data.endpoint.stopBudgetScale (r324WithinHalfPredecessorSlot data.outgoing.terminalContext.state data.outgoing.terminalContext.step) * invSqKerMass * paperSecondOrderModeDecay outgoingMode * (r324WithinHalfInternalEdgeScaleProduct data.outgoing.terminalContext data.endpoint.stopBudgetScale * (SmoothCutoff.r324EndpointPrimitiveSacrifice eps SmoothCutoff.R324EndpointReductionCase.insertedSacrifice * ((C * lam) ^ (2 * residualBlockOrder data.outgoing.terminalData.terminal.2) * K))) * ‖data.outgoing.terminalSplitOuter coefficient incomingMode x v‖

Pay the inserted outgoing integral with the same complete local block constant K. The endpoint sacrifice remains explicit.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalExceptionalRoute.incomingEndpointCoefficient {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalExceptionalRoute providers) (coefficient : (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ) (v : data.outgoing.terminalPost.SurvivingCoordinate → T4) : ℂ

The already-collapsed exceptional incoming endpoint, with an arbitrary post-terminal coefficient still attached.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalExceptionalRoute.norm_incomingEndpointCoefficient_le {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalExceptionalRoute providers) (coefficient : (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ) (v : data.outgoing.terminalPost.SurvivingCoordinate → T4) : ‖data.incomingEndpointCoefficient coefficient v‖ ≤ paperSecondOrderModeDecay incomingMode * data.endpoint.stopBudgetScale 0 * ‖coefficient v‖

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalExceptionalRoute.endpointDensity {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalExceptionalRoute providers) (coefficient : (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ) (outgoingMode : Z4) (x : T4) (v : data.outgoing.terminalPost.SurvivingCoordinate → T4) : ℂ

One complete exceptional/exceptional half after both signed endpoint operations, before any norm.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfExceptionalExceptionalRoute.norm_endpointDensity_le {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (data : R324PaperHalfExceptionalExceptionalRoute providers) (hpred : r324WithinHalfPredecessorSlot data.outgoing.endpoint.stop.state data.outgoing.terminalData.terminal ≠ 0) (hactive : data.outgoing.terminalPost.state.active.Nonempty) (coefficient : (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ) (outgoingMode : Z4) (x : T4) (v : data.outgoing.terminalPost.SurvivingCoordinate → T4) (hne : ∀ edge ∈ data.outgoing.terminalPost.endpointErasedActiveEdgeSlots hactive, data.outgoing.terminalPost.edgeDisplacement 0 0 (data.outgoing.terminalPost.reconstruct v) edge ≠ 0) : ‖data.endpointDensity coefficient outgoingMode x v‖ ≤ paperSecondOrderModeDecay incomingMode * paperSecondOrderModeDecay outgoingMode * (SmoothCutoff.r324EndpointPrimitiveSacrifice eps SmoothCutoff.R324EndpointReductionCase.insertedSacrifice * SmoothCutoff.r324EndpointPrimitiveSacrifice eps SmoothCutoff.R324EndpointReductionCase.insertedSacrifice) * ((∏ edge ∈ data.outgoing.terminalPost.activeEdgeSlots, data.route.terminalScale edge) * invSqKerMass) * data.outgoing.terminalPost.endpointErasedInvSqChainProduct hactive v * ‖coefficient v‖

Pointwise numerical exit of one literal EE half. Both signed endpoint operations have already been completed. The incoming endpoint sacrifice is introduced only as the final case-ledger enlargement.

Literal EE × EE factorization after all four endpoint operations

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.eeeeCrossCoefficient {rho : SmoothCutoff} {C K A lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha : Z4} {leftEEProviders : R324PaperHalfRouteProviders kappaP alpha} {rightEEProviders : R324PaperHalfRouteProviders kappaM (-alpha)} (leftEE : R324PaperHalfExceptionalExceptionalRoute leftEEProviders) (rightEE : R324PaperHalfExceptionalExceptionalRoute rightEEProviders) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (leftPost : leftEE.outgoing.terminalPost.SurvivingCoordinate → T4) (rightPost : rightEE.outgoing.terminalPost.SurvivingCoordinate → T4) : ℂ

The cross primitive sum left untouched by the four endpoint Fourier operations.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.eeeeFinalRawEndpointDensity_eq_endpointFactors {rho : SmoothCutoff} {C K A lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha beta : Z4} {leftEEProviders : R324PaperHalfRouteProviders kappaP alpha} {rightEEProviders : R324PaperHalfRouteProviders kappaM (-alpha)} (leftEE : R324PaperHalfExceptionalExceptionalRoute leftEEProviders) (rightEE : R324PaperHalfExceptionalExceptionalRoute rightEEProviders) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (leftPost : leftEE.outgoing.terminalPost.SurvivingCoordinate → T4) (firstLeft : T4) (rightPost : rightEE.outgoing.terminalPost.SurvivingCoordinate → T4) (firstRight : T4) : leftEE.pack.data.eeeeFinalRawEndpointDensity leftEE.outgoing rightEE.pack.data rightEE.outgoing pi alpha beta (leftPost, firstLeft) rightPost firstRight = leftEE.outgoing.outgoingEndpointDefectDensity (leftEE.incomingEndpointCoefficient fun (x : leftEE.outgoing.terminalPost.SurvivingCoordinate → T4) => 1) alpha beta 0 leftPost firstLeft * rightEE.outgoing.outgoingEndpointDefectDensity (rightEE.incomingEndpointCoefficient (eeeeCrossCoefficient leftEE rightEE pi leftPost)) (-alpha) (-beta) 0 rightPost firstRight

Pointwise, before taking any norm, the final raw four-endpoint density is the product of the two completed signed half densities.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.eeeeNestedEndpointDensity_eq_endpointDensity_mul {rho : SmoothCutoff} {C K A lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha beta : Z4} {leftEEProviders : R324PaperHalfRouteProviders kappaP alpha} {rightEEProviders : R324PaperHalfRouteProviders kappaM (-alpha)} (leftEE : R324PaperHalfExceptionalExceptionalRoute leftEEProviders) (rightEE : R324PaperHalfExceptionalExceptionalRoute rightEEProviders) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (v : (leftEE.pack.data.eeeeTerminalData leftEE.outgoing rightEE.pack.data rightEE.outgoing).NestedCoordinate pi → T4) : let terminal := leftEE.pack.data.eeeeTerminalData leftEE.outgoing rightEE.pack.data rightEE.outgoing; have p := (terminal.terminalProductPiMeasurableEquivNested pi).symm v; leftEE.pack.data.eeeeNestedEndpointDensity leftEE.outgoing rightEE.pack.data rightEE.outgoing pi alpha beta v = leftEE.endpointDensity (fun (x : leftEE.outgoing.terminalPost.SurvivingCoordinate → T4) => 1) beta 0 p.1 * rightEE.endpointDensity (eeeeCrossCoefficient leftEE rightEE pi p.1) (-beta) 0 p.2

Exact Fubini factorization on the common nested carrier. This is the paper's instruction to finish all interval removals and endpoint operations before taking absolute values, written literally.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.norm_endpointDensity_mul_endpointDensity_le_massTwoGrouped {rho : SmoothCutoff} {C K A lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha beta : Z4} {leftEEProviders : R324PaperHalfRouteProviders kappaP alpha} {rightEEProviders : R324PaperHalfRouteProviders kappaM (-alpha)} (leftEE : R324PaperHalfExceptionalExceptionalRoute leftEEProviders) (rightEE : R324PaperHalfExceptionalExceptionalRoute rightEEProviders) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (hleftPred : r324WithinHalfPredecessorSlot leftEE.outgoing.endpoint.stop.state leftEE.outgoing.terminalData.terminal ≠ 0) (hrightPred : r324WithinHalfPredecessorSlot rightEE.outgoing.endpoint.stop.state rightEE.outgoing.terminalData.terminal ≠ 0) (hleft : leftEE.outgoing.terminalPost.state.active.Nonempty) (hright : rightEE.outgoing.terminalPost.state.active.Nonempty) (leftPost : leftEE.outgoing.terminalPost.SurvivingCoordinate → T4) (rightPost : rightEE.outgoing.terminalPost.SurvivingCoordinate → T4) (hneLeft : ∀ edge ∈ leftEE.outgoing.terminalPost.endpointErasedActiveEdgeSlots hleft, leftEE.outgoing.terminalPost.edgeDisplacement 0 0 (leftEE.outgoing.terminalPost.reconstruct leftPost) edge ≠ 0) (hneRight : ∀ edge ∈ rightEE.outgoing.terminalPost.endpointErasedActiveEdgeSlots hright, rightEE.outgoing.terminalPost.edgeDisplacement 0 0 (rightEE.outgoing.terminalPost.reconstruct rightPost) edge ≠ 0) : ‖leftEE.endpointDensity (fun (x : leftEE.outgoing.terminalPost.SurvivingCoordinate → T4) => 1) beta 0 leftPost * rightEE.endpointDensity (eeeeCrossCoefficient leftEE rightEE pi leftPost) (-beta) 0 rightPost‖ ≤ (paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * SmoothCutoff.r324EndpointPrimitiveSacrificeProduct eps fun (x : Fin 4) => SmoothCutoff.R324EndpointReductionCase.insertedSacrifice) * (((∏ edge ∈ leftEE.outgoing.terminalPost.activeEdgeSlots, leftEE.route.terminalScale edge) * ∏ edge ∈ rightEE.outgoing.terminalPost.activeEdgeSlots, rightEE.route.terminalScale edge) * invSqKerMass ^ 2 * leftEE.outgoing.terminalPost.endpointErasedInvSqChainProduct hleft leftPost * rightEE.outgoing.terminalPost.endpointErasedInvSqChainProduct hright rightPost * r324ResidualPrimitiveSumProduct rho eps kappaP kappaM pi (r324TwoHalfRootDoubledReconstruct leftEE.outgoing.terminalPost rightEE.outgoing.terminalPost (leftPost, rightPost)))

Pointwise numerical form of the literal EE × EE factorization. The four endpoint operations contribute the two fourth-order mode decays, four inserted-primitive sacrifices, and two explicit inverse-square masses. No norm was taken before the exact factorization above.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.eeeeEndpointMassCompensation : ℝ

Fixed compensation for the two artificial inverse-square masses in the common grouped Step 3 carrier that are not produced by a literal EE × EE endpoint calculation. This is an order-independent paper constant.

Equations

• Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.eeeeEndpointMassCompensation = max 1 (Anderson4D.invSqKerMass⁻¹ ^ 2)

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.one_le_eeeeEndpointMassCompensation : 1 ≤ eeeeEndpointMassCompensation

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.invSqKerMass_sq_le_compensation_mul_pow_four : invSqKerMass ^ 2 ≤ eeeeEndpointMassCompensation * invSqKerMass ^ 4

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.norm_endpointDensity_mul_endpointDensity_le_compensatedGrouped {rho : SmoothCutoff} {C K A lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha beta : Z4} {leftEEProviders : R324PaperHalfRouteProviders kappaP alpha} {rightEEProviders : R324PaperHalfRouteProviders kappaM (-alpha)} (leftEE : R324PaperHalfExceptionalExceptionalRoute leftEEProviders) (rightEE : R324PaperHalfExceptionalExceptionalRoute rightEEProviders) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (hleftPred : r324WithinHalfPredecessorSlot leftEE.outgoing.endpoint.stop.state leftEE.outgoing.terminalData.terminal ≠ 0) (hrightPred : r324WithinHalfPredecessorSlot rightEE.outgoing.endpoint.stop.state rightEE.outgoing.terminalData.terminal ≠ 0) (hleft : leftEE.outgoing.terminalPost.state.active.Nonempty) (hright : rightEE.outgoing.terminalPost.state.active.Nonempty) (leftPost : leftEE.outgoing.terminalPost.SurvivingCoordinate → T4) (rightPost : rightEE.outgoing.terminalPost.SurvivingCoordinate → T4) (hneLeft : ∀ edge ∈ leftEE.outgoing.terminalPost.endpointErasedActiveEdgeSlots hleft, leftEE.outgoing.terminalPost.edgeDisplacement 0 0 (leftEE.outgoing.terminalPost.reconstruct leftPost) edge ≠ 0) (hneRight : ∀ edge ∈ rightEE.outgoing.terminalPost.endpointErasedActiveEdgeSlots hright, rightEE.outgoing.terminalPost.edgeDisplacement 0 0 (rightEE.outgoing.terminalPost.reconstruct rightPost) edge ≠ 0) : ‖leftEE.endpointDensity (fun (x : leftEE.outgoing.terminalPost.SurvivingCoordinate → T4) => 1) beta 0 leftPost * rightEE.endpointDensity (eeeeCrossCoefficient leftEE rightEE pi leftPost) (-beta) 0 rightPost‖ ≤ eeeeEndpointMassCompensation * (paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * SmoothCutoff.r324EndpointPrimitiveSacrificeProduct eps fun (x : Fin 4) => SmoothCutoff.R324EndpointReductionCase.insertedSacrifice) * (leftEE.pack.data.eeeeTerminalData leftEE.outgoing rightEE.pack.data rightEE.outgoing).endpointIntegratedGroupedMajorant leftEE.route.terminalScale rightEE.route.terminalScale hleft hright pi (leftPost, rightPost)

The literal EE × EE estimate in the common grouped Step 3 currency. The sole conversion is the fixed mass compensation above.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.ae_norm_eeeeNestedEndpointDensity_le_compensatedGrouped {rho : SmoothCutoff} {C K A lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {alpha beta : Z4} {leftEEProviders : R324PaperHalfRouteProviders kappaP alpha} {rightEEProviders : R324PaperHalfRouteProviders kappaM (-alpha)} (leftEE : R324PaperHalfExceptionalExceptionalRoute leftEEProviders) (rightEE : R324PaperHalfExceptionalExceptionalRoute rightEEProviders) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (hleftPred : r324WithinHalfPredecessorSlot leftEE.outgoing.endpoint.stop.state leftEE.outgoing.terminalData.terminal ≠ 0) (hrightPred : r324WithinHalfPredecessorSlot rightEE.outgoing.endpoint.stop.state rightEE.outgoing.terminalData.terminal ≠ 0) (hleft : leftEE.outgoing.terminalPost.state.active.Nonempty) (hright : rightEE.outgoing.terminalPost.state.active.Nonempty) : let terminal := leftEE.pack.data.eeeeTerminalData leftEE.outgoing rightEE.pack.data rightEE.outgoing; (fun (v : terminal.NestedCoordinate pi → T4) => ‖leftEE.pack.data.eeeeNestedEndpointDensity leftEE.outgoing rightEE.pack.data rightEE.outgoing pi alpha beta v‖) ≤ᵐ[MeasureTheory.Measure.pi fun (x : terminal.NestedCoordinate pi) => paperMeasure] fun (v : terminal.NestedCoordinate pi → T4) => eeeeEndpointMassCompensation * (paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * SmoothCutoff.r324EndpointPrimitiveSacrificeProduct eps fun (x : Fin 4) => SmoothCutoff.R324EndpointReductionCase.insertedSacrifice) * terminal.initialNestedEndpointIntegratedGroupedMajorant leftEE.route.terminalScale rightEE.route.terminalScale hleft hright pi v

Product-Haar and initial-nested form of the completed literal EE × EE endpoint estimate.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.eeeeEndpointCompleteAbsorbedBase (A C K B : ℝ) : ℝ

Final complete-run base for the EE × EE branch. It differs from the common two-half base only by the fixed endpoint-mass compensation.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.eeeeEndpointCompleteAbsorbedBase_pos (A C K B : ℝ) : 0 < eeeeEndpointCompleteAbsorbedBase A C K B

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.compensation_mul_primitiveInsertedMajorant_le (B lam eps supportConstant : ℝ) {n : ℕ} (hn : 1 ≤ n) (z : T4) : eeeeEndpointMassCompensation * primitiveInsertedMajorant B lam eps supportConstant n z ≤ primitiveInsertedMajorant (eeeeEndpointMassCompensation * B) lam eps supportConstant n z

At every positive perturbative order, the fixed mass compensation is absorbed by multiplying the primitive base once.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.compensation_mul_integral_primitiveInsertedMajorant_le (B lam : ℝ) {eps : ℝ} (heps : 0 < eps) (supportConstant : ℝ) {n : ℕ} (hn : 1 ≤ n) : eeeeEndpointMassCompensation * ∫ (z : T4), primitiveInsertedMajorant B lam eps supportConstant n z ∂paperMeasure ≤ ∫ (z : T4), primitiveInsertedMajorant (eeeeEndpointMassCompensation * B) lam eps supportConstant n z ∂paperMeasure

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.compensation_mul_integral_completeAbsorbed_le (A C K B lam : ℝ) {eps : ℝ} (heps : 0 < eps) (supportConstant : ℝ) {m : ℕ} (hm : 1 ≤ m) : eeeeEndpointMassCompensation * ∫ (z : T4), primitiveInsertedMajorant (r324TwoHalfCompleteAbsorbedBase A C K B) lam eps supportConstant m z ∂paperMeasure ≤ ∫ (z : T4), primitiveInsertedMajorant (eeeeEndpointCompleteAbsorbedBase A C K B) lam eps supportConstant m z ∂paperMeasure

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.terminal_exceptionalExceptional_exceptionalExceptional_eq_eeeeTerminalData {rho : SmoothCutoff} {C K A lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftMode rightMode : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP leftMode} {rightProviders : R324PaperHalfRouteProviders kappaM rightMode} (hleftFirst : ⟨0, ⋯⟩ ∉ finalActive kappaP) (hleftOutgoing : Fin.last m ∈ extractedRightEdges kappaP) (leftEE : R324PaperHalfExceptionalExceptionalRoute leftProviders) (hrightFirst : ⟨0, ⋯⟩ ∉ finalActive kappaM) (hrightOutgoing : Fin.last m ∈ extractedRightEdges kappaM) (rightEE : R324PaperHalfExceptionalExceptionalRoute rightProviders) : { left := R324PaperHalfEndpointRoute.exceptionalExceptional hleftFirst hleftOutgoing leftEE, right := R324PaperHalfEndpointRoute.exceptionalExceptional hrightFirst hrightOutgoing rightEE }.terminal = leftEE.pack.data.eeeeTerminalData leftEE.outgoing rightEE.pack.data rightEE.outgoing

In the literal EE x EE constructor branch, the common route terminal is exactly the two post-terminal carriers used by the signed splice above. This is the dependent-type seam between branch data and the common grouped majorant.

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.cases_exceptionalExceptional_exceptionalExceptional {rho : SmoothCutoff} {C K A lam eps : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftMode rightMode : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP leftMode} {rightProviders : R324PaperHalfRouteProviders kappaM rightMode} (hleftFirst : ⟨0, ⋯⟩ ∉ finalActive kappaP) (hleftOutgoing : Fin.last m ∈ extractedRightEdges kappaP) (leftEE : R324PaperHalfExceptionalExceptionalRoute leftProviders) (hrightFirst : ⟨0, ⋯⟩ ∉ finalActive kappaM) (hrightOutgoing : Fin.last m ∈ extractedRightEdges kappaM) (rightEE : R324PaperHalfExceptionalExceptionalRoute rightProviders) : { left := R324PaperHalfEndpointRoute.exceptionalExceptional hleftFirst hleftOutgoing leftEE, right := R324PaperHalfEndpointRoute.exceptionalExceptional hrightFirst hrightOutgoing rightEE }.cases = fun (x : Fin 4) => SmoothCutoff.R324EndpointReductionCase.insertedSacrifice

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.weighted_norm_le_endpointPatternAmbientMajorant_of_grouped {rho : SmoothCutoff} {C K A B lam eps supportConstant : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftMode rightMode : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP leftMode} {rightProviders : R324PaperHalfRouteProviders kappaM rightMode} (routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders) (hA : 0 ≤ A) (hC : 0 ≤ C) (hK : 0 ≤ K) (hB : 0 ≤ B) (hlam : 0 < lam) (hleft : routes.terminal.left.state.active.Nonempty) (hright : routes.terminal.right.state.active.Nonempty) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (head : R324NestedCrossBlock kappaP kappaM pi) (tail : List (R324NestedCrossBlock kappaP kappaM pi)) (hremaining : (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remaining = head :: tail) (alpha beta : Z4) (physical : ℂ) (endpointDensity : (routes.terminal.NestedCoordinate pi → T4) → ℂ) (hendpoint : (fun (v : routes.terminal.NestedCoordinate pi → T4) => ‖endpointDensity v‖) ≤ᵐ[MeasureTheory.Measure.pi fun (x : routes.terminal.NestedCoordinate pi) => paperMeasure] fun (v : routes.terminal.NestedCoordinate pi → T4) => paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * SmoothCutoff.r324EndpointPrimitiveSacrificeProduct eps routes.cases * routes.terminal.initialNestedEndpointIntegratedGroupedMajorant routes.left.completedRoute.terminalScale routes.right.completedRoute.terminalScale hleft hright pi v) (heps : 0 < eps) (heps1 : eps ≤ 1) (hlog : 1 ≤ |Real.log eps|) (hm : 1 ≤ m) (hmtrunc : m ≤ truncOrder eps) (hrunBound : let step := r324InitialNestedCrossStepContext kappaP kappaM pi head tail hremaining; have hleftInitial := ⋯; have hrightInitial := ⋯; (∫ (v : step.SurvivingCoordinate → T4), routes.terminal.completeNestedRunDensity step hleftInitial hrightInitial v ∂MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure) ≤ ∫ (z : T4), primitiveInsertedMajorant B lam eps supportConstant step.residual.remainingOrder z ∂paperMeasure) (horder : (initial rho lam eps kappaP).remainingOrder + (initial rho lam eps kappaM).remainingOrder + (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remainingOrder = m) (hcollapse : ↑(lamEps lam eps) ^ (2 * ((initial rho lam eps kappaP).remainingOrder + (initial rho lam eps kappaM).remainingOrder)) * physical = ∫ (v : routes.terminal.NestedCoordinate pi → T4), endpointDensity v ∂MeasureTheory.Measure.pi fun (x : routes.terminal.NestedCoordinate pi) => paperMeasure) : |lamEps lam eps| ^ (2 * m) * ‖physical‖ ≤ paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * (SmoothCutoff.r324EndpointPrimitiveSacrificeProduct eps routes.cases * ∫ (z : T4), primitiveInsertedMajorant (r324TwoHalfCompleteAbsorbedBase A C K B) lam eps supportConstant m z ∂paperMeasure)

Common numerical exit for any two literal endpoint routes. The only branch-specific inputs are the exact signed collapse hcollapse and the post-endpoint grouped domination hendpoint. All scale products, the remaining coupling power, and the complete nested run are consumed here.

This is deliberately stated for an arbitrary completed endpoint density; the EE x EE branch supplies that density by applying lamEps_pow_integral_initialResidual_eq_singleParameter_incomingExceptional_outgoingExceptional to the two halves in succession.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.weighted_norm_le_endpointPatternAmbientMajorant_of_grouped_compensated {rho : SmoothCutoff} {C K A B lam eps supportConstant : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftMode rightMode : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP leftMode} {rightProviders : R324PaperHalfRouteProviders kappaM rightMode} (routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders) (hA : 0 ≤ A) (hC : 0 ≤ C) (hK : 0 ≤ K) (hB : 0 ≤ B) (hlam : 0 < lam) (hleft : routes.terminal.left.state.active.Nonempty) (hright : routes.terminal.right.state.active.Nonempty) (pi : ↥kappaP.singles ≃ ↥kappaM.singles) (head : R324NestedCrossBlock kappaP kappaM pi) (tail : List (R324NestedCrossBlock kappaP kappaM pi)) (hremaining : (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remaining = head :: tail) (alpha beta : Z4) (physical : ℂ) (endpointDensity : (routes.terminal.NestedCoordinate pi → T4) → ℂ) (hendpoint : (fun (v : routes.terminal.NestedCoordinate pi → T4) => ‖endpointDensity v‖) ≤ᵐ[MeasureTheory.Measure.pi fun (x : routes.terminal.NestedCoordinate pi) => paperMeasure] fun (v : routes.terminal.NestedCoordinate pi → T4) => eeeeEndpointMassCompensation * (paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * SmoothCutoff.r324EndpointPrimitiveSacrificeProduct eps routes.cases) * routes.terminal.initialNestedEndpointIntegratedGroupedMajorant routes.left.completedRoute.terminalScale routes.right.completedRoute.terminalScale hleft hright pi v) (heps : 0 < eps) (heps1 : eps ≤ 1) (hlog : 1 ≤ |Real.log eps|) (hm : 1 ≤ m) (hmtrunc : m ≤ truncOrder eps) (hrunBound : let step := r324InitialNestedCrossStepContext kappaP kappaM pi head tail hremaining; have hleftInitial := ⋯; have hrightInitial := ⋯; (∫ (v : step.SurvivingCoordinate → T4), routes.terminal.completeNestedRunDensity step hleftInitial hrightInitial v ∂MeasureTheory.Measure.pi fun (x : step.SurvivingCoordinate) => paperMeasure) ≤ ∫ (z : T4), primitiveInsertedMajorant B lam eps supportConstant step.residual.remainingOrder z ∂paperMeasure) (horder : (initial rho lam eps kappaP).remainingOrder + (initial rho lam eps kappaM).remainingOrder + (R324NestedCrossResidualPrefix.initial kappaP kappaM pi).remainingOrder = m) (hcollapse : ↑(lamEps lam eps) ^ (2 * ((initial rho lam eps kappaP).remainingOrder + (initial rho lam eps kappaM).remainingOrder)) * physical = ∫ (v : routes.terminal.NestedCoordinate pi → T4), endpointDensity v ∂MeasureTheory.Measure.pi fun (x : routes.terminal.NestedCoordinate pi) => paperMeasure) : |lamEps lam eps| ^ (2 * m) * ‖physical‖ ≤ paperFourthOrderModeDecay alpha * paperFourthOrderModeDecay beta * (SmoothCutoff.r324EndpointPrimitiveSacrificeProduct eps routes.cases * ∫ (z : T4), primitiveInsertedMajorant (eeeeEndpointCompleteAbsorbedBase A C K B) lam eps supportConstant m z ∂paperMeasure)

Common numerical exit when an endpoint branch reaches the grouped carrier with the fixed EE × EE mass compensation. The compensation is immediately absorbed into the final primitive base.