Certified within-half traces stopping before an arbitrary named step

This module consumes a prescribed proper prefix of a within-half analytic schedule and stops immediately before a specified step. The complete unconsumed suffix is retained as terminal :: suffix; in particular, the named step need not be the last step of the schedule.

The trace carries only consequences of the genuine local-block provider: the reachable residual prefix, the transported scale and edge certificate, and the literal surviving-coordinate projections. It does not integrate the named step or any part of the suffix.

inductive Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (terminal : R322ExtractionStep m) (suffix : List (R322ExtractionStep m)) (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : (Fin (m + 1) → ℝ) → Type

A certified analytic trace stopped immediately before an arbitrary specified schedule step, retaining that step and its complete suffix.

• stop {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {suffix : List (R322ExtractionStep m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (scale : Fin (m + 1) → ℝ) (hremaining : res.remaining = terminal :: suffix) (certificate : R324WithinHalfEdgeCertificate res.state scale) : R324WithinHalfStopBeforeStepTrace terminal suffix res scale
• step {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {suffix : List (R322ExtractionStep m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (scale : Fin (m + 1) → ℝ) (internal : res.R324WithinHalfResidualInternalReady head tail hremaining) (nextScale : Fin (m + 1) → ℝ) (nextCertificate : R324WithinHalfEdgeCertificate (res.afterHead head tail hremaining).state nextScale) (next : R324WithinHalfStopBeforeStepTrace terminal suffix (res.afterHead head tail hremaining) nextScale) : R324WithinHalfStopBeforeStepTrace terminal suffix res scale

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

Consume exactly pre and stop before terminal, retaining terminal :: suffix. The provider is called precisely on the steps of pre, never on the named stop step or its suffix.

Equations

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

def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.stopPrefix {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {suffix : List (R322ExtractionStep m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : R324WithinHalfStopBeforeStepTrace terminal suffix res scale) : R324WithinHalfResidualPrefix ρ lam ε pairing

The genuine residual prefix at which the trace stops.

Equations

• (Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.stop res scale hremaining certificate).stopPrefix = res
• (Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.step res head tail hremaining scale internal nextScale nextCertificate next).stopPrefix = next.stopPrefix

def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.stopScale {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {suffix : List (R322ExtractionStep m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : R324WithinHalfStopBeforeStepTrace terminal suffix res scale) : Fin (m + 1) → ℝ

The scale transported through the consumed prefix.

Equations

• (Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.stop res scale hremaining certificate).stopScale = scale
• (Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.step res head tail hremaining scale internal nextScale nextCertificate next).stopScale = next.stopScale

def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.stopProjection {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {suffix : List (R322ExtractionStep m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : R324WithinHalfStopBeforeStepTrace terminal suffix res scale) : (res.SurvivingCoordinate → T4) → trace.stopPrefix.SurvivingCoordinate → T4

Restrict a surviving tuple through every genuinely consumed block.

Equations

• One or more equations did not get rendered due to their size.
• (Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.stop res scale hremaining certificate).stopProjection = fun (v : res.SurvivingCoordinate → Anderson4D.T4) => v

def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.WeightedIntegrableAlong {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {suffix : List (R322ExtractionStep m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (x y : T4) (trace : R324WithinHalfStopBeforeStepTrace terminal suffix res scale) (outer : (trace.stopPrefix.SurvivingCoordinate → T4) → ℂ) : Prop

Full weighted integrability at exactly the scalar integrations consumed before the named stop step.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.stopPrefix_remaining_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {suffix : List (R322ExtractionStep m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : R324WithinHalfStopBeforeStepTrace terminal suffix res scale) : trace.stopPrefix.remaining = terminal :: suffix

The stopped prefix retains the named step and its complete suffix.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.stopPrefix_processed_append_eq_schedule {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {suffix : List (R322ExtractionStep m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : R324WithinHalfStopBeforeStepTrace terminal suffix res scale) : trace.stopPrefix.state.processed ++ terminal :: suffix = r322AnalyticSchedule pairing

At the stop, the processed prefix followed by the retained named suffix is exactly the full analytic schedule.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.stopPrefix_remainingOrder_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {suffix : List (R322ExtractionStep m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : R324WithinHalfStopBeforeStepTrace terminal suffix res scale) : trace.stopPrefix.remainingOrder = residualBlockOrder terminal.2 + (List.map (fun (step : R322ExtractionStep m) => residualBlockOrder step.2) suffix).sum

The exact perturbative order retained at the stop is the order of the whole literal suffix beginning at the named step.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.stopCertificate {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {suffix : List (R322ExtractionStep m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : R324WithinHalfStopBeforeStepTrace terminal suffix res scale) : R324WithinHalfEdgeCertificate trace.stopPrefix.state trace.stopScale

The edge certificate genuinely transported to the stopping state.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.lamEps_pow_integral_mul_stopOuter_eq_stop {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {suffix : List (R322ExtractionStep m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (x y : T4) (trace : R324WithinHalfStopBeforeStepTrace terminal suffix res scale) (outer : (trace.stopPrefix.SurvivingCoordinate → T4) → ℂ) (hweighted : WeightedIntegrableAlong x y trace outer) : (↑(lamEps lam ε) ^ (2 * res.remainingOrder) * ∫ (v : res.SurvivingCoordinate → T4), ↑(res.residualIntegrand ρ ε x y (res.reconstruct v)) * outer (trace.stopProjection v) ∂MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) = ↑(lamEps lam ε) ^ (2 * trace.stopPrefix.remainingOrder) * ∫ (v : trace.stopPrefix.SurvivingCoordinate → T4), ↑(trace.stopPrefix.residualIntegrand ρ ε x y (trace.stopPrefix.reconstruct v)) * outer v ∂MeasureTheory.Measure.pi fun (x : trace.stopPrefix.SurvivingCoordinate) => paperMeasure

Exact weighted integral transport through the prescribed prefix.

The right-hand side retains the exact lamEps power 2 * trace.stopPrefix.remainingOrder; neither the named step nor any later suffix step has been integrated.