Quantitative one-block closure for an R-324 within-half suffix

This file supplies the analytic counterpart of the exact residual transport: every genuine schedule head is estimated by Proposition 4.1, its predecessor edge scale is updated once, and the resulting certificate is carried through the literal remaining suffix.

Future outgoing slots remain free Green edges

theorem Anderson4D.r324WithinHalfPredecessorSlot_val_le_step_left {m : ℕ} (state : R324WithinHalfEdgeState m) (step : R322ExtractionStep m) : ↑(r324WithinHalfPredecessorSlot state step) ≤ ↑step.1.1

theorem Anderson4D.R324WithinHalfStateReachable.edge_eq_greenFn_of_processed_right_lt {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {state : R324WithinHalfEdgeState m} (hstate : R324WithinHalfStateReachable pairing ρ lam ε state) (edge : Fin (m + 1)) (hfuture : ∀ earlier ∈ state.processed, ↑earlier.1.2 < ↑edge) : state.edges edge = greenFn

An edge strictly to the right of every processed block is untouched by the genuine within-half collapse recursion.

theorem Anderson4D.R324WithinHalfResidualPrefix.state_edges_head_outgoing_eq_greenFn {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) : res.state.edges (r324InternalVertexEdgeSlot head.1.2) = greenFn

The outgoing edge of the literal remaining head has not yet been updated, so the actual R-324 collapse uses the free Green function there.

Slotwise quantitative certificates

structure Anderson4D.R324WithinHalfEdgeCertificate {m : ℕ} (state : R324WithinHalfEdgeState m) (scale : Fin (m + 1) → ℝ) : Prop

Every named edge is measurable, belongs to the paper's symmetry class, and is controlled off the identity by its own positive inverse-square scale.

• scale_pos (edge : Fin (m + 1)) : 0 < scale edge
• measurable (edge : Fin (m + 1)) : Measurable (state.edges edge)
• memE (edge : Fin (m + 1)) : MemEClassT4 (state.edges edge)
• bound (edge : Fin (m + 1)) (z : T4) : z ≠ 0 → |state.edges edge z| ≤ scale edge * invSqKer z

theorem Anderson4D.exists_r324InitialWithinHalfEdgeCertificate (m : ℕ) : ∃ (A : ℝ), 0 < A ∧ R324WithinHalfEdgeCertificate (r324InitialWithinHalfEdgeState m) fun (x : Fin (m + 1)) => A

The all-Green initial state has a uniform quantitative certificate.

def Anderson4D.r324WithinHalfInternalEdgeScaleProduct {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (scale : Fin (m + 1) → ℝ) : ℝ

Product of all current named scales used by the literal head primitive.

Equations

• Anderson4D.r324WithinHalfInternalEdgeScaleProduct ctx scale = ∏ j : Fin (2 * Anderson4D.residualBlockOrder ctx.step.2 - 1), scale (ctx.internalSlot j)

theorem Anderson4D.R324WithinHalfEdgeCertificate.internalEdgeScaleProduct_pos {m : ℕ} {pairing : PartialPairing (Fin m)} {ctx : R324WithinHalfStepContext pairing} {scale : Fin (m + 1) → ℝ} (hcert : R324WithinHalfEdgeCertificate ctx.state scale) : 0 < r324WithinHalfInternalEdgeScaleProduct ctx scale

def Anderson4D.r324WithinHalfUpdatedEdgeScale {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (scale : Fin (m + 1) → ℝ) (C lam K : ℝ) : Fin (m + 1) → ℝ

Exact local scale ledger for one actual within-half head collapse.

Equations

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

@[simp]

theorem Anderson4D.r324WithinHalfUpdatedEdgeScale_predecessor {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (scale : Fin (m + 1) → ℝ) (C lam K : ℝ) : r324WithinHalfUpdatedEdgeScale ctx scale C lam K (r324WithinHalfPredecessorSlot ctx.state ctx.step) = scale (r324WithinHalfPredecessorSlot ctx.state ctx.step) * r324WithinHalfInternalEdgeScaleProduct ctx scale * (C * lam) ^ (2 * residualBlockOrder ctx.step.2) * K

theorem Anderson4D.r324WithinHalfUpdatedEdgeScale_of_ne {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (scale : Fin (m + 1) → ℝ) (C lam K : ℝ) (edge : Fin (m + 1)) (hne : edge ≠ r324WithinHalfPredecessorSlot ctx.state ctx.step) : r324WithinHalfUpdatedEdgeScale ctx scale C lam K edge = scale edge

One genuine Proposition 4.1 block estimate

structure Anderson4D.R324WithinHalfPrimitiveCertificate {m : ℕ} {pairing : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext pairing) (scale : Fin (m + 1) → ℝ) (ρ : SmoothCutoff) (C lam ε supportConstant : ℝ) : Prop

The local analytic data derived for the primitive kernel of one literal schedule head. Its scale is the product of the current internal edge scales; integrability is for the exact three-kernel collapse with free Green outgoing edge.

• measurable : Measurable (ctx.primitiveKernel ρ lam ε)
• memE : MemEClassT4 (ctx.primitiveKernel ρ lam ε)
• bound (u : T4) : u ≠ 0 → |ctx.primitiveKernel ρ lam ε u| ≤ r324WithinHalfInternalEdgeScaleProduct ctx scale * primitiveKernelMajorant C lam ε supportConstant (residualBlockOrder ctx.step.2) u
• integrable (x : T4) : x ≠ 0 → MeasureTheory.Integrable (r322CollapseIntegrand (ctx.state.edges (r324WithinHalfPredecessorSlot ctx.state ctx.step)) (ctx.primitiveKernel ρ lam ε) greenFn x) (paperMeasure.prod paperMeasure)

theorem Anderson4D.R324WithinHalfEdgeCertificate.primitiveCertificate {m : ℕ} {pairing : PartialPairing (Fin m)} {ctx : R324WithinHalfStepContext pairing} {scale : Fin (m + 1) → ℝ} (hcert : R324WithinHalfEdgeCertificate ctx.state scale) (ρ : SmoothCutoff) (C lam ε supportConstant : ℝ) (hε : 0 < ε) (hlog : 0 < |Real.log ε|) (hprop : ∀ (H : Fin (2 * residualBlockOrder ctx.step.2 - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput (residualBlockOrder ctx.step.2) H → MemEClassT4 (primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ H) ∧ MemEClassT4 (primitiveKernelInsertedDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ H) ∧ PrimitiveKernelBounds ρ lam ε (residualBlockOrder ctx.step.2) ⋯ H supportConstant C) : R324WithinHalfPrimitiveCertificate ctx scale ρ C lam ε supportConstant

The current slotwise certificate and Proposition 4.1 produce the full local primitive certificate. In particular, raw integrability is derived from the inverse-square convolution majorant, rather than stored globally.

theorem Anderson4D.exists_r324WithinHalf_localBlockClosure {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (ρ : SmoothCutoff) (C lam ε : ℝ) (m : ℕ) (pairing : PartialPairing (Fin m)) (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (scale : Fin (m + 1) → ℝ), R324WithinHalfEdgeCertificate res.state scale → 0 < C → 0 < lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → (∀ (H : Fin (2 * residualBlockOrder head.2 - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput (residualBlockOrder head.2) H → MemEClassT4 (primitiveKernelDiff ρ lam ε (residualBlockOrder head.2) ⋯ H) ∧ MemEClassT4 (primitiveKernelInsertedDiff ρ lam ε (residualBlockOrder head.2) ⋯ H) ∧ PrimitiveKernelBounds ρ lam ε (residualBlockOrder head.2) ⋯ H supportConstant C) → (∀ (x : T4), x ≠ 0 → |(res.afterHead head tail hremaining).state.edges (r324WithinHalfPredecessorSlot res.state head) x| ≤ r324WithinHalfUpdatedEdgeScale (res.headContext head tail hremaining) scale C lam K (r324WithinHalfPredecessorSlot res.state head) * invSqKer x) ∧ R324WithinHalfEdgeCertificate (res.afterHead head tail hremaining).state (r324WithinHalfUpdatedEdgeScale (res.headContext head tail hremaining) scale C lam K)

Local block inequality and certificate transport.

The universal constant comes from the one-block Proposition 4.1 collapse estimate. For each literal schedule head, the first conjunct is the exact predecessor-edge inequality; the second conjunct transports the complete slotwise certificate to afterHead.

Literal suffix induction

def Anderson4D.R324WithinHalfProp41Provider (ρ : SmoothCutoff) (C lam ε supportConstant : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) : Prop

Proposition 4.1 evidence at every literal head that can occur during the within-half suffix recursion. This is a family of local block estimates, not a global moment bound.

Equations

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

def Anderson4D.R324WithinHalfLocalBlockProvider (ρ : SmoothCutoff) (C lam ε K : ℝ) {m : ℕ} (pairing : PartialPairing (Fin m)) : Prop

A provider of one certified scale update at every nonempty literal suffix. Its first output is the actual local pointwise block inequality.

Equations

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

inductive Anderson4D.R324WithinHalfQuantitativeIterationReady {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) : (Fin (m + 1) → ℝ) → Prop

A proof-relevant trace records every genuine local inequality and exact scale update through the remaining list.

• terminal {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (scale : Fin (m + 1) → ℝ) (hremaining : res.remaining = []) (certificate : R324WithinHalfEdgeCertificate res.state scale) : R324WithinHalfQuantitativeIterationReady res scale
• step {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (scale : Fin (m + 1) → ℝ) (certificate : R324WithinHalfEdgeCertificate res.state scale) (localBound : ∀ (x : T4), x ≠ 0 → |(res.afterHead head tail hremaining).state.edges (r324WithinHalfPredecessorSlot res.state head) x| ≤ r324WithinHalfUpdatedEdgeScale (res.headContext head tail hremaining) scale C lam K (r324WithinHalfPredecessorSlot res.state head) * invSqKer x) (next : R324WithinHalfQuantitativeIterationReady (res.afterHead head tail hremaining) (r324WithinHalfUpdatedEdgeScale (res.headContext head tail hremaining) scale C lam K)) : R324WithinHalfQuantitativeIterationReady res scale

theorem Anderson4D.R324WithinHalfQuantitativeIterationReady.of_provider {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K pairing) (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (scale : Fin (m + 1) → ℝ) (certificate : R324WithinHalfEdgeCertificate res.state scale) : R324WithinHalfQuantitativeIterationReady res scale

Structural recursion on the literal remaining suffix constructs the complete quantitative trace from local block closure.

theorem Anderson4D.R324WithinHalfQuantitativeIterationReady.exists_terminal_certificate {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {res : R324WithinHalfResidualPrefix ρ lam ε pairing} {scale : Fin (m + 1) → ℝ} (ready : R324WithinHalfQuantitativeIterationReady res scale) : ∃ (terminal : R324WithinHalfResidualPrefix ρ lam ε pairing) (terminalScale : Fin (m + 1) → ℝ), terminal.remaining = [] ∧ terminal.state.processed = r322AnalyticSchedule pairing ∧ R324WithinHalfEdgeCertificate terminal.state terminalScale

A complete local trace reaches the literal empty suffix and leaves a certified terminal state whose processed list is the whole analytic schedule.

theorem Anderson4D.exists_r324WithinHalf_terminalCertificate_of_prop41 {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (ρ : SmoothCutoff) (C lam ε : ℝ) (m : ℕ) (pairing : PartialPairing (Fin m)), 0 < C → 0 < lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → R324WithinHalfProp41Provider ρ C lam ε supportConstant pairing → ∀ (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (scale : Fin (m + 1) → ℝ), R324WithinHalfEdgeCertificate res.state scale → ∃ (terminal : R324WithinHalfResidualPrefix ρ lam ε pairing) (terminalScale : Fin (m + 1) → ℝ), terminal.remaining = [] ∧ terminal.state.processed = r322AnalyticSchedule pairing ∧ R324WithinHalfEdgeCertificate terminal.state terminalScale

Phase-A quantitative closure: Proposition 4.1 is applied locally at every block and then iterated through the literal suffix. The conclusion is only a terminal slotwise certificate; no target-shaped global moment bound is assumed.