Certified within-half traces stopping before the last block

This module gives a generic analytic trace which consumes a prescribed prefix of a within-half residual schedule and stops with one specified block still present. It is deliberately independent of any theorem identifying which block is last in a concrete schedule.

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

A certified analytic trace which stops immediately before a specified last block.

The step constructor stores the same analytic data as R324WithinHalfCertifiedAnalyticTrace.step: internal Fubini evidence, the updated scale, and a certificate for the updated edge state.

• stop {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (scale : Fin (m + 1) → ℝ) (hremaining : res.remaining = [terminal]) (certificate : R324WithinHalfEdgeCertificate res.state scale) : R324WithinHalfStopBeforeLastTrace terminal res scale
• step {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : 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 : R324WithinHalfStopBeforeLastTrace terminal (res.afterHead head tail hremaining) nextScale) : R324WithinHalfStopBeforeLastTrace terminal res scale

def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeLastTrace.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) (pre : List (R322ExtractionStep m)) (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (scale : Fin (m + 1) → ℝ) (certificate : R324WithinHalfEdgeCertificate res.state scale) (hremaining : res.remaining = pre ++ [terminal]) : R324WithinHalfStopBeforeLastTrace terminal res scale

Consume exactly the supplied prefix and leave the specified final block untouched. In particular, the local provider is never called on terminal.

Equations

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

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

The residual prefix at which the trace stops.

Equations

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

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

The scale certified at the stopping prefix.

Equations

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

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

Restrict a surviving tuple through all consumed prefix blocks.

Equations

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

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

Full weighted integrability at exactly the scalar integrals consumed before the last block.

Equations

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

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeLastTrace.stopPrefix_remaining_eq_singleton {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : R324WithinHalfStopBeforeLastTrace terminal res scale) : trace.stopPrefix.remaining = [terminal]

The stopping prefix has the requested singleton suffix.

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

At the stop, the processed prefix followed by the retained block is the full analytic schedule.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeLastTrace.stopPrefix_remainingOrder_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (trace : R324WithinHalfStopBeforeLastTrace terminal res scale) : trace.stopPrefix.remainingOrder = residualBlockOrder terminal.2

The exact perturbative order retained at the stop is the order of the single untouched block.

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

The final edge certificate carried by the trace.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeLastTrace.lamEps_pow_integral_mul_stopOuter_eq_stop {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {terminal : R322ExtractionStep m} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (x y : T4) (trace : R324WithinHalfStopBeforeLastTrace terminal 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 iteration through the prescribed prefix.

Unlike the full trace theorem, the right-hand side retains the exact lamEps power belonging to the untouched singleton block.