Quantitative carrier-relative R-322 update

This file connects the production heterogeneous-edge state transition with the analytic one-block estimate. The outgoing-edge invariant removes the last apparent mismatch: the quantitative collapse theorem is stated with a free right Green kernel, and the next production edge is proved to have exactly that kernel.

theorem Anderson4D.R322AnalyticProperStepContext.nextState_predecessor_eq_r322Collapse {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (lam ε : ℝ) (u : T4) : (ctx.nextState ρ lam ε).edges ctx.predecessorEdge u = r322Collapse (ctx.state.edges ctx.predecessorEdge) (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges) (ctx.state.edges ctx.outgoingEdge) u

At the predecessor slot, the state update is definitionally the three-kernel collapse with the current heterogeneous incoming, primitive, and outgoing kernels.

theorem Anderson4D.R322AnalyticProperStepContext.nextState_predecessor_eq_r322Collapse_greenFn {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) {ρ : SmoothCutoff} {lam ε : ℝ} {κ : PartialPairing (Fin (2 * q))} {hκ : κ ∈ nonSplitPairings q} (hstate : R322AnalyticAbsorbedState ρ lam ε hq κ hκ ctx.state) (hpairing : ctx.pairing = κ) (u : T4) : (ctx.nextState ρ lam ε).edges ctx.predecessorEdge u = r322Collapse (ctx.state.edges ctx.predecessorEdge) (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges) greenFn u

For an actually reachable state, the same update is the precise free-right-Green collapse required by the quantitative one-block theorem.

theorem Anderson4D.exists_r322AnalyticNextState_predecessor_le {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (ρ : SmoothCutoff) (C lam ε A : ℝ) (q : ℕ) (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (ctx : R322AnalyticProperStepContext q hq), R322AnalyticAbsorbedState ρ lam ε hq κ hκ ctx.state → ctx.pairing = κ → 0 ≤ C → 0 ≤ lam → 0 ≤ A → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → Measurable (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges) → MemEClassT4 (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges) → (∀ (u : T4), |primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges u| ≤ primitiveKernelMajorant C lam ε supportConstant (residualBlockOrder ctx.step.2) u) → (∀ (z : T4), z ≠ 0 → |ctx.state.edges ctx.predecessorEdge z| ≤ A * invSqKer z) → (∀ (x : T4), x ≠ 0 → MeasureTheory.Integrable (r322CollapseIntegrand (ctx.state.edges ctx.predecessorEdge) (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges) greenFn x) (paperMeasure.prod paperMeasure)) → ∀ (x : T4), x ≠ 0 → |(ctx.nextState ρ lam ε).edges ctx.predecessorEdge x| ≤ A * (C * lam) ^ (2 * residualBlockOrder ctx.step.2) * K * invSqKer x

A production proper step inherits the exact inverse-square estimate of exists_r322Collapse_le. The constant is chosen before every scale, coupling, block order, state, and endpoint.