Exhaustive one-half and two-half endpoint route cases

This is the finite structural case split behind paper Step 4(A). The four constructors retain the branch-specific witness needed by the corresponding signed identity; completedRoute forgets only that dependent witness and keeps the common terminal budget. Pairing two values therefore represents the literal 4 x 4 endpoint table without duplicating any transport proof.

def Anderson4D.R324WithinHalfResidualPrefix.r324PaperActualHalfEndpointCases {m : ℕ} (pairing : PartialPairing (Fin m)) : R324PaperHalfEndpointCases

The actual incoming/outgoing endpoint cases of one half, in paper order.

Equations

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

inductive Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointRoute {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} (providers : R324PaperHalfRouteProviders pairing incomingMode) : Type

Exhaustive structural route for one half. Evidence for the two actual classification tests is stored in the constructor, so a route cannot be mislabelled by assigning a convenient endpoint ledger after the fact.

• directDirect {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (hfirst : ⟨0, ⋯⟩ ∈ finalActive pairing) (houtgoing : Fin.last m ∉ extractedRightEdges pairing) (data : R324PaperHalfDirectDirectRoute providers) : R324PaperHalfEndpointRoute providers
• directExceptional {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (hfirst : ⟨0, ⋯⟩ ∈ finalActive pairing) (houtgoing : Fin.last m ∈ extractedRightEdges pairing) (data : R324PaperHalfDirectExceptionalRoute providers) : R324PaperHalfEndpointRoute providers
• exceptionalDirect {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (hfirst : ⟨0, ⋯⟩ ∉ finalActive pairing) (houtgoing : Fin.last m ∉ extractedRightEdges pairing) (data : R324PaperHalfExceptionalDirectRoute providers) : R324PaperHalfEndpointRoute providers
• exceptionalExceptional {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (hfirst : ⟨0, ⋯⟩ ∉ finalActive pairing) (houtgoing : Fin.last m ∈ extractedRightEdges pairing) (data : R324PaperHalfExceptionalExceptionalRoute providers) : R324PaperHalfEndpointRoute providers

def Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointRoute.completedRoute {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (route : R324PaperHalfEndpointRoute providers) : R324PaperHalfCompletedRoute pairing incomingMode

Forget the branch-dependent signed witness only after it has produced the common completed terminal route.

Equations

• (Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointRoute.directDirect hfirst houtgoing data).completedRoute = data.route
• (Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointRoute.directExceptional hfirst houtgoing data).completedRoute = data.route
• (Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointRoute.exceptionalDirect hfirst houtgoing data).completedRoute = data.route
• (Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointRoute.exceptionalExceptional hfirst houtgoing data).completedRoute = data.route

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointRoute.completedRoute_cases {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} {providers : R324PaperHalfRouteProviders pairing incomingMode} (route : R324PaperHalfEndpointRoute providers) : route.completedRoute.cases = r324PaperActualHalfEndpointCases pairing

The stored literal branch ledger agrees with the classification of the actual pairing.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperHalfEndpointRoute.exists_of_singles {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {incomingMode : Z4} (providers : R324PaperHalfRouteProviders pairing incomingMode) (hsingles : pairing.singles.Nonempty) : Nonempty (R324PaperHalfEndpointRoute providers)

Construct the unique actual branch. A residual single is needed only in the EE branch, exactly where it proves that the incoming and outgoing exceptional blocks are distinct.

The literal 4 x 4 structural table

structure Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftMode rightMode : Z4} (leftProviders : R324PaperHalfRouteProviders kappaP leftMode) (rightProviders : R324PaperHalfRouteProviders kappaM rightMode) : Type

• left : R324PaperHalfEndpointRoute leftProviders
• right : R324PaperHalfEndpointRoute rightProviders

def Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.terminal {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftMode rightMode : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP leftMode} {rightProviders : R324PaperHalfRouteProviders kappaM rightMode} (routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders) : R324TwoHalfTerminalData rho lam eps kappaP kappaM

Equations

• routes.terminal = routes.left.completedRoute.twoHalfTerminal routes.right.completedRoute

def Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.cases {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftMode rightMode : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP leftMode} {rightProviders : R324PaperHalfRouteProviders kappaM rightMode} (routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders) : Fin 4 → SmoothCutoff.R324EndpointReductionCase

Equations

• routes.cases = routes.left.completedRoute.combinedCases routes.right.completedRoute

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.cases_eq_actual {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftMode rightMode : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP leftMode} {rightProviders : R324PaperHalfRouteProviders kappaM rightMode} (routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders) : routes.cases = ![r324PaperActualHalfEndpointCases kappaP 0, r324PaperActualHalfEndpointCases kappaP 1, r324PaperActualHalfEndpointCases kappaM 0, r324PaperActualHalfEndpointCases kappaM 1]

The order is definitionally LI, LO, RI, RO, and both halves carry their actual pairing classifications.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.endpointSacrifice_mul_eq_product {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftMode rightMode : Z4} {leftProviders : R324PaperHalfRouteProviders kappaP leftMode} {rightProviders : R324PaperHalfRouteProviders kappaM rightMode} (routes : R324PaperTwoHalfEndpointRoutes leftProviders rightProviders) : routes.left.completedRoute.endpointSacrifice * routes.right.completedRoute.endpointSacrifice = SmoothCutoff.r324EndpointPrimitiveSacrificeProduct eps routes.cases

Exact multiplication of the two literal half costs; no eps^-8 uniformization is performed here.

theorem Anderson4D.R324WithinHalfResidualPrefix.R324PaperTwoHalfEndpointRoutes.exists_of_singles {rho : SmoothCutoff} {C lam eps K A : ℝ} {m : ℕ} {kappaP kappaM : PartialPairing (Fin m)} {leftMode rightMode : Z4} (leftProviders : R324PaperHalfRouteProviders kappaP leftMode) (rightProviders : R324PaperHalfRouteProviders kappaM rightMode) (hleft : kappaP.singles.Nonempty) (hright : kappaM.singles.Nonempty) : Nonempty (R324PaperTwoHalfEndpointRoutes leftProviders rightProviders)