Automatic cosine integrability at a full-pairing terminal block #
The exact terminal cosine identity previously exposed the two real integrability premises needed for Bochner linearity. For a genuine full-pairing budget/geometry adapter these premises follow directly from the ordinary Proposition 4.1 bound:
- the adapter certificate makes every terminal internal edge measurable;
PrimitiveKernelBoundsdominates the resultingprimitiveKernelDiffby the integrable ordinary majorant; and- the real and imaginary parts of a torus character are bounded measurable multipliers.
Thus the terminal cosine identity below has no explicit hcos or hsin
input. No target moment estimate or routing output is assumed.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.integrable_terminalPrimitiveKernelDiff_of_bounds
{ρ : SmoothCutoff}
{C lam ε K A : ℝ}
{q : ℕ}
{κ : PartialPairing (Fin (2 * q))}
{budget : R324FullPairingBudgetStopTrace κ}
(data : R324FullPairingBudgetTerminalAdapter budget)
(hε : 0 < ε)
(supportConstant primitiveConstant : ℝ)
(hbound :
PrimitiveKernelBounds ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯
(data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges supportConstant
primitiveConstant)
:
MeasureTheory.Integrable
(primitiveKernelDiff ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯
(data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges)
paperMeasure
The ordinary Proposition 4.1 majorant makes the genuine terminal primitive kernel integrable. Measurability is supplied by the same edge certificate that was used to reach the terminal block.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.integrable_terminalPrimitiveKernelDiff_mul_characterCosSubOne_of_bounds
{ρ : SmoothCutoff}
{C lam ε K A : ℝ}
{q : ℕ}
{κ : PartialPairing (Fin (2 * q))}
{budget : R324FullPairingBudgetStopTrace κ}
(data : R324FullPairingBudgetTerminalAdapter budget)
(hε : 0 < ε)
(supportConstant primitiveConstant : ℝ)
(hbound :
PrimitiveKernelBounds ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯
(data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges supportConstant
primitiveConstant)
(β : Z4)
:
MeasureTheory.Integrable
(fun (u : T4) =>
primitiveKernelDiff ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯
(data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges u * (r324CharacterCos β u - 1))
paperMeasure
The cosine-minus-one weighted terminal primitive kernel is integrable. The multiplier has norm at most two.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.integrable_terminalPrimitiveKernelDiff_mul_characterSin_of_bounds
{ρ : SmoothCutoff}
{C lam ε K A : ℝ}
{q : ℕ}
{κ : PartialPairing (Fin (2 * q))}
{budget : R324FullPairingBudgetStopTrace κ}
(data : R324FullPairingBudgetTerminalAdapter budget)
(hε : 0 < ε)
(supportConstant primitiveConstant : ℝ)
(hbound :
PrimitiveKernelBounds ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯
(data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges supportConstant
primitiveConstant)
(β : Z4)
:
MeasureTheory.Integrable
(fun (u : T4) =>
primitiveKernelDiff ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯
(data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges u * r324CharacterSin β u)
paperMeasure
The sine-weighted terminal primitive kernel is integrable. The multiplier has norm at most one.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324FullPairingBudgetTerminalAdapter.integral_terminalPrimitiveKernelDiff_mul_negCharacterSubOne_eq_cos_of_bounds
{ρ : SmoothCutoff}
{C lam ε K A : ℝ}
{q : ℕ}
{κ : PartialPairing (Fin (2 * q))}
{budget : R324FullPairingBudgetStopTrace κ}
(data : R324FullPairingBudgetTerminalAdapter budget)
(hε : 0 < ε)
(supportConstant primitiveConstant : ℝ)
(hbound :
PrimitiveKernelBounds ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯
(data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges supportConstant
primitiveConstant)
(β : Z4)
:
∫ (u : T4), ↑(primitiveKernelDiff ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯
(data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges u) * (charT4 (-β) u - 1) ∂paperMeasure = ∫ (u : T4), ↑(primitiveKernelDiff ρ lam ε (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯
(data.geometry.trace.stopPrefix.headContext data.geometry.terminalData.terminal [] ⋯).internalEdges u * (r324CharacterCos β u - 1)) ∂paperMeasure
Terminal cosine identity with certificate-produced integrability.
The exact gap orientation is unchanged from the endpoint Fourier identity;
the adapter supplies 𝓔-membership and the Proposition 4.1 bound supplies
both Bochner-integrability premises.