Certificate-scaled ordinary primitive defect

The internal kernels present at a stopped within-half block are not normalized primitive inputs. Their individual inverse-square constants are stored in R324WithinHalfEdgeCertificate. This module extracts the generic form of the already proved incoming-exceptional estimate: normalize through that certificate, apply Proposition 4.1, and retain the product of the actual internal scales exactly once.

The norm is taken only after the complete signed primitive sum has been integrated. The value at the identity is discarded using atomlessness of paper Haar measure.

theorem Anderson4D.norm_incomingExceptionalPrimitiveDefect_le_scaled_of_certificate {ρ : SmoothCutoff} {C lam ε supportConstant : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} (ctx : R324WithinHalfStepContext κ) (scale : Fin (m + 1) → ℝ) (certificate : R324WithinHalfEdgeCertificate ctx.state scale) (hε : 0 < ε) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (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) (k : Z4) : ‖incomingExceptionalPrimitiveDefect ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges k‖ ≤ 2 * r324WithinHalfInternalEdgeScaleProduct ctx scale * ∫ (u : T4), primitiveKernelMajorant C lam ε supportConstant (residualBlockOrder ctx.step.2) u ∂paperMeasure

Generic certificate-scaled form of the ordinary-J Step-4 loss. This is the reusable local estimate for both incoming and outgoing shortcut terminals.

theorem Anderson4D.R324WithinHalfResidualPrefix.norm_incomingExceptionalHeadCollapseFactor_le_scaled {ρ : SmoothCutoff} {C lam ε supportConstant : ℝ} {m : ℕ} {κ : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε κ) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (scale : Fin (m + 1) → ℝ) (certificate : R324WithinHalfEdgeCertificate res.state scale) (hε : 0 < ε) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hprop : ∀ (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) (k : Z4) : ‖res.incomingExceptionalHeadCollapseFactor head tail hremaining k‖ ≤ 2 * r324WithinHalfInternalEdgeScaleProduct (res.headContext head tail hremaining) scale * ∫ (u : T4), primitiveKernelMajorant C lam ε supportConstant (residualBlockOrder head.2) u ∂paperMeasure

Certificate-scaled form of the complete incoming endpoint head factor. The Fourier multiplier is kept exact until the primitive defect has been formed; its norm is then bounded by one.