Paper Step 4(A): outgoing-gap Fubini and endpoint-free outer factor

This module supplies the two exact coordinate facts needed after the retained outgoing terminal has been split from an arbitrary endpoint stop.

• The existing primitive-head gap reindex is turned from last = first + gap into the outgoing paper orientation last = first - gap, and ordered with first outermost.
• Once the terminal is removed and a residual single remains, the phased split factor outside the terminal head is independent of the outgoing endpoint variable.

Only measure-preserving changes of variables and sparse-chain geometry are used. No norm or estimate occurs.

The paper's outgoing (first, gap, internal) coordinates

noncomputable def Anderson4D.r324EndpointFirstOutgoingGapMeasurableEquiv : T4 × T4 ≃ᵐ T4 × T4

On endpoint pairs, change (first,last) to (first, first - last). This is the existing gap-first shear followed by negation of the gap and a swap; it introduces no new coordinate analysis.

Equations

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

@[simp]

theorem Anderson4D.r324EndpointFirstOutgoingGapMeasurableEquiv_apply (first last : T4) : r324EndpointFirstOutgoingGapMeasurableEquiv (first, last) = (first, first - last)

@[simp]

theorem Anderson4D.r324EndpointFirstOutgoingGapMeasurableEquiv_symm_apply (first gap : T4) : r324EndpointFirstOutgoingGapMeasurableEquiv.symm (first, gap) = (first, first - gap)

theorem Anderson4D.measurePreserving_r324NegT4 : MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.neg T4)) paperMeasure paperMeasure

Negation preserves the paper Haar measure on the four-torus.

theorem Anderson4D.measurePreserving_r324EndpointFirstOutgoingGapMeasurableEquiv : MeasureTheory.MeasurePreserving (⇑r324EndpointFirstOutgoingGapMeasurableEquiv) (paperMeasure.prod paperMeasure) (paperMeasure.prod paperMeasure)

The outgoing endpoint shear preserves the exact paper product measure.

noncomputable def Anderson4D.r324PrimitiveHeadFirstOutgoingGapMeasurableEquiv (n : ℕ) (hn : 1 ≤ n) : (Fin (2 * n) → T4) ≃ᵐ (T4 × T4) × (Fin (2 * n - 2) → T4)

Split a positive primitive tuple in the exact outgoing paper order ((first,gap),internal), with last = first - gap.

Equations

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

@[simp]

theorem Anderson4D.r324PrimitiveHeadFirstOutgoingGapMeasurableEquiv_symm_apply (n : ℕ) (hn : 1 ≤ n) (first gap : T4) (u : Fin (2 * n - 2) → T4) : (r324PrimitiveHeadFirstOutgoingGapMeasurableEquiv n hn).symm ((first, gap), u) = primitiveAssemble n hn first (first - gap) u

theorem Anderson4D.measurePreserving_r324PrimitiveHeadFirstOutgoingGapMeasurableEquiv (n : ℕ) (hn : 1 ≤ n) : MeasureTheory.MeasurePreserving (⇑(r324PrimitiveHeadFirstOutgoingGapMeasurableEquiv n hn)) (MeasureTheory.Measure.pi fun (x : Fin (2 * n)) => paperMeasure) ((paperMeasure.prod paperMeasure).prod (MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure))

The full outgoing primitive-head reindex preserves product Haar measure.

theorem Anderson4D.integral_standardBlock_eq_integral_first_outgoingGap_internal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (n : ℕ) (hn : 1 ≤ n) (f : (Fin (2 * n) → T4) → E) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : Fin (2 * n)) => paperMeasure)) : (∫ (t : Fin (2 * n) → T4), f t ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n)) => paperMeasure) = ∫ (first : T4), ∫ (gap : T4), ∫ (u : Fin (2 * n - 2) → T4), f (primitiveAssemble n hn first (first - gap) u) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * n - 2)) => paperMeasure ∂paperMeasure ∂paperMeasure

Exact primitive-block Fubini in outgoing paper coordinates, with first outermost so the fixed-first Fourier-defect identity applies directly.

Endpoint independence of the terminal split outer factor

@[reducible, inline]

