The two direct-incoming left endpoint transforms #
This is the literal left-half part of paper Step 4(A). The genuine refined
physical root has already been written as a direct-incoming source in
R324PaperActualEndpointCollapse. Here that source is fed directly to the
existing DD and DE signed one-half transforms. The residual primitive
cross factor stays signed and is merely read on the final carrier through
the already proved coordinate projections.
No norm, endpoint sacrifice, or new summation occurs in this file.
The two coordinate projections #
theorem
Anderson4D.R324WithinHalfResidualPrefix.r324PaperLeftCanonicalCoefficient_eq_directDriver
{rho : SmoothCutoff}
{lam eps : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{alpha : Z4}
(transport : (initial rho lam eps kappaP).R324WithinHalfAlternatingTransport)
(beta : Z4)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(s : R324PaperLeftOuterParameter rho lam eps kappaM)
(v : (initial rho lam eps kappaP).SurvivingCoordinate → T4)
:
(initial rho lam eps kappaP).r324PaperLeftCanonicalCoefficient alpha beta pi s v = transport.final.r324PaperLeftCanonicalCoefficient alpha beta pi s (transport.projection v)
A direct/direct transport changes only the presentation of the left carrier; the canonical signed coefficient itself is unchanged.
theorem
Anderson4D.R324WithinHalfResidualPrefix.r324PaperLeftCanonicalCoefficient_eq_directOutgoing
{rho : SmoothCutoff}
{lam eps : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{alpha : Z4}
(outgoing : (initial rho lam eps kappaP).R324PaperOutgoingEndpointTerminal)
(beta : Z4)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(s : R324PaperLeftOuterParameter rho lam eps kappaM)
(v : (initial rho lam eps kappaP).SurvivingCoordinate → T4)
:
(initial rho lam eps kappaP).r324PaperLeftCanonicalCoefficient alpha beta pi s v = outgoing.terminalPost.r324PaperLeftCanonicalCoefficient alpha beta pi s
((outgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv outgoing.terminalData.terminal [] ⋯)
(outgoing.endpoint.projection v)).2
Removing the retained outgoing terminal likewise only changes the presentation on which the canonical signed coefficient is read.
theorem
Anderson4D.R324WithinHalfResidualPrefix.directExceptionalGeometryCoefficient_initialProjection
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP : PartialPairing (Fin m)}
{alpha : Z4}
{providers : R324PaperHalfRouteProviders kappaP alpha}
(data : R324PaperHalfDirectExceptionalRoute providers)
{U : Type u_1}
(coefficient : U → (data.outgoing.terminalPost.SurvivingCoordinate → T4) → ℂ)
(s : U)
(v : (initial rho lam eps kappaP).SurvivingCoordinate → T4)
:
R324PaperHalfEndpointUniformBound.ExactTransform.directExceptionalGeometryCoefficient data coefficient s
((data.geometry.transport.stop.splitSurvivingPiMeasurableEquiv data.geometry.terminalData.terminal [] ⋯)
(data.geometry.transport.projection v)).2 = data.directIncomingEndpointCoefficient (coefficient s)
((data.outgoing.endpoint.stop.splitSurvivingPiMeasurableEquiv data.outgoing.terminalData.terminal [] ⋯)
(data.outgoing.endpoint.projection v)).2
The coefficient transport in the DE constructor is exactly the
outgoing-terminal coordinate projection. This is only dependent transport
along the structural equality already stored by the route.
Direct/direct #
theorem
Anderson4D.R324WithinHalfResidualPrefix.leftDirectDirect_exactTransform_and_source_eq_physical
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{alpha : Z4}
{providers : R324PaperHalfRouteProviders kappaP alpha}
(houtgoing : Fin.last m ∉ extractedRightEdges kappaP)
(data : R324PaperHalfDirectDirectRoute providers)
(beta : Z4)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(physical : ℂ)
(hleft :
MeasureTheory.Integrable (r324PaperLeftDirectInitialSourceDensity alpha beta pi)
((paperMeasure.prod (r324PaperLeftOuterParameterMeasure rho lam eps kappaM)).prod
(MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaP).SurvivingCoordinate) => paperMeasure)))
(hphysical :
physical = ∫ (q :
(T4 × R324PaperLeftOuterParameter rho lam eps kappaM) × ((initial rho lam eps kappaP).SurvivingCoordinate → T4)), r324PaperLeftDirectInitialSourceDensity alpha beta pi
q ∂(paperMeasure.prod (r324PaperLeftOuterParameterMeasure rho lam eps kappaM)).prod
(MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaP).SurvivingCoordinate) => paperMeasure))
(hterminal :
MeasureTheory.Integrable
(fun
(q : (T4 × R324PaperLeftOuterParameter rho lam eps kappaM) × (data.transport.final.SurvivingCoordinate → T4)) =>
data.transport.final.incomingPhasedResidualDensity
(charT4 beta q.1.1 * (data.transport.multiplier alpha * (↑(paperSecondOrderModeDecay alpha) * data.transport.final.r324PaperLeftCanonicalCoefficient alpha beta pi q.1.2 q.2)))
alpha rho eps 0 q.1.1 q.2)
((paperMeasure.prod (r324PaperLeftOuterParameterMeasure rho lam eps kappaM)).prod
(MeasureTheory.Measure.pi fun (x : data.transport.final.SurvivingCoordinate) => paperMeasure)))
:
∃ (transform :
(R324PaperHalfEndpointUniformBound.ofDirectDirect houtgoing data).ExactTransform
(r324PaperLeftOuterParameterMeasure rho lam eps kappaM)
(fun (s : R324PaperLeftOuterParameter rho lam eps kappaM)
(v : (R324PaperHalfEndpointUniformBound.ofDirectDirect houtgoing data).carrier.SurvivingCoordinate → T4) =>
data.transport.final.r324PaperLeftCanonicalCoefficient alpha beta pi s v)
beta),
transform.source = physical
The genuine direct-incoming physical source is exactly the source field
of the literal left DD transform. The only analytic premise not already
contained in the physical entrance is integrability on the completed
terminal carrier, which is supplied by the terminal joint-integrability
producer at the final route call site.
Direct/exceptional #
theorem
Anderson4D.R324WithinHalfResidualPrefix.leftDirectExceptional_exactTransform_and_source_eq_physical
{rho : SmoothCutoff}
{C lam eps K A : ℝ}
{m : ℕ}
{kappaP kappaM : PartialPairing (Fin m)}
{alpha : Z4}
{providers : R324PaperHalfRouteProviders kappaP alpha}
(data : R324PaperHalfDirectExceptionalRoute providers)
(beta : Z4)
(pi : ↥kappaP.singles ≃ ↥kappaM.singles)
(physical : ℂ)
(hphysical :
physical = ∫ (q :
(T4 × R324PaperLeftOuterParameter rho lam eps kappaM) × ((initial rho lam eps kappaP).SurvivingCoordinate → T4)), r324PaperLeftDirectInitialSourceDensity alpha beta pi
q ∂(paperMeasure.prod (r324PaperLeftOuterParameterMeasure rho lam eps kappaM)).prod
(MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaP).SurvivingCoordinate) => paperMeasure))
(hcurrent :
MeasureTheory.Integrable
(fun
(q :
R324PaperLeftOuterParameter rho lam eps kappaM × T4 × ((initial rho lam eps kappaP).SurvivingCoordinate → T4)) =>
(initial rho lam eps kappaP).incomingPhasedResidualDensity
(R324PaperHalfEndpointUniformBound.ExactTransform.directExceptionalGeometryCoefficient data
(fun (s : R324PaperLeftOuterParameter rho lam eps kappaM)
(v : data.outgoing.terminalPost.SurvivingCoordinate → T4) =>
data.outgoing.terminalPost.r324PaperLeftCanonicalCoefficient alpha beta pi s v)
q.1
((data.geometry.transport.stop.splitSurvivingPiMeasurableEquiv data.geometry.terminalData.terminal [] ⋯)
(data.geometry.transport.projection q.2.2)).2)
alpha rho eps 0 q.2.1 q.2.2)
((r324PaperLeftOuterParameterMeasure rho lam eps kappaM).prod
(paperMeasure.prod
(MeasureTheory.Measure.pi fun (x : (initial rho lam eps kappaP).SurvivingCoordinate) => paperMeasure))))
(hstop :
MeasureTheory.Integrable
(fun
(q :
R324PaperLeftOuterParameter rho lam eps kappaM × T4 × (data.geometry.transport.stop.SurvivingCoordinate → T4)) =>
data.geometry.transport.stop.incomingPhasedResidualDensity
(data.geometry.transport.multiplier alpha * R324PaperHalfEndpointUniformBound.ExactTransform.directExceptionalGeometryCoefficient data
(fun (s : R324PaperLeftOuterParameter rho lam eps kappaM)
(v : data.outgoing.terminalPost.SurvivingCoordinate → T4) =>
data.outgoing.terminalPost.r324PaperLeftCanonicalCoefficient alpha beta pi s v)
q.1
((data.geometry.transport.stop.splitSurvivingPiMeasurableEquiv data.geometry.terminalData.terminal [] ⋯)
q.2.2).2)
alpha rho eps 0 q.2.1 q.2.2)
((r324PaperLeftOuterParameterMeasure rho lam eps kappaM).prod
(paperMeasure.prod
(MeasureTheory.Measure.pi fun (x : data.geometry.transport.stop.SurvivingCoordinate) => paperMeasure))))
(hint :
∀ (gap first : T4) (kappaB : ↥(primitiveFullPairings (residualBlockOrder data.geometry.terminalData.terminal.2))),
MeasureTheory.Integrable
(fun (r : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 2) → T4) =>
detJclosedIntegrandWith rho eps (2 * residualBlockOrder data.geometry.terminalData.terminal.2) (↑kappaB)
data.geometry.paperOutgoingTerminal.terminalContext.internalEdges
(primitiveAssemble (residualBlockOrder data.geometry.terminalData.terminal.2) ⋯ first (first - gap) r))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder data.geometry.terminalData.terminal.2 - 2)) =>
paperMeasure))
:
∃ (transform :
(R324PaperHalfEndpointUniformBound.ofDirectExceptional data).ExactTransform
(r324PaperLeftOuterParameterMeasure rho lam eps kappaM)
(fun (s : R324PaperLeftOuterParameter rho lam eps kappaM)
(v : (R324PaperHalfEndpointUniformBound.ofDirectExceptional data).carrier.SurvivingCoordinate → T4) =>
data.outgoing.terminalPost.r324PaperLeftCanonicalCoefficient alpha beta pi s v)
beta),
transform.source = physical
The direct-incoming physical source is also exactly the source of the
literal left DE transform. The small product regroup below only changes
the order from (outgoing endpoint, outer parameter, internal carrier) to
the order consumed by the already proved retained-terminal identity.
The displayed hcurrent, hstop, and fixed-section integrability premises
are precisely those of ExactTransform.ofDirectExceptional; no new
analytic assumption is introduced by this adapter.