Documentation

Anderson4D.DetParametrix.Paper42_Moment.R324DriverRootInstantiation

Driver instantiation at the genuine refined physical root #

The alternating driver transports the incoming phased residual density from any reachable residual prefix to a terminal prefix with empty remaining list, accumulating one collapsed-head factor per exceptional stop into its multiplier. This module instantiates the driver at the genuine refined physical root: the after-head prefix produced by the seam-2 endpoint is transported a.e. in the root parameter, with the refined-root outer coefficient factored through the driver's terminal projection.

Unlike the phased-trace endpoint, no OrdinaryAlong hypothesis is taken: slot-zero-fed heads inside the after-head suffix are absorbed by the driver's exceptional collapse and appear as factors of the terminal multiplier.

Terminal evaluation of the residual factors #

No outgoing production slots remain at a terminal prefix.

theorem Anderson4D.R324WithinHalfResidualPrefix.residualDifferenceProduct_of_remaining_nil {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hnil : res.remaining = []) (x y : T4) (v : Fin m → T4) :

The signed-difference product of a terminal prefix is one.

theorem Anderson4D.R324WithinHalfResidualPrefix.residualPrimitiveProduct_of_remaining_nil {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hnil : res.remaining = []) (ρ' : SmoothCutoff) (ε' : ℝ) (v : Fin m → T4) :
res.residualPrimitiveProduct ρ' ε' v = 1

The primitive covariance product of a terminal prefix is one.

theorem Anderson4D.R324WithinHalfResidualPrefix.residualChainEdgeFactor_of_remaining_nil {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hnil : res.remaining = []) (x y : T4) (v : Fin m → T4) (edge : Fin (m + 1)) :
res.residualChainEdgeFactor x y v edge = if edge ∈ res.activeEdgeSlots then res.state.edges edge (res.edgeDisplacement x y v edge) else 1

At a terminal prefix every ordinary sparse-chain factor is the named edge at its displacement on active slots and one elsewhere: no slot is reserved for a remaining signed difference.

The slot-zero-erased chain product of a nonempty completed half-chain is the outgoing boundary factor times the endpoint-erased interior product.

theorem Anderson4D.R324WithinHalfResidualPrefix.terminal_incomingErasedResidualIntegrand_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hnil : res.remaining = []) (hactive : res.state.active.Nonempty) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (v : Fin m → T4) :
res.incomingErasedResidualIntegrand ρ' ε' x y v = res.outgoingBoundaryFactor hactive x y v * res.endpointErasedSignedChain hactive x y v

Terminal form of the slot-zero-erased residual core. At a terminal prefix with nonempty active carrier, the difference and primitive products are exhausted and only the surviving signed chain remains: the outgoing boundary Green factor times the endpoint-erased interior pair product.

With a nonempty active carrier the incoming phase anchor is the endpoint-independent first surviving internal point.

theorem Anderson4D.R324WithinHalfResidualPrefix.terminal_incomingPhasedResidualDensity_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hnil : res.remaining = []) (hactive : res.state.active.Nonempty) (coefficient : ℂ) (k : Z4) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (v : res.SurvivingCoordinate → T4) :
res.incomingPhasedResidualDensity coefficient k ρ' ε' x y v = coefficient * charT4 k (res.terminalIncomingAnchor (res.reconstruct v)) * ↑(res.outgoingBoundaryFactor hactive x y (res.reconstruct v) * res.endpointErasedSignedChain hactive x y (res.reconstruct v))

Terminal evaluation of the incoming phased residual density. At a terminal prefix with nonempty active carrier the density is the coefficient, the incoming character at the endpoint-independent first surviving internal point, and the explicit product of the surviving outgoing Green boundary factor with the endpoint-erased interior signed chain.

With an empty active carrier the incoming edge points directly at the outgoing external endpoint.

With an empty active carrier only the incoming production slot is active.

With an empty active carrier the slot-zero-erased chain product is one.

theorem Anderson4D.R324WithinHalfResidualPrefix.terminal_incomingPhasedResidualDensity_eq_of_active_empty {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hnil : res.remaining = []) (hempty : res.state.active = ∅) (coefficient : ℂ) (k : Z4) (ρ' : SmoothCutoff) (ε' : ℝ) (x y : T4) (v : res.SurvivingCoordinate → T4) :
res.incomingPhasedResidualDensity coefficient k ρ' ε' x y v = coefficient * charT4 k y

Degenerate terminal evaluation. At a terminal prefix whose active carrier is empty, every interior factor is exhausted and the phased density is the coefficient times the incoming character read directly at the outgoing external endpoint.

