Paper Step 4: the two endpoint operations of one half-chain

Paper §4.2, Step 4 integrates the two external variables of a half-chain only after the signed primitive-interval removals are complete. This file is the small common seam for those endpoint operations. It deliberately does not introduce a route, trace, or scale ledger.

There are two ingredients.

• For a completed direct half-chain, both genuine boundary factors are Fourier-integrated exactly. The norm is taken only after both integrals.
• For a retained outgoing shortcut terminal, the endpoint-stop geometry is fed directly to the existing fixed-terminal ordinary-J theorem. Thus the shortcut branch pays exactly one ordinary-versus-inserted sacrifice, while a direct endpoint has sacrifice one.

The remaining global splice is intentionally not hidden here: its source density must first be identified with the separated endpoint form below (or with the retained-terminal form) after all interval coordinates have been removed.

Exact separated two-endpoint operation

@[reducible, inline]

abbrev Anderson4D.R324PaperHalfEndpointAnchors : Type

The two anchors of one half-chain, incoming first and outgoing second. Each pair consists of the ordinary endpoint anchor and the subtraction anchor used only in the shortcut branch.

Equations

• Anderson4D.R324PaperHalfEndpointAnchors = (Fin 2 → Anderson4D.T4 × Anderson4D.T4)

@[reducible, inline]

abbrev Anderson4D.R324PaperHalfEndpointCases : Type

The two paper endpoint cases of one half-chain.

Equations

• Anderson4D.R324PaperHalfEndpointCases = (Fin 2 → Anderson4D.SmoothCutoff.R324EndpointReductionCase)

def Anderson4D.r324PaperEndpointCaseShortcut : SmoothCutoff.R324EndpointReductionCase → Bool

The Boolean endpoint-kernel flag represented by a paper endpoint case.

Equations

• Anderson4D.r324PaperEndpointCaseShortcut Anderson4D.SmoothCutoff.R324EndpointReductionCase.directFourier = false
• Anderson4D.r324PaperEndpointCaseShortcut Anderson4D.SmoothCutoff.R324EndpointReductionCase.insertedSacrifice = true

noncomputable def Anderson4D.r324PaperHalfEndpointIntegrand (incomingMode outgoingMode : Z4) (anchors : R324PaperHalfEndpointAnchors) (cases : R324PaperHalfEndpointCases) (core : ℂ) (x y : T4) : ℂ

The endpoint-separated signed density for one half-chain. core is the complete signed primitive fibre left after Steps 1--3; in particular this definition does not move a norm inside that fibre.

Equations

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

theorem Anderson4D.integral_r324PaperHalfEndpointIntegrand (incomingMode outgoingMode : Z4) (anchors : R324PaperHalfEndpointAnchors) (cases : R324PaperHalfEndpointCases) (core : ℂ) : ∫ (x : T4), ∫ (y : T4), r324PaperHalfEndpointIntegrand incomingMode outgoingMode anchors cases core x y ∂paperMeasure ∂paperMeasure = r324EndpointCoefficient incomingMode (anchors 0).1 (anchors 0).2 (r324PaperEndpointCaseShortcut (cases 0)) * (r324EndpointCoefficient outgoingMode (anchors 1).1 (anchors 1).2 (r324PaperEndpointCaseShortcut (cases 1)) * core)

Both external integrations are evaluated before any norm is taken.

theorem Anderson4D.norm_integral_r324PaperHalfEndpointIntegrand (incomingMode outgoingMode : Z4) (anchors : R324PaperHalfEndpointAnchors) (cases : R324PaperHalfEndpointCases) (core : ℂ) : ‖∫ (x : T4), ∫ (y : T4), r324PaperHalfEndpointIntegrand incomingMode outgoingMode anchors cases core x y ∂paperMeasure ∂paperMeasure‖ = ‖r324EndpointCoefficient incomingMode (anchors 0).1 (anchors 0).2 (r324PaperEndpointCaseShortcut (cases 0))‖ * ‖r324EndpointCoefficient outgoingMode (anchors 1).1 (anchors 1).2 (r324PaperEndpointCaseShortcut (cases 1))‖ * ‖core‖

The first norm occurs after the two exact endpoint integrations.

Case-faithful ordinary-J sacrifice

