Phased within-half transport stopping before a named terminal step

The complete alternating driver consumes the whole analytic schedule. In the outgoing-shortcut branch this is one step too far: the distinguished terminal block must remain visible for the endpoint Fourier collapse.

This module runs the same ordinary/exceptional alternation only through the proper prefix before a prescribed final step. Ordinary runs are represented by R324WithinHalfStopBeforeStepTrace; a slot-zero-fed head is represented by R324WithinHalfNextExceptionalStop. The recursion is on the length of the proper prefix before the named terminal. Consequently the terminal step is never absorbed.

No norm is taken here. The exact signed/phased integral, its transported coefficient, and a quantitative edge certificate at the stop are retained.

The strictly decreasing terminal-prefix ledger

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfNextExceptionalStop.exists_terminalPrefix_lt {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (data : res.R324WithinHalfNextExceptionalStop scale) (pre : List (R322ExtractionStep m)) (hremaining : res.remaining = pre ++ [terminal]) (hbefore : data.pre.length < pre.length) : ∃ (post : List (R322ExtractionStep m)), data.suffix = post ++ [terminal] ∧ post.length < pre.length

At a next exceptional stop lying strictly inside the proper prefix before terminal, the after-head suffix again has a proper-prefix/terminal decomposition, and that new proper prefix is strictly shorter.

The endpoint-stop transport package

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

Exact phased transport from a reachable residual prefix to the state immediately before a prescribed final schedule step. The terminal remains the singleton remaining list.

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

  Genuine parameter-carrying integrability. Paper Step 4(A) keeps the untouched opposite-half endpoint variables outside every signed elimination, so the retained outgoing terminal needs this joint form for the final Fubini exchange.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointStopAtTerminal.stop_processed_append_terminal_eq_schedule {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} (data : R324WithinHalfEndpointStopAtTerminal terminal res) : data.stop.state.processed ++ [terminal] = r322AnalyticSchedule pairing

The stopped state still satisfies the exact schedule ledger.

Base case: the proper prefix is wholly ordinary

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointStopAtTerminal.of_ordinaryTrace {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : R324WithinHalfStopBeforeStepTrace terminal [] res scale) (hordinary : trace.OrdinaryAlong) : R324WithinHalfEndpointStopAtTerminal terminal res

An ordinary stop-before-step trace is already an endpoint-stop transport, with trivial multiplier and its transported edge certificate.

Equations

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

Recursive step: one exceptional head before the terminal

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

Compose the ordinary run and exceptional collapse at the next stop with an endpoint-stop transport of its after-head suffix. The named terminal remains untouched in the recursive subtransport.

Equations

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

Strong-induction driver

@[irreducible]

def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointStopAtTerminal.of_localBlockProvider {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K pairing) (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (scale : Fin (m + 1) → ℝ) (certificate : R324WithinHalfEdgeCertificate res.state scale) (terminal : R322ExtractionStep m) (pre : List (R322ExtractionStep m)) (hremaining : res.remaining = pre ++ [terminal]) : R324WithinHalfEndpointStopAtTerminal terminal res

Endpoint-stop driver. Starting from an explicit decomposition remaining = pre ++ [terminal], alternate ordinary runs and exceptional head collapses only through pre. The recursion terminates because the proper prefix exposed after every exceptional head is strictly shorter. The named terminal itself is never consumed.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointStopAtTerminal.exists_r324WithinHalfEndpointStopAtTerminal {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K pairing) (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (scale : Fin (m + 1) → ℝ) (certificate : R324WithinHalfEdgeCertificate res.state scale) (terminal : R322ExtractionStep m) (pre : List (R322ExtractionStep m)) (hremaining : res.remaining = pre ++ [terminal]) : Nonempty (R324WithinHalfEndpointStopAtTerminal terminal res)

Headline existence form used by the outgoing-shortcut assembly.