Paper Step 4(A): reuse of the paired incoming endpoint #
The exceptional-incoming machinery already performs the paper-ordered operation: all earlier signed interval removals, incoming Fourier integration, and the complete primitive-head integration are exact before the ordinary primitive defect is exposed. To reuse that result with the endpoint-stop driver, only a coordinate statement is missing: the untouched refined outer functional factors through the driver's stop projection.
This file supplies precisely that projection adapter and composes it with the existing exact refined-root identity. It contains no norm estimate.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointStopAtTerminal.reconstruct_projection
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{terminal : R322ExtractionStep m}
{res : R324WithinHalfResidualPrefix ρ lam ε pairing}
(data : R324WithinHalfEndpointStopAtTerminal terminal res)
(v : res.SurvivingCoordinate → T4)
(i : data.stop.SurvivingCoordinate)
:
Reconstruction at a coordinate surviving to the endpoint stop commutes with the endpoint-stop projection.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfEndpointStopAtTerminal.finalActive_subset_stop_active
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{terminal : R322ExtractionStep m}
{res : R324WithinHalfResidualPrefix ρ lam ε pairing}
(data : R324WithinHalfEndpointStopAtTerminal terminal res)
:
finalActive pairing ⊆ data.stop.state.active
Every final residual vertex is still present immediately before the retained endpoint terminal.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.exists_incomingEndpointStopAtOutgoingTerminal_of_suffix_eq
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{κp : PartialPairing (Fin m)}
{initialScale : Fin (m + 1) → ℝ}
{outgoingTerminal : R322ExtractionStep m}
(data : R324IncomingExceptionalStopTraceAssembly κp initialScale)
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(provider : R324WithinHalfLocalBlockProvider ρ C lam ε K κp)
(middle : List (R322ExtractionStep m))
(hdistinct : data.terminal ≠ outgoingTerminal)
(hsuffix : data.suffix = middle ++ [outgoingTerminal])
:
Nonempty
(R324WithinHalfEndpointStopAtTerminal outgoingTerminal (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯))
In the distinct paired-endpoint branch, the outgoing shortcut is the last step of the suffix left after the incoming exceptional head. The existing endpoint-stop driver can therefore start directly from that after-head residual prefix. Its initial certificate is exactly the one already produced while absorbing the incoming head.
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalRefinedRootEndpointPostOuter
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{initialScale : Fin (m + 1) → ℝ}
{outgoingTerminal : R322ExtractionStep m}
(data : R324IncomingExceptionalStopTraceAssembly κp initialScale)
(endpoint :
R324WithinHalfEndpointStopAtTerminal outgoingTerminal (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯))
(α β : Z4)
(π : ↥κp.singles ≃ ↥κm.singles)
(ω : R324IncomingExceptionalRootParameter ρ lam ε κm)
(u : endpoint.stop.SurvivingCoordinate → T4)
:
The untouched refined outer functional, read on the carrier immediately before the retained outgoing endpoint terminal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalRefinedRootPostOuter_eq_endpointProjection
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{initialScale : Fin (m + 1) → ℝ}
{outgoingTerminal : R322ExtractionStep m}
(data : R324IncomingExceptionalStopTraceAssembly κp initialScale)
(endpoint :
R324WithinHalfEndpointStopAtTerminal outgoingTerminal (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯))
(α β : Z4)
(π : ↥κp.singles ≃ ↥κm.singles)
(ω : R324IncomingExceptionalRootParameter ρ lam ε κm)
(v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)
:
data.incomingExceptionalRefinedRootPostOuter α β π ω v = data.incomingExceptionalRefinedRootEndpointPostOuter endpoint α β π ω (endpoint.projection v)
The refined-root outer functional sees only final residual coordinates, so it factors exactly through an endpoint-stop projection.
noncomputable def
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalRefinedRootEndpointCoefficient
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{initialScale : Fin (m + 1) → ℝ}
{outgoingTerminal : R322ExtractionStep m}
(data : R324IncomingExceptionalStopTraceAssembly κp initialScale)
(endpoint :
R324WithinHalfEndpointStopAtTerminal outgoingTerminal (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯))
(α β : Z4)
(π : ↥κp.singles ≃ ↥κm.singles)
(ω : R324IncomingExceptionalRootParameter ρ lam ε κm)
(u : endpoint.stop.SurvivingCoordinate → T4)
:
The already-collapsed paired incoming endpoint coefficient, now read on
the endpoint-stop carrier. The primitive defect is the existing signed
ordinary-J defect; it is not estimated here.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.norm_incomingExceptionalRefinedRootEndpointCoefficient_le_scaled
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{initialScale : Fin (m + 1) → ℝ}
{outgoingTerminal : R322ExtractionStep m}
(data : R324IncomingExceptionalStopTraceAssembly κp initialScale)
(endpoint :
R324WithinHalfEndpointStopAtTerminal outgoingTerminal (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯))
(α β : Z4)
(π : ↥κp.singles ≃ ↥κm.singles)
(ω : R324IncomingExceptionalRootParameter ρ lam ε κm)
(u : endpoint.stop.SurvivingCoordinate → T4)
{primitiveConstant supportConstant : ℝ}
(hε : 0 < ε)
(hprimitive : 0 ≤ primitiveConstant)
(hlam : 0 ≤ lam)
(hprop :
∀ (H : Fin (2 * residualBlockOrder data.terminal.2 - 1) → T4 → ℝ),
IsAdmissiblePrimitiveInput (residualBlockOrder data.terminal.2) H →
MemEClassT4 (primitiveKernelDiff ρ lam ε (residualBlockOrder data.terminal.2) ⋯ H) ∧ MemEClassT4 (primitiveKernelInsertedDiff ρ lam ε (residualBlockOrder data.terminal.2) ⋯ H) ∧ PrimitiveKernelBounds ρ lam ε (residualBlockOrder data.terminal.2) ⋯ H supportConstant primitiveConstant)
:
‖data.incomingExceptionalRefinedRootEndpointCoefficient endpoint α β π ω u‖ ≤ paperFourthOrderModeDecay α * (2 * r324WithinHalfInternalEdgeScaleProduct data.stopContext data.stopScale * ∫ (z : T4), primitiveKernelMajorant primitiveConstant lam ε supportConstant (residualBlockOrder data.terminal.2)
z ∂paperMeasure) * ‖data.incomingExceptionalRefinedRootEndpointPostOuter endpoint α β π ω u‖
Quantitative form of the already-collapsed paired incoming endpoint. The exact incoming Fourier operation has already produced the square of the second-order multiplier; only the resulting ordinary primitive defect is bounded here, using the certificate transported to the genuine stop. No norm is moved through an earlier interval removal.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalPostCoefficient_refinedRoot_eq_endpointProjection
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{initialScale : Fin (m + 1) → ℝ}
{outgoingTerminal : R322ExtractionStep m}
(data : R324IncomingExceptionalStopTraceAssembly κp initialScale)
(endpoint :
R324WithinHalfEndpointStopAtTerminal outgoingTerminal (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯))
(α β : Z4)
(π : ↥κp.singles ≃ ↥κm.singles)
(ω : R324IncomingExceptionalRootParameter ρ lam ε κm)
(v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4)
:
data.incomingExceptionalPostCoefficient α (data.incomingExceptionalRefinedRootPostOuter α β π) ω v = data.incomingExceptionalRefinedRootEndpointCoefficient endpoint α β π ω (endpoint.projection v)
The incoming exceptional coefficient factors through the endpoint-stop projection without moving a norm across any interval removal.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.incomingExceptionalAfterHeadPhasedIntegrand_refinedRoot_endpoint_section_eq
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{κp κm : PartialPairing (Fin m)}
{initialScale : Fin (m + 1) → ℝ}
{outgoingTerminal : R322ExtractionStep m}
(data : R324IncomingExceptionalStopTraceAssembly κp initialScale)
(endpoint :
R324WithinHalfEndpointStopAtTerminal outgoingTerminal (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯))
(α β : Z4)
(π : ↥κp.singles ≃ ↥κm.singles)
(ω : R324IncomingExceptionalRootParameter ρ lam ε κm)
:
(fun (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) =>
data.incomingExceptionalAfterHeadPhasedIntegrand α
(fun (ω' : R324IncomingExceptionalRootParameter ρ lam ε κm) => ω'.1.1)
(data.incomingExceptionalRefinedRootPostOuter α β π) (ω, v)) = fun (v : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).SurvivingCoordinate → T4) =>
(data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).incomingPhasedResidualDensity
(data.incomingExceptionalRefinedRootEndpointCoefficient endpoint α β π ω (endpoint.projection v)) α ρ ε 0 ω.1.1 v
Section form consumed directly by endpoint.transport.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_r324RefinedPhysicalIntegral_eq_incomingEndpointStop
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{initialScale : Fin (m + 1) → ℝ}
{outgoingTerminal : R322ExtractionStep m}
(p : R324RefinedScheduleIndex m)
(e₀ : MomentContraction m)
(he₀ : e₀ ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd)
(data : R324IncomingExceptionalStopTraceAssembly e₀.fst initialScale)
(endpoint :
R324WithinHalfEndpointStopAtTerminal outgoingTerminal (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯))
(hm : 0 < m)
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(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))
(α β : Z4)
:
↑(lamEps lam ε) ^ (2 * (initial ρ lam ε e₀.fst).remainingOrder) * r324RefinedPhysicalIntegral ρ ε m α β p = ∫ (ω : R324IncomingExceptionalRootParameter ρ lam ε e₀.snd.fst), ↑(lamEps lam ε) ^ (2 * endpoint.stop.remainingOrder) * ∫ (u : endpoint.stop.SurvivingCoordinate → T4), endpoint.stop.incomingPhasedResidualDensity
(endpoint.multiplier α * data.incomingExceptionalRefinedRootEndpointCoefficient endpoint α β e₀.snd.snd ω u) α
ρ ε 0 ω.1.1
u ∂MeasureTheory.Measure.pi fun (x : endpoint.stop.SurvivingCoordinate) =>
paperMeasure ∂r324IncomingExceptionalRootParameterMeasure ρ lam ε e₀.snd.fst
Exact root-to-endpoint-stop identity for the paired incoming branch. All earlier interval removals and the incoming primitive collapse are completed before the endpoint-stop transport is invoked.