Processed-integrand invariant for R-322

An unintegrated original endpoint-fibre integrand is not pointwise equal to a state in which earlier blocks have already been integrated. The honest invariant is therefore inductive: the initial state is reachable, and one certified proper spatial collapse produces the next reachable state. Its processed list remains a prefix of the production analytic schedule.

For the current step, processedLocalFactor uses the production r322ExtractionBlockPrimitiveSum. The pointwise theorem below identifies that pre-integration factor with the exact generalized closed-J integrand consumed by the one-step Fubini theorem.

inductive Anderson4D.R322AnalyticAbsorbedState (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) : R322AnalyticEdgeState q hq → Prop

States obtained from the all-Green production state by the exact proper updates of R322AnalyticProperStepContext. This records absorption history, not a pointwise equality with the unintegrated original integrand.

• initial {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} {κ : PartialPairing (Fin (2 * q))} {hκ : κ ∈ nonSplitPairings q} : R322AnalyticAbsorbedState ρ lam ε hq κ hκ (r322InitialAnalyticEdgeState q hq)
• update {ρ : SmoothCutoff} {lam ε : ℝ} {q : ℕ} {hq : 1 ≤ q} {κ : PartialPairing (Fin (2 * q))} {hκ : κ ∈ nonSplitPairings q} (ctx : R322AnalyticProperStepContext q hq) (hpairing : ctx.pairing = κ) (previous : R322AnalyticAbsorbedState ρ lam ε hq κ hκ ctx.state) : R322AnalyticAbsorbedState ρ lam ε hq κ hκ (ctx.nextState ρ lam ε)

theorem Anderson4D.R322AnalyticAbsorbedState.processed_prefix {q : ℕ} {hq : 1 ≤ q} {ρ : SmoothCutoff} {lam ε : ℝ} {κ : PartialPairing (Fin (2 * q))} {hκ : κ ∈ nonSplitPairings q} {state : R322AnalyticEdgeState q hq} (hstate : R322AnalyticAbsorbedState ρ lam ε hq κ hκ state) : ∃ (remaining : List (R322ExtractionStep (2 * q))), r322AnalyticSchedule κ = state.processed ++ remaining

Reachability always carries an actual processed prefix of the fixed production schedule.

theorem Anderson4D.R322AnalyticAbsorbedState.localSpatialIntegral_eq_updatedEdge {q : ℕ} {hq : 1 ≤ q} {ρ : SmoothCutoff} {lam ε : ℝ} {κ : PartialPairing (Fin (2 * q))} {hκ : κ ∈ nonSplitPairings q} (ctx : R322AnalyticProperStepContext q hq) (hpairing : ctx.pairing = κ) (_hstate : R322AnalyticAbsorbedState ρ lam ε hq κ hκ ctx.state) (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.nextState ρ lam ε).edges ctx.predecessorEdge u

The induction constructor preserves the exact one-step integral identity whenever its genuine section-integrability premises hold.

noncomputable def Anderson4D.R322AnalyticProperStepContext.processedLocalFactor {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (ε : ℝ) (u : T4) (x : Fin (2 * q) → T4) : ℝ

Translation-normalized local factor before the current block is integrated. The covariance coordinate is the actual extraction-block factor, while the external successor has been placed at zero. A separate translated-tuple bridge is required before this is used in the ambient endpoint-fibre integrand.

Equations

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

theorem Anderson4D.R322AnalyticProperStepContext.processedLocalFactor_eq_rawLocalIntegrand {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (ε : ℝ) (u : T4) (x : Fin (2 * q) → T4) : ctx.processedLocalFactor ρ ε u x = ctx.rawLocalIntegrand ρ ε u (ctx.standardBlockTuple x)

Exact pointwise reconstruction of the zero-successor current-block factor as the raw local integrand on its canonical sparse tuple.

theorem Anderson4D.R322AnalyticProperStepContext.processedLocalFactor_eq_localIntegrand {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (ε : ℝ) (u : T4) (x : Fin (2 * q) → T4) : ctx.processedLocalFactor ρ ε u x = ctx.localIntegrand ρ ε u (ctx.standardBlockTuple x)

Hence the zero-successor current-block factor is exactly the closed-J integrand already consumed by the signed spatial collapse.

theorem Anderson4D.R322AnalyticProperStepContext.processedLocalFactor_mul_outer {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (ε : ℝ) (u : T4) (x : Fin (2 * q) → T4) (outer : ℝ) : ctx.processedLocalFactor ρ ε u x * outer = ctx.localIntegrand ρ ε u (ctx.standardBlockTuple x) * outer

Pointwise local-times-outer form used immediately below the outer integral. The outer factor is not constrained or smuggled in as a target equality.

def Anderson4D.R322AnalyticProperStepContext.reconstructBlockTuple {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (base : Fin (2 * q) → T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : Fin (2 * q) → T4

Replace exactly the ambient vertices of the current concrete block by a standard sparse tuple; all complementary ambient coordinates are retained.

Equations

• ctx.reconstructBlockTuple base t i = if hi : i ∈ ctx.step.2 then t (ctx.blockOrderIso.symm ⟨i, hi⟩) else base i

@[simp]

theorem Anderson4D.R322AnalyticProperStepContext.standardBlockTuple_reconstructBlockTuple {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (base : Fin (2 * q) → T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : ctx.standardBlockTuple (ctx.reconstructBlockTuple base t) = t

Reading the reconstructed ambient tuple on the production block returns the supplied standard tuple literally.

theorem Anderson4D.R322AnalyticProperStepContext.processedLocalFactor_reconstructBlockTuple {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (ε : ℝ) (u : T4) (base : Fin (2 * q) → T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : ctx.processedLocalFactor ρ ε u (ctx.reconstructBlockTuple base t) = ctx.localIntegrand ρ ε u t

Zero-successor coordinate reconstruction. This is not by itself the ambient production bridge: there the supplied block tuple and incoming coordinate must first be translated by the active successor.