theorem Anderson4D.R324WithinHalfResidualPrefix.integral_char_mul_terminal_incomingPhasedResidualDensity_eq {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hnil : res.remaining = []) (hactive : res.state.active.Nonempty) (hedge : res.state.edges (res.terminalOutgoingEdgeSlot hactive) = greenFn) (coefficient : ℂ) (k β : Z4) (ρ' : SmoothCutoff) (ε' : ℝ) (x : T4) (v : res.SurvivingCoordinate → T4) :
∫ (y : T4), charT4 β y * res.incomingPhasedResidualDensity coefficient k ρ' ε' x y v ∂paperMeasure = coefficient * charT4 k (res.terminalIncomingAnchor (res.reconstruct v)) * ↑(res.endpointErasedSignedChain hactive 0 0 (res.reconstruct v)) * translatedGreenMode β (res.terminalOutgoingAnchor hactive (res.reconstruct v))

Fourier evaluation of the terminal outgoing leg. Integrating the terminal phased density against an outgoing character in the free outgoing endpoint produces the translated Green mode at the last surviving internal point; the incoming character and the endpoint-erased interior chain are endpoint-independent and factor out. This is the identity consumed by the endpoint branch summation once the outgoing character has been split off the root coefficient.

The driver's terminal prefix has consumed the whole analytic schedule: an empty remaining list forces the processed list to be the literal schedule.

The driver-terminal active carrier is the final active set of the frozen pairing: the branch dichotomy (nonempty against empty) for the terminal evaluation is decided by the pairing combinatorics alone.

Reconstruction at every driver-terminal coordinate is unchanged by the driver projection.

noncomputable def Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.afterHeadAlternatingTransport {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {κp : PartialPairing (Fin m)} {initialScale : Fin (m + 1) → ℝ} (data : R324IncomingExceptionalStopTraceAssembly κp initialScale) (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K κp) :

The alternating transport of the complete after-head suffix, built from the local block provider and the certificate transported to the exceptional stop. Later slot-zero-fed heads are absorbed into the driver multiplier.

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

    The untouched refined-root outer functional read on the terminal carrier of an alternating transport of the after-head prefix: the retained endpoint characters, the untouched right initial residual, and the cross-cut primitive factor reconstructed from the driver-terminal prefix.

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

      Driver-terminal factorization of the refined-root outer functional. The cross-cut primitive factor reads only coordinates on the doubled residual carrier, all of which survive to the driver's terminal prefix; hence the whole refined-root outer functional factors through the projection of any alternating transport of the after-head prefix.

      The collapsed-head coefficient of the genuine refined root, read on the driver's terminal carrier: squared second-order decay, primitive Step-4 defect of the exceptional head, and the driver-terminal form of the untouched refined outer functional.

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

        The collapsed-head refined-root coefficient factors through the projection of any alternating transport of the after-head prefix.

        At a fixed root parameter, the after-head phased integrand of the genuine refined root is the after-head phased density whose coefficient is the driver-terminal refined coefficient read through the driver projection.

        theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_r324RefinedPhysicalIntegral_eq_driverTerminal {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {initialScale : Fin (m + 1) → ℝ} (p : R324RefinedScheduleIndex m) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) (data : R324IncomingExceptionalStopTraceAssembly e₀.fst initialScale) (t : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) (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) :

        Driver instantiation at the genuine refined root. The weighted single-fibre refined physical integral, with the exceptional head absorbed by the base case and the whole after-head suffix absorbed by the alternating driver: the right-hand side integrates the driver-terminal phased density over the root parameter and the terminal coordinates, with the driver multiplier times the collapsed-head refined coefficient read on the terminal carrier. No ordinariness hypothesis is taken.

        theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.lamEps_pow_r324RefinedPhysicalIntegral_eq_afterHeadDriverTerminal {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {initialScale : Fin (m + 1) → ℝ} (p : R324RefinedScheduleIndex m) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) (data : R324IncomingExceptionalStopTraceAssembly e₀.fst initialScale) (hm : 0 < m) (hε : 0 < ε) (hε1 : ε ≤ 1) (provider : R324WithinHalfLocalBlockProvider ρ C lam ε K e₀.fst) (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) :

        The driver instantiation with the transport built directly from the local block provider and the stop certificate: the complete root endgame equation with every after-head hypothesis discharged from the provider.

        theorem Anderson4D.R324WithinHalfResidualPrefix.R324IncomingExceptionalStopTraceAssembly.eventually_integrable_incomingExceptionalRefinedRootDriverTerminal {ρ : SmoothCutoff} {C lam ε K : ℝ} {m : ℕ} {initialScale : Fin (m + 1) → ℝ} (p : R324RefinedScheduleIndex m) (e₀ : MomentContraction m) (he₀ : e₀ ∈ momentRefinedContractionFiber m ↑p.fst ↑p.snd) (data : R324IncomingExceptionalStopTraceAssembly e₀.fst initialScale) (t : (data.trace.stopPrefix.afterHead data.terminal data.suffix ⋯).R324WithinHalfAlternatingTransport) (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) :

        Driver-terminal integrability at the genuine refined root. For almost every root parameter, the driver-terminal phased density with the multiplier-weighted refined terminal coefficient is integrable over the terminal coordinates.