noncomputable abbrev Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.terminalPost {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} (data : res.R324PaperOutgoingEndpointTerminal) : R324WithinHalfResidualPrefix rho lam eps pairing

The completed residual prefix after removing the retained outgoing terminal.

Equations

• data.terminalPost = data.endpoint.stop.afterHead data.terminalData.terminal [] ⋯

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.terminalPost_remaining {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} (data : res.R324PaperOutgoingEndpointTerminal) : data.terminalPost.remaining = []

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.terminalPost_processed_eq_schedule {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} (data : res.R324PaperOutgoingEndpointTerminal) : data.terminalPost.state.processed = r322AnalyticSchedule pairing

Removing the singleton terminal completes the analytic schedule.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.terminalPost_active_eq_finalActive {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} (data : res.R324PaperOutgoingEndpointTerminal) : data.terminalPost.state.active = finalActive pairing

The completed post-terminal carrier is the paper's final residual carrier.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.terminalPost_active_nonempty_of_singles {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} (data : res.R324PaperOutgoingEndpointTerminal) (hsingles : pairing.singles.Nonempty) : data.terminalPost.state.active.Nonempty

A surviving single gives the nonempty terminal interior carrier used to separate both endpoint legs.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.terminalPost_active_lt_terminal_left {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} (data : res.R324PaperOutgoingEndpointTerminal) {i : Fin m} (hi : i ∈ data.terminalPost.state.active) : i < data.terminalData.terminal.1.1

Every vertex surviving the outgoing terminal lies strictly to the left of that terminal. Its right endpoint is the final internal vertex, so there is no second exterior region.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.predecessorSlot_eq_terminalPost_outgoing {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} (data : res.R324PaperOutgoingEndpointTerminal) (hpred : r324WithinHalfPredecessorSlot data.endpoint.stop.state data.terminalData.terminal ≠ 0) (hactive : data.terminalPost.state.active.Nonempty) : r324WithinHalfPredecessorSlot data.endpoint.stop.state data.terminalData.terminal = data.terminalPost.terminalOutgoingEdgeSlot hactive

