Fourier coefficients of direct terminal boundary legs

This file identifies a completed sparse half-chain boundary leg with one translated Green kernel whenever its reachable edge state still stores the free Green function at that boundary slot. The result is exact and precedes all norm estimates.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.terminalIncomingAnchor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (v : Fin m → T4) : T4

The first surviving internal point of a nonempty completed half-chain, written without choosing a new finite index.

Equations

• res.terminalIncomingAnchor v = Anderson4D.assemble 0 0 v (res.edgeSuccessor 0)

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.terminalOutgoingAnchor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) (v : Fin m → T4) : T4

The last surviving internal point of a nonempty completed half-chain.

Equations

• res.terminalOutgoingAnchor hactive v = Anderson4D.assemble 0 0 v (res.terminalOutgoingEdgeSlot hactive).castSucc

theorem Anderson4D.R324WithinHalfResidualPrefix.edgeSuccessor_zero_ne_last_of_active {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) : res.edgeSuccessor 0 ≠ Fin.last (m + 1)

With a nonempty active carrier, the successor of the incoming edge is an internal vertex rather than the external right endpoint.

theorem Anderson4D.R324WithinHalfResidualPrefix.assemble_edgeSuccessor_zero_eq_terminalIncomingAnchor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) (x y : T4) (v : Fin m → T4) : assemble x y v (res.edgeSuccessor 0) = res.terminalIncomingAnchor v

The incoming successor coordinate is independent of both external endpoints whenever the completed half-chain is nonempty.

theorem Anderson4D.R324WithinHalfResidualPrefix.edgeSuccessor_terminalOutgoingEdgeSlot_eq_last {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) : res.edgeSuccessor (res.terminalOutgoingEdgeSlot hactive) = Fin.last (m + 1)

The maximal active slot has no surviving internal successor.

theorem Anderson4D.R324WithinHalfResidualPrefix.assemble_terminalOutgoing_castSucc_eq_terminalOutgoingAnchor {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hactive : res.state.active.Nonempty) (x y : T4) (v : Fin m → T4) : assemble x y v (res.terminalOutgoingEdgeSlot hactive).castSucc = res.terminalOutgoingAnchor hactive v

The source coordinate of the outgoing terminal slot is independent of both external endpoints.

theorem Anderson4D.R324WithinHalfResidualPrefix.incomingBoundaryFactor_eq_incomingEndpointKernel {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hremaining : res.remaining = []) (hactive : res.state.active.Nonempty) (hedge : res.state.edges 0 = greenFn) (x y : T4) (v : Fin m → T4) : ↑(res.incomingBoundaryFactor x y v) = r324IncomingEndpointKernel (res.terminalIncomingAnchor v) (res.terminalIncomingAnchor v) false x

Exact direct incoming-boundary kernel identity.

theorem Anderson4D.R324WithinHalfResidualPrefix.outgoingBoundaryFactor_eq_outgoingEndpointKernel {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hremaining : res.remaining = []) (hactive : res.state.active.Nonempty) (hedge : res.state.edges (res.terminalOutgoingEdgeSlot hactive) = greenFn) (x y : T4) (v : Fin m → T4) : ↑(res.outgoingBoundaryFactor hactive x y v) = r324OutgoingEndpointKernel (res.terminalOutgoingAnchor hactive v) (res.terminalOutgoingAnchor hactive v) false y

Exact direct outgoing-boundary kernel identity.

theorem Anderson4D.R324WithinHalfResidualPrefix.integral_char_mul_incomingBoundaryFactor_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hremaining : res.remaining = []) (hactive : res.state.active.Nonempty) (hedge : res.state.edges 0 = greenFn) (k : Z4) (y : T4) (v : Fin m → T4) : ∫ (x : T4), charT4 k x * ↑(res.incomingBoundaryFactor x y v) ∂paperMeasure = translatedGreenMode k (res.terminalIncomingAnchor v)

Fourier coefficient of a direct incoming terminal leg.

theorem Anderson4D.R324WithinHalfResidualPrefix.integral_char_mul_outgoingBoundaryFactor_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hremaining : res.remaining = []) (hactive : res.state.active.Nonempty) (hedge : res.state.edges (res.terminalOutgoingEdgeSlot hactive) = greenFn) (k : Z4) (x : T4) (v : Fin m → T4) : ∫ (y : T4), charT4 k y * ↑(res.outgoingBoundaryFactor hactive x y v) ∂paperMeasure = translatedGreenMode k (res.terminalOutgoingAnchor hactive v)

Fourier coefficient of a direct outgoing terminal leg.

theorem Anderson4D.R324WithinHalfResidualPrefix.integral_char_mul_outgoingBoundaryFactor_eq_of_directOutgoing {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hremaining : res.remaining = []) (hm : 0 < m) (hprocessed : res.state.processed = r322AnalyticSchedule pairing) (hdirect : Fin.last m ∉ extractedRightEdges pairing) (hactive : res.state.active.Nonempty) (k : Z4) (x : T4) (v : Fin m → T4) : ∫ (y : T4), charT4 k y * ↑(res.outgoingBoundaryFactor hactive x y v) ∂paperMeasure = translatedGreenMode k (res.terminalOutgoingAnchor hactive v)

Consumer-facing direct-branch coefficient: schedule completion and non-extraction of the last edge discharge the raw-Green premise.

theorem Anderson4D.R324WithinHalfResidualPrefix.integral_char_mul_outgoingBoundaryFactor_eq_of_not_shortcut {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hremaining : res.remaining = []) (hm : 0 < m) (hprocessed : res.state.processed = r322AnalyticSchedule pairing) (hdirect : r324OutgoingIsShortcut pairing = false) (hactive : res.state.active.Nonempty) (k : Z4) (x : T4) (v : Fin m → T4) : ∫ (y : T4), charT4 k y * ↑(res.outgoingBoundaryFactor hactive x y v) ∂paperMeasure = translatedGreenMode k (res.terminalOutgoingAnchor hactive v)

Boolean spelling of the preceding direct-branch coefficient.