Coordinate projection to an arbitrary R-324 stopping step

A certified stop-before-step trace removes only the coordinates belonging to the genuinely consumed schedule prefix. This module realizes the resulting coordinate transport as a literal embedding of stop coordinates into the carrier at which the trace starts. It also proves that projection is pointwise restriction along that embedding and that ambient reconstruction commutes with the restriction.

Unlike the terminal projection API, the named stop step and its complete suffix remain unprocessed. Consequently the stop active carrier need not equal finalActive; the exact generally valid statement is the inclusion of finalActive in the stop carrier.

def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.stopCoordinateEmbedding {ρ : 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.SurvivingCoordinate → res.SurvivingCoordinate

Regard a coordinate surviving to the named stopping step as a coordinate of the residual prefix at which the trace starts.

Equations

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

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.stopCoordinateEmbedding_val {ρ : 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) (i : trace.stopPrefix.SurvivingCoordinate) : ↑(trace.stopCoordinateEmbedding i) = ↑i

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.stopProjection_apply {ρ : 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) (v : res.SurvivingCoordinate → T4) (i : trace.stopPrefix.SurvivingCoordinate) : trace.stopProjection v i = v (trace.stopCoordinateEmbedding i)

The trace projection is pointwise restriction along the concrete stop coordinate embedding.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.reconstruct_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) (v : res.SurvivingCoordinate → T4) (i : trace.stopPrefix.SurvivingCoordinate) : res.reconstruct v ↑i = trace.stopPrefix.reconstruct (trace.stopProjection v) ↑i

Reconstruction at every stop coordinate is unchanged by projecting through the consumed prefix.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.finalActive_subset_stopPrefix_active {ρ : 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) : finalActive pairing ⊆ trace.stopPrefix.state.active

Every terminal residual vertex survives at any earlier named stopping step. Equality is generally false because the retained step and suffix still contribute unprocessed block coordinates.

def Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.finalActiveCoordinateEmbedding {ρ : 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) : ↥(finalActive pairing) → trace.stopPrefix.SurvivingCoordinate

Embed a terminal residual coordinate into the still-larger carrier at the named stopping step.

Equations

• trace.finalActiveCoordinateEmbedding i = ⟨↑i, ⋯⟩

@[simp]

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfStopBeforeStepTrace.finalActiveCoordinateEmbedding_val {ρ : 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) (i : ↥(finalActive pairing)) : ↑(trace.finalActiveCoordinateEmbedding i) = ↑i

theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.finalActive_subset_stop_active {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κ initialScale) : finalActive κ ⊆ data.trace.stopPrefix.state.active

Consumer form of the terminal-carrier inclusion for an incoming exceptional stop package.