In the residual terminal branch, the old head predecessor is exactly the outgoing boundary slot of the completed post-terminal carrier.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.terminalPost_incomingPhaseAnchor_eq_of_outgoing_endpoint {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} (data : res.R324PaperOutgoingEndpointTerminal) (hactive : data.terminalPost.state.active.Nonempty) (x y y' : T4) (v : data.terminalPost.SurvivingCoordinate → T4) : data.terminalPost.incomingPhaseAnchor x y v = data.terminalPost.incomingPhaseAnchor x y' v

At a nonempty completed post-terminal carrier, the incoming phase anchor does not see the outgoing external variable.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.incomingErasedHeadOuterFactor_eq_of_outgoing_endpoint {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} (data : res.R324PaperOutgoingEndpointTerminal) (hpred : r324WithinHalfPredecessorSlot data.endpoint.stop.state data.terminalData.terminal ≠ 0) (hactive : data.terminalPost.state.active.Nonempty) (x y y' : T4) (v : data.terminalPost.SurvivingCoordinate → T4) : data.endpoint.stop.incomingErasedHeadOuterFactor data.terminalData.terminal [] ⋯ rho eps x y v = data.endpoint.stop.incomingErasedHeadOuterFactor data.terminalData.terminal [] ⋯ rho eps x y' v

Every ordinary factor outside the retained terminal head is independent of the outgoing endpoint. The only post-terminal active edge that can reach that endpoint is the old predecessor, and it belongs to headChainSlots, so the erased outer product excludes it.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.terminalSplitOuter {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} (data : res.R324PaperOutgoingEndpointTerminal) (coefficient : (data.terminalPost.SurvivingCoordinate → T4) → ℂ) (incomingMode : Z4) (x : T4) (v : data.terminalPost.SurvivingCoordinate → T4) : ℂ

The complete coefficient/phase/exterior factor held fixed during the outgoing terminal's primitive and endpoint integrations.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.incomingPhasedResidualDensity_terminal_split_eq_rawLocal_mul_outer {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} (data : res.R324PaperOutgoingEndpointTerminal) (hpred : r324WithinHalfPredecessorSlot data.endpoint.stop.state data.terminalData.terminal ≠ 0) (hactive : data.terminalPost.state.active.Nonempty) (coefficient : (data.terminalPost.SurvivingCoordinate → T4) → ℂ) (incomingMode : Z4) (x y : T4) (t : Fin (2 * residualBlockOrder data.terminalData.terminal.2) → T4) (v : data.terminalPost.SurvivingCoordinate → T4) : data.endpoint.stop.incomingPhasedResidualDensity (coefficient v) incomingMode rho eps x y ((data.endpoint.stop.splitSurvivingPiMeasurableEquiv data.terminalData.terminal [] ⋯).symm (t, v)) = ↑(data.terminalContext.rawLocalIntegrand rho eps (data.terminalPredecessorPoint x v - y) fun (j : Fin (2 * residualBlockOrder data.terminalContext.step.2)) => t j - y) * data.terminalSplitOuter coefficient incomingMode x v

Exact pointwise terminal split with the outgoing-independent outer factor made literal.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperOutgoingEndpointTerminal.lamEps_pow_integral_standardBlock_outgoingFourier_eq_defect {rho : SmoothCutoff} {lam eps : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix rho lam eps pairing} (data : res.R324PaperOutgoingEndpointTerminal) (hpred : r324WithinHalfPredecessorSlot data.endpoint.stop.state data.terminalData.terminal ≠ 0) (hactive : data.terminalPost.state.active.Nonempty) (coefficient : (data.terminalPost.SurvivingCoordinate → T4) → ℂ) (incomingMode outgoingMode : Z4) (x : T4) (v : data.terminalPost.SurvivingCoordinate → T4) (hhead : MeasureTheory.Integrable (fun (t : Fin (2 * residualBlockOrder data.terminalData.terminal.2) → T4) => ∫ (y : T4), charT4 outgoingMode y * data.endpoint.stop.incomingPhasedResidualDensity (coefficient v) incomingMode rho eps x y ((data.endpoint.stop.splitSurvivingPiMeasurableEquiv data.terminalData.terminal [] ⋯).symm (t, v)) ∂paperMeasure) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminalData.terminal.2)) => paperMeasure)) (hint : ∀ (gap first : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder data.terminalData.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2) → T4) => detJclosedIntegrandWith rho eps (2 * residualBlockOrder data.terminalData.terminal.2) (↑κB) data.terminalContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminalData.terminal.2) ⋯ first (first - gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2)) => paperMeasure)) : (↑(lamEps lam eps) ^ (2 * residualBlockOrder data.terminalData.terminal.2) * ∫ (t : Fin (2 * residualBlockOrder data.terminalData.terminal.2) → T4), ∫ (y : T4), charT4 outgoingMode y * data.endpoint.stop.incomingPhasedResidualDensity (coefficient v) incomingMode rho eps x y ((data.endpoint.stop.splitSurvivingPiMeasurableEquiv data.terminalData.terminal [] ⋯).symm (t, v)) ∂paperMeasure ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminalData.terminal.2)) => paperMeasure) = ∫ (first : T4), (↑(data.terminalContext.state.edges (r324WithinHalfPredecessorSlot data.terminalContext.state data.terminalContext.step) (data.terminalPredecessorPoint x v - first)) * ↑(paperSecondOrderModeDecay outgoingMode) * charT4 outgoingMode first * ∫ (gap : T4), ↑(primitiveKernelDiff rho lam eps (residualBlockOrder data.terminalData.terminal.2) ⋯ data.terminalContext.internalEdges gap) * (charT4 (-outgoingMode) gap - 1) ∂paperMeasure) * data.terminalSplitOuter coefficient incomingMode x v ∂paperMeasure

Complete exact outgoing-terminal section.

For fixed post-terminal coordinates, the whole standard primitive tuple and the outgoing Fourier variable are integrated in the paper order. The terminal split outer factor is held fixed only after its endpoint independence has been proved above. The conclusion exposes exactly the ordinary primitive phase defect; no absolute value has been taken.