noncomputable def Anderson4D.r324PaperHalfEndpointSacrifice (ε : ℝ) (cases : R324PaperHalfEndpointCases) : ℝ

The product of the two genuine ordinary-versus-inserted costs of one half-chain. A direct endpoint contributes exactly one.

Equations

• Anderson4D.r324PaperHalfEndpointSacrifice ε cases = Anderson4D.SmoothCutoff.r324EndpointPrimitiveSacrifice ε (cases 0) * Anderson4D.SmoothCutoff.r324EndpointPrimitiveSacrifice ε (cases 1)

theorem Anderson4D.r324PaperHalfEndpointSacrifice_nonneg (ε : ℝ) (cases : R324PaperHalfEndpointCases) : 0 ≤ r324PaperHalfEndpointSacrifice ε cases

theorem Anderson4D.r324PaperHalfEndpointSacrifice_eq_one_of_direct (ε : ℝ) (cases : R324PaperHalfEndpointCases) (hcases : ∀ (i : Fin 2), cases i = SmoothCutoff.R324EndpointReductionCase.directFourier) : r324PaperHalfEndpointSacrifice ε cases = 1

In the genuinely direct/direct branch the primitive sacrifice is definitionally one: no hidden uniform ε⁻² is charged.

theorem Anderson4D.r324PaperHalfEndpointSacrifice_eq_invSq_of_outgoing_inserted (ε : ℝ) (cases : R324PaperHalfEndpointCases) (hincoming : cases 0 = SmoothCutoff.R324EndpointReductionCase.directFourier) (houtgoing : cases 1 = SmoothCutoff.R324EndpointReductionCase.insertedSacrifice) : r324PaperHalfEndpointSacrifice ε cases = ε⁻¹ ^ 2

A single paired terminal endpoint contributes exactly one ε⁻² ordinary-J sacrifice.

theorem Anderson4D.r324PaperShortcutPrimitiveMajorant_le_sacrifice_mul_inserted (C lam supportConstant : ℝ) (n : ℕ) {ε : ℝ} (hε : 0 < ε) (z : T4) : primitiveKernelMajorant C lam ε supportConstant n z ≤ SmoothCutoff.r324EndpointPrimitiveSacrifice ε SmoothCutoff.R324EndpointReductionCase.insertedSacrifice * primitiveInsertedMajorant C lam ε supportConstant n z

Pointwise analytic bridge used after a paired terminal collapse: the ordinary primitive majorant is converted to the inserted majorant at the single outgoing endpoint's case cost.

theorem Anderson4D.r324PaperHalfEndpointSacrifice_le {ε : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (cases : R324PaperHalfEndpointCases) : r324PaperHalfEndpointSacrifice ε cases ≤ ε⁻¹ ^ 4

At most two exceptional endpoints occur in one half, hence the sharp uniform half-chain loss is ε⁻⁴. This does not charge a direct endpoint: its factor remains definitionally one in r324PaperHalfEndpointSacrifice.

Actual completed direct half-chain

theorem Anderson4D.R324WithinHalfResidualPrefix.integral_two_directBoundaryFactors_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hremaining : res.remaining = []) (hactive : res.state.active.Nonempty) (hincoming : res.state.edges 0 = greenFn) (houtgoing : res.state.edges (res.terminalOutgoingEdgeSlot hactive) = greenFn) (incomingMode outgoingMode : Z4) (v : Fin m → T4) (core : ℂ) : ∫ (x : T4), ∫ (y : T4), charT4 incomingMode x * ↑(res.incomingBoundaryFactor x y v) * (charT4 outgoingMode y * ↑(res.outgoingBoundaryFactor hactive x y v)) * core ∂paperMeasure ∂paperMeasure = translatedGreenMode incomingMode (res.terminalIncomingAnchor v) * (translatedGreenMode outgoingMode (res.terminalOutgoingAnchor hactive v) * core)

A completed half-chain whose two boundary edges are still free has the exact separated two-endpoint form. This is the direct/direct paper branch, with no ε-loss and no norm before either Fourier integration.

