Uniform endpoint-integrated boundary bounds #
The terminal edge certificate controls every actual boundary kernel by its
own inverse-square scale. After the external endpoint variables have been
integrated, this gives a mode-independent L¹ constant. No direct-Green
hypothesis and no estimate of the grouped internal core is used here.
theorem
Anderson4D.R324WithinHalfEdgeCertificate.integrable_edge
{m : ℕ}
{state : R324WithinHalfEdgeState m}
{scale : Fin (m + 1) → ℝ}
(cert : R324WithinHalfEdgeCertificate state scale)
(edge : Fin (m + 1))
:
MeasureTheory.Integrable (state.edges edge) paperMeasure
A certified named edge is genuinely integrable. The certificate is off-diagonal; the only omitted point is null for paper measure.
theorem
Anderson4D.R324WithinHalfEdgeCertificate.norm_integral_char_mul_edge_sub_le
{m : ℕ}
{state : R324WithinHalfEdgeState m}
{scale : Fin (m + 1) → ℝ}
(cert : R324WithinHalfEdgeCertificate state scale)
(edge : Fin (m + 1))
(k : Z4)
(anchor : T4)
:
A Fourier character cannot increase the L¹ bound of a certified
edge translated in the x - anchor orientation.
theorem
Anderson4D.R324WithinHalfEdgeCertificate.norm_integral_char_mul_edge_sub_left_le
{m : ℕ}
{state : R324WithinHalfEdgeState m}
{scale : Fin (m + 1) → ℝ}
(cert : R324WithinHalfEdgeCertificate state scale)
(edge : Fin (m + 1))
(k : Z4)
(anchor : T4)
:
The corresponding bound in the anchor - x orientation.
theorem
Anderson4D.R324WithinHalfResidualPrefix.incomingBoundaryFactor_terminal_eq_edgeKernel
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(hterminal : res.remaining = [])
(hactive : res.state.active.Nonempty)
(x y : T4)
(v : Fin m → T4)
:
At a completed nonempty half, the incoming boundary factor is the actual stored edge kernel translated from the first surviving anchor.
theorem
Anderson4D.R324WithinHalfResidualPrefix.outgoingBoundaryFactor_terminal_eq_edgeKernel
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(hterminal : res.remaining = [])
(hactive : res.state.active.Nonempty)
(x y : T4)
(v : Fin m → T4)
:
res.outgoingBoundaryFactor hactive x y v = res.state.edges (res.terminalOutgoingEdgeSlot hactive) (res.terminalOutgoingAnchor hactive v - y)
The outgoing boundary factor is the actual stored terminal-slot kernel translated from the last surviving anchor.
theorem
Anderson4D.R324TwoHalfTerminalData.leftBoundaryModeCoefficient_eq_terminalEdgeModes
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
(hleft : terminal.left.state.active.Nonempty)
(α β : Z4)
(vl : terminal.left.SurvivingCoordinate → T4)
:
terminal.leftBoundaryModeCoefficient hleft α β vl = (∫ (x : T4), charT4 α x * ↑(terminal.left.state.edges 0
(x - terminal.left.terminalIncomingAnchor (terminal.left.reconstruct vl))) ∂paperMeasure) * ∫ (y : T4), charT4 β y * ↑(terminal.left.state.edges (terminal.left.terminalOutgoingEdgeSlot hleft)
(terminal.left.terminalOutgoingAnchor hleft (terminal.left.reconstruct vl) - y)) ∂paperMeasure
The completed left boundary coefficient is exactly the product of the two Fourier coefficients of its actual stored boundary kernels.
theorem
Anderson4D.R324TwoHalfTerminalData.rightBoundaryModeCoefficient_eq_terminalEdgeModes
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
(hright : terminal.right.state.active.Nonempty)
(α β : Z4)
(vr : terminal.right.SurvivingCoordinate → T4)
:
terminal.rightBoundaryModeCoefficient hright α β vr = (∫ (z : T4), charT4 (-α) z * ↑(terminal.right.state.edges 0
(z - terminal.right.terminalIncomingAnchor (terminal.right.reconstruct vr))) ∂paperMeasure) * ∫ (w : T4), charT4 (-β) w * ↑(terminal.right.state.edges (terminal.right.terminalOutgoingEdgeSlot hright)
(terminal.right.terminalOutgoingAnchor hright (terminal.right.reconstruct vr) - w)) ∂paperMeasure
Right-half analogue, with the literal modes (-α,-β).
theorem
Anderson4D.R324TwoHalfTerminalData.norm_leftBoundaryModeCoefficient_le_terminalScale
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
(hleft : terminal.left.state.active.Nonempty)
{scale : Fin (m + 1) → ℝ}
(cert : R324WithinHalfEdgeCertificate terminal.left.state scale)
(α β : Z4)
(vl : terminal.left.SurvivingCoordinate → T4)
:
‖terminal.leftBoundaryModeCoefficient hleft α β vl‖ ≤ scale 0 * scale (terminal.left.terminalOutgoingEdgeSlot hleft) * invSqKerMass ^ 2
Uniform left boundary coefficient bound from an arbitrary terminal certificate. It is independent of the external modes and keeps the grouped internal core entirely outside the estimate.
theorem
Anderson4D.R324TwoHalfTerminalData.norm_rightBoundaryModeCoefficient_le_terminalScale
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
(terminal : R324TwoHalfTerminalData ρ lam ε κp κm)
(hright : terminal.right.state.active.Nonempty)
{scale : Fin (m + 1) → ℝ}
(cert : R324WithinHalfEdgeCertificate terminal.right.state scale)
(α β : Z4)
(vr : terminal.right.SurvivingCoordinate → T4)
:
‖terminal.rightBoundaryModeCoefficient hright α β vr‖ ≤ scale 0 * scale (terminal.right.terminalOutgoingEdgeSlot hright) * invSqKerMass ^ 2
Uniform right boundary coefficient bound from its terminal certificate.
Stored-certificate API for certified traces #
theorem
Anderson4D.R324TwoHalfTerminalData.norm_leftBoundaryModeCoefficient_le_storedTerminalScale
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{leftRes : R324WithinHalfResidualPrefix ρ lam ε κp}
{rightRes : R324WithinHalfResidualPrefix ρ lam ε κm}
{leftInitialScale rightInitialScale : Fin (m + 1) → ℝ}
(leftTrace : leftRes.R324WithinHalfCertifiedAnalyticTrace leftInitialScale)
(rightTrace : rightRes.R324WithinHalfCertifiedAnalyticTrace rightInitialScale)
(hleft : leftTrace.terminalPrefix.state.active.Nonempty)
(α β : Z4)
(vl : leftTrace.terminalPrefix.SurvivingCoordinate → T4)
:
let terminal := ofCertifiedTraces leftTrace rightTrace;
‖terminal.leftBoundaryModeCoefficient hleft α β vl‖ ≤ leftTrace.terminalScale 0 * leftTrace.terminalScale (leftTrace.terminalPrefix.terminalOutgoingEdgeSlot hleft) * invSqKerMass ^ 2
The requested left trace-level interface. The two scales are exactly
the incoming slot 0 and the outgoing terminal slot stored at the end of
the Phase-A trace.
theorem
Anderson4D.R324TwoHalfTerminalData.norm_rightBoundaryModeCoefficient_le_storedTerminalScale
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{leftRes : R324WithinHalfResidualPrefix ρ lam ε κp}
{rightRes : R324WithinHalfResidualPrefix ρ lam ε κm}
{leftInitialScale rightInitialScale : Fin (m + 1) → ℝ}
(leftTrace : leftRes.R324WithinHalfCertifiedAnalyticTrace leftInitialScale)
(rightTrace : rightRes.R324WithinHalfCertifiedAnalyticTrace rightInitialScale)
(hright : rightTrace.terminalPrefix.state.active.Nonempty)
(α β : Z4)
(vr : rightTrace.terminalPrefix.SurvivingCoordinate → T4)
:
let terminal := ofCertifiedTraces leftTrace rightTrace;
‖terminal.rightBoundaryModeCoefficient hright α β vr‖ ≤ rightTrace.terminalScale 0 * rightTrace.terminalScale (rightTrace.terminalPrefix.terminalOutgoingEdgeSlot hright) * invSqKerMass ^ 2
Right trace-level analogue.