The first Step-4 unit after an incoming exceptional Fourier stop #
At an exceptional incoming stop, endpoint Fourier integration leaves its character at the first point of the retained primitive block. This file performs the next local operation, before any suffix iteration:
- expose the exact Green multiplier and the retained head character;
- route that character across the outgoing signed difference;
- identify the resulting gap factor as
charT4 (-k) u - 1, foru = z - w; - reduce this complex defect to the real cosine defect and charge it with the ordinary half of Proposition 4.1.
The after-head coordinates and their outer factor remain fixed throughout. No claim about propagation of the transported character through a later suffix block is made here.
Exposing the phase left by the incoming endpoint integral #
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalStopFourierDensity_eq_phase
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{κ : PartialPairing (Fin m)}
{initialScale : Fin (m + 1) → ℝ}
{Ω : Type u_1}
(data : R324IncomingExceptionalStopTraceAssembly κ initialScale)
(k : Z4)
(y : Ω → T4)
(postOuter : Ω → ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ)
(ω : Ω)
(t : Fin (2 * residualBlockOrder data.terminal.2) → T4)
(v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)
:
data.incomingExceptionalStopFourierDensity k y postOuter (ω, t, v) = ↑(paperSecondOrderModeDecay k) * charT4 k (t ⟨0, ⋯⟩) * data.stopContext.incomingErasedTranslatedRawLocalCore ρ ε
(data.trace.stopPrefix.headSuccessorPoint data.terminal data.suffix ⋯ 0 (y ω) v) t * (↑(data.trace.stopPrefix.headOuterFactor data.terminal data.suffix ⋯ ρ ε 0 (y ω) v) * postOuter ω v)
The stop Fourier density contains exactly one head character and one paper Green multiplier. Everything depending on the after-head tuple is left untouched.
Routing a head character through the outgoing difference #
The Fourier mode of the outgoing edge, translated to the genuine after-head successor. This is the factor that carries the character into the remaining suffix.
Equations
- Anderson4D.incomingExceptionalTransportedMode k a H = ∫ (q : Anderson4D.T4), Anderson4D.charT4 k q * ↑(H (q - a)) ∂Anderson4D.paperMeasure
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalTransportedMode_eq_translatedGreenMode
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{κ : PartialPairing (Fin m)}
{initialScale : Fin (m + 1) → ℝ}
(data : R324IncomingExceptionalStopTraceAssembly κ initialScale)
(k : Z4)
(a : T4)
:
incomingExceptionalTransportedMode k a (data.stopContext.state.edges data.stopContext.outgoingSlot) = translatedGreenMode k a
At a genuine exceptional stop the outgoing edge of the retained head is still the free Green kernel. Hence its transported mode is exactly the standard translated Green mode.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integrable_char_mul_stopOutgoing_sub
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{κ : PartialPairing (Fin m)}
{initialScale : Fin (m + 1) → ℝ}
(data : R324IncomingExceptionalStopTraceAssembly κ initialScale)
(k : Z4)
(a : T4)
:
MeasureTheory.Integrable
(fun (q : T4) => charT4 k q * ↑(data.stopContext.state.edges data.stopContext.outgoingSlot (q - a))) paperMeasure
The outgoing Fourier section required by the exact head theorem is automatically integrable at a genuine exceptional stop.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalTransportedMode_eq_decay_mul_afterHeadAnchor
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{κ : PartialPairing (Fin m)}
{initialScale : Fin (m + 1) → ℝ}
{Ω : Type u_1}
(data : R324IncomingExceptionalStopTraceAssembly κ initialScale)
(k : Z4)
(y : Ω → T4)
(ω : Ω)
(v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)
:
incomingExceptionalTransportedMode k (data.trace.stopPrefix.headSuccessorPoint data.terminal data.suffix ⋯ 0 (y ω) v)
(data.stopContext.state.edges data.stopContext.outgoingSlot) = ↑(paperSecondOrderModeDecay k) * charT4 k ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).incomingPhaseAnchor 0 (y ω) v)
The genuine post-head successor is the phase anchor of the residual suffix. The outgoing mode therefore contributes one further Green decay and places the character on that named anchor.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.paperDecay_mul_incomingExceptionalTransportedMode_mul_eq_anchor
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{κ : PartialPairing (Fin m)}
{initialScale : Fin (m + 1) → ℝ}
{Ω : Type u_1}
(data : R324IncomingExceptionalStopTraceAssembly κ initialScale)
(k : Z4)
(y : Ω → T4)
(ω : Ω)
(v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)
(payload : ℂ)
:
↑(paperSecondOrderModeDecay k) * incomingExceptionalTransportedMode k
(data.trace.stopPrefix.headSuccessorPoint data.terminal data.suffix ⋯ 0 (y ω) v)
(data.stopContext.state.edges data.stopContext.outgoingSlot) * payload = ↑(paperSecondOrderModeDecay k) ^ 2 * charT4 k ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).incomingPhaseAnchor 0 (y ω) v) * payload
Consumer form for the exact head theorem: the incoming Green endpoint and the genuine outgoing Green edge contribute two paper second-order decays, while all remaining scalar data is carried unchanged.
theorem
Anderson4D.R324WithinHalfStepContext.incomingErasedTranslatedRawLocalCore_eq_completePrimitive_mul_outgoingDifference
{m : ℕ}
{κ : PartialPairing (Fin m)}
(ctx : R324WithinHalfStepContext κ)
(ρ : SmoothCutoff)
(ε : ℝ)
(a : T4)
(t : Fin (2 * residualBlockOrder ctx.step.2) → T4)
:
ctx.incomingErasedTranslatedRawLocalCore ρ ε a t = ↑((∑ κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2)),
detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges t) * (ctx.state.edges ctx.outgoingSlot (t (primitiveLast (residualBlockOrder ctx.step.2) ⋯) - a) - ctx.state.edges ctx.outgoingSlot (t ⟨0, ⋯⟩ - a)))
The post-Fourier raw head core is the complete signed primitive sum times its literal outgoing edge difference. This is the pointwise bridge from the genuine stop density to the standard Proposition 4.1 kernel.
theorem
Anderson4D.R324WithinHalfStepContext.lamEps_pow_integral_incomingErasedTranslatedRawLocalCore_eq
{m : ℕ}
{κ : PartialPairing (Fin m)}
(ctx : R324WithinHalfStepContext κ)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(a first last : T4)
(hint :
∀ (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))),
MeasureTheory.Integrable
(fun (r : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) =>
detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges
(primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ first last r))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure))
:
(↑(lamEps lam ε) ^ (2 * residualBlockOrder ctx.step.2) * ∫ (r : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4), ctx.incomingErasedTranslatedRawLocalCore ρ ε a
(primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ first last
r) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure) = ↑(primitiveKernelDiff ρ lam ε (residualBlockOrder ctx.step.2) ⋯ ctx.internalEdges (first - last) * (ctx.state.edges ctx.outgoingSlot (last - a) - ctx.state.edges ctx.outgoingSlot (first - a)))
Integrating the internal coordinates of the genuine post-Fourier head core produces the ordinary primitive kernel, while the outgoing signed difference remains literal.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_integral_incomingExceptionalStopFourierDensity_internal_eq
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{κ : PartialPairing (Fin m)}
{initialScale : Fin (m + 1) → ℝ}
{Ω : Type u_1}
(data : R324IncomingExceptionalStopTraceAssembly κ initialScale)
(k : Z4)
(y : Ω → T4)
(postOuter : Ω → ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ)
(ω : Ω)
(v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)
(gap first : T4)
(hG : ∀ (j : Fin (2 * residualBlockOrder data.stopContext.step.2 - 1)), MemEClassT4 (data.stopContext.internalEdges j))
(hint :
∀ (κB : ↥(primitiveFullPairings (residualBlockOrder data.terminal.2))),
MeasureTheory.Integrable
(fun (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4) =>
detJclosedIntegrandWith ρ ε (2 * residualBlockOrder data.terminal.2) (↑κB) data.stopContext.internalEdges
(primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure))
:
(↑(lamEps lam ε) ^ (2 * residualBlockOrder data.terminal.2) * ∫ (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4), data.incomingExceptionalStopFourierDensity k y postOuter
(ω, primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r, v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure) = ↑(paperSecondOrderModeDecay k) * charT4 k first * ↑(primitiveKernelDiff ρ lam ε (residualBlockOrder data.terminal.2) ⋯ data.stopContext.internalEdges gap) * ↑(data.stopContext.state.edges data.stopContext.outgoingSlot
(first + gap - data.trace.stopPrefix.headSuccessorPoint data.terminal data.suffix ⋯ 0 (y ω) v) - data.stopContext.state.edges data.stopContext.outgoingSlot
(first - data.trace.stopPrefix.headSuccessorPoint data.terminal data.suffix ⋯ 0 (y ω) v)) * (↑(data.trace.stopPrefix.headOuterFactor data.terminal data.suffix ⋯ ρ ε 0 (y ω) v) * postOuter ω v)
Fixed after-head coordinates, fixed gap, and fixed first endpoint:
the genuine stop Fourier density integrates in its internal primitive
coordinates to the ordinary primitiveKernelDiff, with the transported
head character and outgoing edge difference still exact.
theorem
Anderson4D.integrable_char_mul_outgoing_shift_of_base
(k : Z4)
(a u : T4)
(H : T4 → ℝ)
(hbase : MeasureTheory.Integrable (fun (w : T4) => charT4 k w * ↑(H (w - a))) paperMeasure)
:
MeasureTheory.Integrable (fun (w : T4) => charT4 k w * ↑(H (w + u - a))) paperMeasure
For the gap orientation u = z - w, translating the z term of the
outgoing signed difference leaves exactly
charT4 (-k) u - 1. The assumptions are only those needed to split the
Bochner integral of the signed difference.
theorem
Anderson4D.integral_char_mul_outgoingDifference_eq_defect_mul_transportedMode
(k : Z4)
(a u : T4)
(H : T4 → ℝ)
(hbase : MeasureTheory.Integrable (fun (w : T4) => charT4 k w * ↑(H (w - a))) paperMeasure)
:
For the gap orientation u = z - w, translating the z term of the
outgoing signed difference leaves exactly
charT4 (-k) u - 1. The sole integrability premise is the untranslated
outgoing Fourier section; translation invariance supplies the shifted
section automatically.
theorem
Anderson4D.integral_kernel_mul_char_outgoingDifference_eq_transportedMode_mul_defect
(k : Z4)
(a : T4)
(H J : T4 → ℝ)
(hbase : MeasureTheory.Integrable (fun (w : T4) => charT4 k w * ↑(H (w - a))) paperMeasure)
:
After the outgoing coordinate is integrated, the whole two-endpoint phase is the transported Fourier mode times the one-variable primitive defect. This is the exact transported/base-plus-defect decomposition used before taking any norm.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integral_lamEps_pow_incomingExceptionalStopFourierDensity_head_eq_transportedMode_mul_defect
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{κ : PartialPairing (Fin m)}
{initialScale : Fin (m + 1) → ℝ}
{Ω : Type u_1}
(data : R324IncomingExceptionalStopTraceAssembly κ initialScale)
(k : Z4)
(y : Ω → T4)
(postOuter : Ω → ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ)
(ω : Ω)
(v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)
(hG : ∀ (j : Fin (2 * residualBlockOrder data.stopContext.step.2 - 1)), MemEClassT4 (data.stopContext.internalEdges j))
(hint :
∀ (gap first : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder data.terminal.2))),
MeasureTheory.Integrable
(fun (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4) =>
detJclosedIntegrandWith ρ ε (2 * residualBlockOrder data.terminal.2) (↑κB) data.stopContext.internalEdges
(primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure))
(hbase :
MeasureTheory.Integrable
(fun (first : T4) =>
charT4 k first * ↑(data.stopContext.state.edges data.stopContext.outgoingSlot
(first - data.trace.stopPrefix.headSuccessorPoint data.terminal data.suffix ⋯ 0 (y ω) v)))
paperMeasure)
:
∫ (gap : T4), ∫ (first : T4), ↑(lamEps lam ε) ^ (2 * residualBlockOrder data.terminal.2) * ∫ (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4), data.incomingExceptionalStopFourierDensity k y postOuter
(ω, primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r, v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) =>
paperMeasure ∂paperMeasure ∂paperMeasure = ↑(paperSecondOrderModeDecay k) * incomingExceptionalTransportedMode k
(data.trace.stopPrefix.headSuccessorPoint data.terminal data.suffix ⋯ 0 (y ω) v)
(data.stopContext.state.edges data.stopContext.outgoingSlot) * incomingExceptionalPrimitiveDefect ρ lam ε (residualBlockOrder data.terminal.2) ⋯ data.stopContext.internalEdges
k * (↑(data.trace.stopPrefix.headOuterFactor data.terminal data.suffix ⋯ ρ ε 0 (y ω) v) * postOuter ω v)
Exact fixed-post head decomposition.
The actual incoming exceptional stop density is integrated in the
reindexed head coordinates
(gap, first, internal), where the last endpoint is first + gap.
The result is the transported outgoing Fourier mode times the single
ordinary primitive defect. No norm and no suffix estimate occurs in this
identity.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_integral_incomingExceptionalStopFourierDensity_head_eq_transportedMode_mul_defect
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{κ : PartialPairing (Fin m)}
{initialScale : Fin (m + 1) → ℝ}
{Ω : Type u_1}
(data : R324IncomingExceptionalStopTraceAssembly κ initialScale)
(k : Z4)
(y : Ω → T4)
(postOuter : Ω → ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ)
(ω : Ω)
(v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)
(hhead :
MeasureTheory.Integrable
(fun (t : Fin (2 * residualBlockOrder data.terminal.2) → T4) =>
data.incomingExceptionalStopFourierDensity k y postOuter (ω, t, v))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2)) => paperMeasure))
(hG : ∀ (j : Fin (2 * residualBlockOrder data.stopContext.step.2 - 1)), MemEClassT4 (data.stopContext.internalEdges j))
(hint :
∀ (gap first : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder data.terminal.2))),
MeasureTheory.Integrable
(fun (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4) =>
detJclosedIntegrandWith ρ ε (2 * residualBlockOrder data.terminal.2) (↑κB) data.stopContext.internalEdges
(primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure))
(hbase :
MeasureTheory.Integrable
(fun (first : T4) =>
charT4 k first * ↑(data.stopContext.state.edges data.stopContext.outgoingSlot
(first - data.trace.stopPrefix.headSuccessorPoint data.terminal data.suffix ⋯ 0 (y ω) v)))
paperMeasure)
:
(↑(lamEps lam ε) ^ (2 * residualBlockOrder data.terminal.2) * ∫ (t : Fin (2 * residualBlockOrder data.terminal.2) → T4), data.incomingExceptionalStopFourierDensity k y postOuter
(ω, t, v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2)) => paperMeasure) = ↑(paperSecondOrderModeDecay k) * incomingExceptionalTransportedMode k
(data.trace.stopPrefix.headSuccessorPoint data.terminal data.suffix ⋯ 0 (y ω) v)
(data.stopContext.state.edges data.stopContext.outgoingSlot) * incomingExceptionalPrimitiveDefect ρ lam ε (residualBlockOrder data.terminal.2) ⋯ data.stopContext.internalEdges
k * (↑(data.trace.stopPrefix.headOuterFactor data.terminal data.suffix ⋯ ρ ε 0 (y ω) v) * postOuter ω v)
Original-head-measure form of the preceding decomposition. The measure-preserving primitive-head gap shear is applied once, and the perturbative power remains outside the raw head integral until that exact reindexing has been performed.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_integral_incomingExceptionalStopFourierDensity_head_eq_decay_sq_mul_anchor
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{κ : PartialPairing (Fin m)}
{initialScale : Fin (m + 1) → ℝ}
{Ω : Type u_1}
(data : R324IncomingExceptionalStopTraceAssembly κ initialScale)
(k : Z4)
(y : Ω → T4)
(postOuter : Ω → ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) → ℂ)
(ω : Ω)
(v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)
(hhead :
MeasureTheory.Integrable
(fun (t : Fin (2 * residualBlockOrder data.terminal.2) → T4) =>
data.incomingExceptionalStopFourierDensity k y postOuter (ω, t, v))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2)) => paperMeasure))
(hG : ∀ (j : Fin (2 * residualBlockOrder data.stopContext.step.2 - 1)), MemEClassT4 (data.stopContext.internalEdges j))
(hint :
∀ (gap first : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder data.terminal.2))),
MeasureTheory.Integrable
(fun (r : Fin (2 * residualBlockOrder data.terminal.2 - 2) → T4) =>
detJclosedIntegrandWith ρ ε (2 * residualBlockOrder data.terminal.2) (↑κB) data.stopContext.internalEdges
(primitiveAssemble (residualBlockOrder data.terminal.2) ⋯ first (first + gap) r))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2 - 2)) => paperMeasure))
:
(↑(lamEps lam ε) ^ (2 * residualBlockOrder data.terminal.2) * ∫ (t : Fin (2 * residualBlockOrder data.terminal.2) → T4), data.incomingExceptionalStopFourierDensity k y postOuter
(ω, t, v) ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminal.2)) => paperMeasure) = ↑(paperSecondOrderModeDecay k) ^ 2 * charT4 k ((data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).incomingPhaseAnchor 0 (y ω) v) * incomingExceptionalPrimitiveDefect ρ lam ε (residualBlockOrder data.terminal.2) ⋯ data.stopContext.internalEdges
k * (↑(data.trace.stopPrefix.headOuterFactor data.terminal data.suffix ⋯ ρ ε 0 (y ω) v) * postOuter ω v)
Genuine-stop anchor form. The outgoing-section integrability premise is discharged by the untouched Green edge, and the exact coefficient is the square of the paper second-order decay.
The ordinary Step-4 charge #
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.integrable_incomingExceptionalPrimitiveDefect_of_prop41
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{κ : PartialPairing (Fin m)}
{initialScale : Fin (m + 1) → ℝ}
(data : R324IncomingExceptionalStopTraceAssembly κ initialScale)
(hε : 0 < ε)
(hlog : 0 < |Real.log ε|)
(supportConstant : ℝ)
(hC : 0 ≤ C)
(hlam : 0 ≤ lam)
(hprop : R324WithinHalfProp41Provider ρ C lam ε supportConstant κ)
(k : Z4)
:
MeasureTheory.Integrable
(fun (u : T4) =>
↑(primitiveKernelDiff ρ lam ε (residualBlockOrder data.terminal.2) ⋯ data.stopContext.internalEdges u) * (charT4 (-k) u - 1))
paperMeasure
The stored stop certificate and the normalized Proposition 4.1 provider make the exact complex defect density integrable.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.norm_incomingExceptionalPrimitiveDefect_le_scaled_of_prop41
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{κ : PartialPairing (Fin m)}
{initialScale : Fin (m + 1) → ℝ}
(data : R324IncomingExceptionalStopTraceAssembly κ initialScale)
(hε : 0 < ε)
(supportConstant : ℝ)
(hC : 0 ≤ C)
(hlam : 0 ≤ lam)
(hprop : R324WithinHalfProp41Provider ρ C lam ε supportConstant κ)
(k : Z4)
:
‖incomingExceptionalPrimitiveDefect ρ lam ε (residualBlockOrder data.terminal.2) ⋯ data.stopContext.internalEdges k‖ ≤ 2 * r324WithinHalfInternalEdgeScaleProduct data.stopContext data.stopScale * ∫ (u : T4), primitiveKernelMajorant C lam ε supportConstant (residualBlockOrder data.terminal.2) u ∂paperMeasure
Certificate-scaled incoming Step-4 charge.
The raw internal head edges are normalized through the stored stop certificate before Proposition 4.1 is used. Their positive scale product appears exactly once. The value at the identity is discarded only through atomlessness of paper Haar measure.
theorem
Anderson4D.integrable_incomingExceptionalPrimitiveKernelDiff_of_bounds
(ρ : SmoothCutoff)
(lam ε : ℝ)
(n : ℕ)
(hn : 1 ≤ n)
(G : Fin (2 * n - 1) → T4 → ℝ)
(hGmeas : ∀ (j : Fin (2 * n - 1)), Measurable (G j))
(supportConstant primitiveConstant : ℝ)
(hε : 0 < ε)
(hbound : PrimitiveKernelBounds ρ lam ε n hn G supportConstant primitiveConstant)
:
MeasureTheory.Integrable (primitiveKernelDiff ρ lam ε n hn G) paperMeasure
Measurable primitive inputs and the ordinary Proposition 4.1 majorant make the primitive gap kernel integrable.
theorem
Anderson4D.integrable_incomingExceptionalPrimitiveKernelDiff_mul_characterCosSubOne_of_bounds
(ρ : SmoothCutoff)
(lam ε : ℝ)
(n : ℕ)
(hn : 1 ≤ n)
(G : Fin (2 * n - 1) → T4 → ℝ)
(hGmeas : ∀ (j : Fin (2 * n - 1)), Measurable (G j))
(supportConstant primitiveConstant : ℝ)
(hε : 0 < ε)
(hbound : PrimitiveKernelBounds ρ lam ε n hn G supportConstant primitiveConstant)
(k : Z4)
:
MeasureTheory.Integrable (fun (u : T4) => primitiveKernelDiff ρ lam ε n hn G u * (r324CharacterCos k u - 1))
paperMeasure
The cosine defect is integrable under the same ordinary majorant.
theorem
Anderson4D.integrable_incomingExceptionalPrimitiveKernelDiff_mul_characterSin_of_bounds
(ρ : SmoothCutoff)
(lam ε : ℝ)
(n : ℕ)
(hn : 1 ≤ n)
(G : Fin (2 * n - 1) → T4 → ℝ)
(hGmeas : ∀ (j : Fin (2 * n - 1)), Measurable (G j))
(supportConstant primitiveConstant : ℝ)
(hε : 0 < ε)
(hbound : PrimitiveKernelBounds ρ lam ε n hn G supportConstant primitiveConstant)
(k : Z4)
:
MeasureTheory.Integrable (fun (u : T4) => primitiveKernelDiff ρ lam ε n hn G u * r324CharacterSin k u) paperMeasure
The sine component is integrable under the same ordinary majorant.
theorem
Anderson4D.incomingExceptionalPrimitiveDefect_eq_cos
(ρ : SmoothCutoff)
(lam ε : ℝ)
(n : ℕ)
(hn : 1 ≤ n)
(G : Fin (2 * n - 1) → T4 → ℝ)
(hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j))
(k : Z4)
(hcos :
MeasureTheory.Integrable (fun (u : T4) => primitiveKernelDiff ρ lam ε n hn G u * (r324CharacterCos k u - 1))
paperMeasure)
(hsin :
MeasureTheory.Integrable (fun (u : T4) => primitiveKernelDiff ρ lam ε n hn G u * r324CharacterSin (-k) u)
paperMeasure)
:
incomingExceptionalPrimitiveDefect ρ lam ε n hn G k = ∫ (u : T4), ↑(primitiveKernelDiff ρ lam ε n hn G u * (r324CharacterCos k u - 1)) ∂paperMeasure
𝓔 symmetry removes the sine part of the incoming exceptional defect.
The orientation remains charT4 (-k) u - 1.
theorem
Anderson4D.norm_incomingExceptionalPrimitiveDefect_le_two_mul
(ρ : SmoothCutoff)
(lam ε : ℝ)
(n : ℕ)
(hn : 1 ≤ n)
(G : Fin (2 * n - 1) → T4 → ℝ)
(supportConstant primitiveConstant : ℝ)
(hε : 0 < ε)
(hbound : PrimitiveKernelBounds ρ lam ε n hn G supportConstant primitiveConstant)
(hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j))
(k : Z4)
(hcos :
MeasureTheory.Integrable (fun (u : T4) => primitiveKernelDiff ρ lam ε n hn G u * (r324CharacterCos k u - 1))
paperMeasure)
(hsin :
MeasureTheory.Integrable (fun (u : T4) => primitiveKernelDiff ρ lam ε n hn G u * r324CharacterSin (-k) u)
paperMeasure)
:
‖incomingExceptionalPrimitiveDefect ρ lam ε n hn G k‖ ≤ 2 * ∫ (u : T4), primitiveKernelMajorant primitiveConstant lam ε supportConstant n u ∂paperMeasure
The ordinary half of Proposition 4.1 charges the whole complex defect. There is no additional frequency gain and no inserted-kernel estimate in this branch.
theorem
Anderson4D.norm_incomingExceptionalPrimitiveDefect_le_two_mul_of_bounds
(ρ : SmoothCutoff)
(lam ε : ℝ)
(n : ℕ)
(hn : 1 ≤ n)
(G : Fin (2 * n - 1) → T4 → ℝ)
(hGmeas : ∀ (j : Fin (2 * n - 1)), Measurable (G j))
(hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j))
(supportConstant primitiveConstant : ℝ)
(hε : 0 < ε)
(hbound : PrimitiveKernelBounds ρ lam ε n hn G supportConstant primitiveConstant)
(k : Z4)
:
‖incomingExceptionalPrimitiveDefect ρ lam ε n hn G k‖ ≤ 2 * ∫ (u : T4), primitiveKernelMajorant primitiveConstant lam ε supportConstant n u ∂paperMeasure
Certificate-ready form: measurability and the ordinary
PrimitiveKernelBounds premise produce both cosine-seam integrability
requirements.
theorem
Anderson4D.norm_transportedMode_mul_incomingExceptionalPrimitiveDefect_le
(ρ : SmoothCutoff)
(lam ε : ℝ)
(n : ℕ)
(hn : 1 ≤ n)
(G : Fin (2 * n - 1) → T4 → ℝ)
(supportConstant primitiveConstant : ℝ)
(hε : 0 < ε)
(hbound : PrimitiveKernelBounds ρ lam ε n hn G supportConstant primitiveConstant)
(hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j))
(k : Z4)
(a : T4)
(H : T4 → ℝ)
(hcos :
MeasureTheory.Integrable (fun (u : T4) => primitiveKernelDiff ρ lam ε n hn G u * (r324CharacterCos k u - 1))
paperMeasure)
(hsin :
MeasureTheory.Integrable (fun (u : T4) => primitiveKernelDiff ρ lam ε n hn G u * r324CharacterSin (-k) u)
paperMeasure)
:
‖incomingExceptionalTransportedMode k a H * incomingExceptionalPrimitiveDefect ρ lam ε n hn G k‖ ≤ ‖incomingExceptionalTransportedMode k a H‖ * (2 * ∫ (u : T4), primitiveKernelMajorant primitiveConstant lam ε supportConstant n u ∂paperMeasure)
The local head output is the norm of the transported suffix mode times the ordinary Step-4 charge.
theorem
Anderson4D.norm_transportedMode_mul_incomingExceptionalPrimitiveDefect_le_of_bounds
(ρ : SmoothCutoff)
(lam ε : ℝ)
(n : ℕ)
(hn : 1 ≤ n)
(G : Fin (2 * n - 1) → T4 → ℝ)
(hGmeas : ∀ (j : Fin (2 * n - 1)), Measurable (G j))
(hG : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j))
(supportConstant primitiveConstant : ℝ)
(hε : 0 < ε)
(hbound : PrimitiveKernelBounds ρ lam ε n hn G supportConstant primitiveConstant)
(k : Z4)
(a : T4)
(H : T4 → ℝ)
:
‖incomingExceptionalTransportedMode k a H * incomingExceptionalPrimitiveDefect ρ lam ε n hn G k‖ ≤ ‖incomingExceptionalTransportedMode k a H‖ * (2 * ∫ (u : T4), primitiveKernelMajorant primitiveConstant lam ε supportConstant n u ∂paperMeasure)
Certificate-ready local head bound with no explicit cosine or sine integrability premises.