Actual retained outgoing-shortcut terminal

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointTerminalGeometry.integral_lamEps_pow_terminalOutgoingFourier_gap_eq_defect {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (data : R324WithinHalfEndpointTerminalGeometry pairing) (k : Z4) (x first : T4) (outer : ℂ) (hint : ∀ (gap : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder data.terminalData.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder data.terminalData.terminal.2) (↑κB) data.terminalContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminalData.terminal.2) ⋯ first (first - gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2)) => paperMeasure)) : ∫ (gap : T4), ↑(lamEps lam ε) ^ (2 * residualBlockOrder data.terminalData.terminal.2) * ∫ (r : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2) → T4), ∫ (y : T4), charT4 k y * (↑(data.terminalContext.rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder data.terminalContext.step.2)) => primitiveAssemble (residualBlockOrder data.terminalData.terminal.2) ⋯ first (first - gap) r j - y) * outer) ∂paperMeasure ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2)) => paperMeasure ∂paperMeasure = (↑(data.terminalContext.state.edges (r324WithinHalfPredecessorSlot data.terminalContext.state data.terminalContext.step) (x - first)) * ↑(paperSecondOrderModeDecay k) * charT4 k first * ∫ (gap : T4), ↑(primitiveKernelDiff ρ lam ε (residualBlockOrder data.terminalData.terminal.2) ⋯ data.terminalContext.internalEdges gap) * (charT4 (-k) gap - 1) ∂paperMeasure) * outer

Exact outgoing shortcut operation specialized to the endpoint-stop driver. Endpoint Fourier integration, internal primitive integration, and gap integration all occur before the resulting ordinary phase defect is exposed.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointTerminalGeometry.norm_integral_lamEps_pow_terminalOutgoingFourier_gap_le_scaled {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {C supportConstant : ℝ} (data : R324WithinHalfEndpointTerminalGeometry pairing) (scale : Fin (m + 1) → ℝ) (certificate : R324WithinHalfEdgeCertificate data.terminalContext.state scale) (k : Z4) (x first : T4) (outer : ℂ) (hint : ∀ (gap : T4) (κB : ↥(primitiveFullPairings (residualBlockOrder data.terminalData.terminal.2))), MeasureTheory.Integrable (fun (r : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder data.terminalData.terminal.2) (↑κB) data.terminalContext.internalEdges (primitiveAssemble (residualBlockOrder data.terminalData.terminal.2) ⋯ first (first - gap) r)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2)) => paperMeasure)) (hε : 0 < ε) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hprop : ∀ (H : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput (residualBlockOrder data.terminalData.terminal.2) H → MemEClassT4 (primitiveKernelDiff ρ lam ε (residualBlockOrder data.terminalData.terminal.2) ⋯ H) ∧ MemEClassT4 (primitiveKernelInsertedDiff ρ lam ε (residualBlockOrder data.terminalData.terminal.2) ⋯ H) ∧ PrimitiveKernelBounds ρ lam ε (residualBlockOrder data.terminalData.terminal.2) ⋯ H supportConstant C) : ‖∫ (gap : T4), ↑(lamEps lam ε) ^ (2 * residualBlockOrder data.terminalData.terminal.2) * ∫ (r : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2) → T4), ∫ (y : T4), charT4 k y * (↑(data.terminalContext.rawLocalIntegrand ρ ε (x - y) fun (j : Fin (2 * residualBlockOrder data.terminalContext.step.2)) => primitiveAssemble (residualBlockOrder data.terminalData.terminal.2) ⋯ first (first - gap) r j - y) * outer) ∂paperMeasure ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.terminalData.terminal.2 - 2)) => paperMeasure ∂paperMeasure‖ ≤ |data.terminalContext.state.edges (r324WithinHalfPredecessorSlot data.terminalContext.state data.terminalContext.step) (x - first)| * paperSecondOrderModeDecay k * (2 * r324WithinHalfInternalEdgeScaleProduct data.terminalContext scale * ∫ (gap : T4), primitiveKernelMajorant C lam ε supportConstant (residualBlockOrder data.terminalData.terminal.2) gap ∂paperMeasure) * ‖outer‖

Certificate-scaled numerical form of the retained outgoing shortcut. The exact endpoint, internal-coordinate, and terminal-gap integrations are performed first by the preceding theorem. Only then is the norm bounded by the ordinary Proposition 4.1 majorant, retaining the product of the actual internal edge scales exactly once.