Honest processed integrands for an R-324 within-half step

The current heterogeneous edge state represents blocks already integrated from the analytic prefix. The next block remains an actual local spatial integral, multiplied by an arbitrary fixed outer factor. No statement here identifies an unprocessed production integrand pointwise with this state.

def Anderson4D.R324WithinHalfStepContext.blockIndex {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) : ExtractionBlockIndex pairing

The current concrete block as a genuine extraction-block coordinate.

Equations

• ctx.blockIndex = ⟨ctx.step.2, ⋯⟩

def Anderson4D.R324WithinHalfStepContext.standardBlockTuple {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (x : Fin m → T4) : Fin (2 * residualBlockOrder ctx.step.2) → T4

Restriction of an ambient within-half tuple to the current sparse block.

Equations

• ctx.standardBlockTuple x i = x ↑(ctx.blockOrderIso i)

theorem Anderson4D.R324WithinHalfStepContext.extractionBlockPrimitiveSum_eq_standardBlock {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (ρ : SmoothCutoff) (ε : ℝ) (x : Fin m → T4) : r322ExtractionBlockPrimitiveSum ρ ε pairing ctx.blockIndex x = ∑ κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2)), primitiveCovarianceProduct ρ ε (residualBlockOrder ctx.step.2) (↑κB) (ctx.standardBlockTuple x)

noncomputable def Anderson4D.R324WithinHalfStepContext.rawLocalIntegrand {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (ρ : SmoothCutoff) (ε : ℝ) (u : T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : ℝ

The unintegrated local factor in standard block coordinates.

Equations

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

noncomputable def Anderson4D.R324WithinHalfStepContext.localIntegrand {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (ρ : SmoothCutoff) (ε : ℝ) (u : T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : ℝ

Closed-J form consumed by the signed three-kernel collapse.

Equations

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

theorem Anderson4D.R324WithinHalfStepContext.rawLocalIntegrand_eq_localIntegrand {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (ρ : SmoothCutoff) (ε : ℝ) (u : T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : ctx.rawLocalIntegrand ρ ε u t = ctx.localIntegrand ρ ε u t

noncomputable def Anderson4D.R324WithinHalfStepContext.processedIntegrand {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (ρ : SmoothCutoff) (ε : ℝ) (u : T4) (x : Fin m → T4) (outer : ℝ) : ℝ

Ambient processed factor for the current block and a fixed outer factor. Earlier blocks enter only through ctx.state.edges.

Equations

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

theorem Anderson4D.R324WithinHalfStepContext.processedIntegrand_eq_local_mul_outer {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (ρ : SmoothCutoff) (ε : ℝ) (u : T4) (x : Fin m → T4) (outer : ℝ) : ctx.processedIntegrand ρ ε u x outer = ctx.localIntegrand ρ ε u (ctx.standardBlockTuple x) * outer

Exact pointwise local-times-outer factorization of the processed state.

noncomputable def Anderson4D.R324WithinHalfStepContext.localSpatialIntegral {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (ρ : SmoothCutoff) (lam ε : ℝ) (u : T4) : ℝ

Signed spatial integral of the current processed local factor.

Equations

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

theorem Anderson4D.R324WithinHalfStepContext.localSpatialIntegral_eq_absorb_predecessor {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (ρ : SmoothCutoff) (lam ε : ℝ) (u : T4) (hstandard : MeasureTheory.Integrable (ctx.localIntegrand ρ ε u) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))), MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges (primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ p.1 p.2 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure)) : ctx.localSpatialIntegral ρ lam ε u = (ctx.absorb ρ lam ε).edges (r324WithinHalfPredecessorSlot ctx.state ctx.step) u

One honest processed spatial section is exactly the predecessor edge of the absorbed state.