Candidate Route147 pointwise closers

Route147's integrated candidate side currently consumes CandidateRoute146Closers, whose remaining Section 8 assumptions are seven pointwise scalar/Frattini atoms. This sidecar does not edit that integrated route. It exposes a same-call-shape replacement provider whose proof bypasses those seven pointwise atoms:

• scalar values and selected additivity are induced by the lower R-valued obstruction map on the middle exact-image source;
• base/fibre coordinates, curried realization, and inverse laws are induced by the lower Frattini affine-fibre exact-image partition.

The resulting closure is strictly lower than the Route147 pointwise frontier: the final provider depends only on the two semantic Section 8 leaves centralCover_candidateObstructionMapData and centralCover_candidateFrattiniExactImageCardinalityData, plus Lean standard axioms.

Scalar pointwise values from the middle R-obstruction

def Q2Presentation.Induction.CentralCoverCandidateMiddleRLiftObstructionMapData.route147ScalarPushoutValueAtPointData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) (lam : ↥B.XR) (x : centralCoverCandidateMiddleSource T) : CentralCoverCandidateMiddleScalarPushoutNonzeroValueAtPointData B T lam x

Route147 scalar value at one point, obtained by evaluating the selected R-obstruction against lambda : B.XR.

Equations

• D.route147ScalarPushoutValueAtPointData lam x = { value := (D.obstruction x) lam }

def Q2Presentation.Induction.CentralCoverCandidateMiddleRLiftObstructionMapData.route147NonzeroScalarPushoutValueAtData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) (lam : ↥B.XR) : CentralCoverCandidateMiddleScalarPushoutNonzeroValueAtData B T lam

Route147 scalar value packet for one scalar, induced by the selected middle R-obstruction.

Equations

• D.route147NonzeroScalarPushoutValueAtData lam = { valueAt := fun (x : Q2Presentation.Induction.centralCoverCandidateMiddleSource T) => (D.obstruction x) lam }

def Q2Presentation.Induction.CentralCoverCandidateMiddleRLiftObstructionMapData.route147ScalarPushoutFamilyData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : CentralCoverCandidateMiddleScalarPushoutFamilyData B T

The selected Route147 scalar-pushout family induced by the lower R-obstruction map.

Equations

• D.route147ScalarPushoutFamilyData = { valueAt := fun (lam : ↥B.XR) => (D.route147NonzeroScalarPushoutValueAtData lam).valueData }

def Q2Presentation.Induction.CentralCoverCandidateMiddleRLiftObstructionMapData.route147NonzeroDistinctAdditivityAtData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) (x : centralCoverCandidateMiddleSource T) (lam mu : ↥B.XR) (hlam : lam ≠ 0) (hmu : mu ≠ 0) (hdiff : lam ≠ mu) : CentralCoverCandidateMiddleScalarPushoutNonzeroDistinctAdditivityAtData D.route147ScalarPushoutFamilyData x lam mu hlam hmu hdiff

Pointwise additivity for the selected Route147 scalar family. This closes the pointwise additivity shape after replacing the arbitrary family by the family induced by the semantic obstruction map.

Equations

• D.route147NonzeroDistinctAdditivityAtData x lam mu hlam hmu hdiff = { map_add_at := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateMiddleRLiftObstructionMapData.route147NonzeroDistinctAdditivityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : CentralCoverCandidateMiddleScalarPushoutNonzeroDistinctAdditivityData D.route147ScalarPushoutFamilyData

Nonzero-distinct additivity for the selected Route147 scalar family.

Equations

• D.route147NonzeroDistinctAdditivityData = { map_add_nonzero_distinct := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateMiddleRLiftObstructionMapData.route147ScalarPushoutData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : CentralCoverCandidateRoute106ScalarPushoutData B T

Route106-shaped scalar packet induced by the lower middle obstruction.

Equations

• D.route147ScalarPushoutData = { scalarFamily := D.route147ScalarPushoutFamilyData, zero_value := ⋯, additivityNonzeroDistinct := D.route147NonzeroDistinctAdditivityData }

theorem Q2Presentation.Induction.centralCover_candidateMiddleScalarPushoutNonzeroValueAtPointData_from_candidateRoute147PointwiseClosers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (lam : ↥B.XR) (_h : lam ≠ 0) (x : centralCoverCandidateMiddleSource T) : Nonempty (CentralCoverCandidateMiddleScalarPushoutNonzeroValueAtPointData B T lam x)

The Route147 pointwise scalar-value atom is closed from the lower semantic middle R-obstruction map.

theorem Q2Presentation.Induction.centralCover_candidateMiddleScalarPushoutNonzeroValueAtData_from_candidateRoute147PointwiseClosers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (lam : ↥B.XR) (_h : lam ≠ 0) : Nonempty (CentralCoverCandidateMiddleScalarPushoutNonzeroValueAtData B T lam)

The nonzero scalar value packet assembled from theorem-level pointwise values induced by the same lower obstruction map.

theorem Q2Presentation.Induction.centralCover_candidateMiddleScalarPushoutNonzeroDistinctAdditivityAtData_from_candidateRoute147PointwiseClosers_selected {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (x : centralCoverCandidateMiddleSource T) (lam mu : ↥B.XR) (hlam : lam ≠ 0) (hmu : mu ≠ 0) (hdiff : lam ≠ mu) : Nonempty ((D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) × CentralCoverCandidateMiddleScalarPushoutNonzeroDistinctAdditivityAtData D.route147ScalarPushoutFamilyData x lam mu hlam hmu hdiff)

Selected pointwise additivity: the arbitrary-family Route147 additivity atom is strictly lowered to the family induced by the semantic obstruction map.

theorem Q2Presentation.Induction.centralCover_candidateRoute147SelectedNonzeroDistinctAdditivityData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty ((V : CentralCoverCandidateMiddleScalarPushoutFamilyData B T) × CentralCoverCandidateMiddleScalarPushoutNonzeroDistinctAdditivityData V)

Selected scalar family with nonzero-distinct additivity, strictly below the arbitrary-family Route147 pointwise additivity atom.

theorem Q2Presentation.Induction.centralCover_candidateRoute147ScalarPushoutData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverCandidateRoute106ScalarPushoutData B T)

Route147 scalar packet from the lower middle obstruction.

Frattini pointwise data from the affine-fibre partition

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route147BaseCoordinateAtData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (P : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F) (f : centralCoverCandidateSource) : CentralCoverCandidateFrattiniBaseCoordinateAtData B T D f

Pointwise base coordinate induced by the selected Frattini partition.

Equations

• P.route147BaseCoordinateAtData f = { baseCoordinateAt := (P.partition.bij f).fst }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route147BaseCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (P : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F) : CentralCoverCandidateFrattiniBaseCoordinateData B T D

Base coordinate map induced by the selected Frattini partition.

Equations

• P.route147BaseCoordinateData = { baseCoordinate := fun (f : Q2Presentation.Induction.centralCoverCandidateSource) => (P.route147BaseCoordinateAtData f).baseCoordinateAt }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route147FiberCoordinateAtData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (P : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F) (f : centralCoverCandidateSource) : CentralCoverCandidateFrattiniFiberCoordinateAtData P.route147BaseCoordinateData f

Pointwise fibre coordinate over the selected Route147 base coordinate.

Equations

• P.route147FiberCoordinateAtData f = { fiberCoordinateAt := (P.partition.bij f).snd }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route147FiberCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (P : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F) : CentralCoverCandidateFrattiniFiberCoordinateData P.route147BaseCoordinateData

Fibre coordinate map over the selected Route147 base coordinate.

Equations

• P.route147FiberCoordinateData = { fiberCoordinate := fun (f : Q2Presentation.Induction.centralCoverCandidateSource) => (P.route147FiberCoordinateAtData f).fiberCoordinateAt }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route147FiberRealizationAtData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (P : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F) (x : CentralCoverCandidateFrattiniBaseTarget B T D) (y : D.affineFiberTorsorData.F.Lift x) : CentralCoverCandidateFrattiniFiberRealizationAtData B T D x y

Pointwise realization induced by the inverse of the selected Frattini partition.

Equations

• P.route147FiberRealizationAtData x y = { realizeFiberAt := P.partition.bij.invFun ⟨x, y⟩ }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route147FiberRealizationData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (P : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F) : CentralCoverCandidateFrattiniFiberRealizationData B T D

Curried realization induced by the inverse of the selected Frattini partition.

Equations

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

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route147RealizeLiftCoordinateAtData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (P : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F) (f : centralCoverCandidateSource) : CentralCoverCandidateFrattiniRealizeLiftCoordinateAtData P.route147BaseCoordinateData P.route147FiberCoordinateData P.route147FiberRealizationData f

Pointwise realization-after-coordinate law for the selected Route147 coordinates.

Equations

• P.route147RealizeLiftCoordinateAtData f = { realize_liftCoordinate_at := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route147RealizeLiftCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (P : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F) : CentralCoverCandidateFrattiniRealizeLiftCoordinateData P.route147BaseCoordinateData P.route147FiberCoordinateData P.route147FiberRealizationData

Realization-after-coordinate law for the selected Route147 coordinates.

Equations

• P.route147RealizeLiftCoordinateData = { realize_liftCoordinate := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route147LiftCoordinateRealizeAtData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (P : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F) (y : CentralCoverCandidateFrattiniAffineFiberTarget B T D) : CentralCoverCandidateFrattiniLiftCoordinateRealizeAtData P.route147BaseCoordinateData P.route147FiberCoordinateData P.route147FiberRealizationData y

Pointwise coordinate-after-realization law for the selected Route147 coordinates.

Equations

• P.route147LiftCoordinateRealizeAtData y = { liftCoordinate_realize_at := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route147LiftCoordinateRealizeData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (P : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F) : CentralCoverCandidateFrattiniLiftCoordinateRealizeData P.route147BaseCoordinateData P.route147FiberCoordinateData P.route147FiberRealizationData

Coordinate-after-realization law for the selected Route147 coordinates.

Equations

• P.route147LiftCoordinateRealizeData = { liftCoordinate_realize := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route147FrattiniCoordinateSystemData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (P : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F) : CentralCoverCandidateRoute85FrattiniCoordinateSystemData B T D

Route85-shaped Frattini coordinate system induced by the selected Route147 affine-fibre partition.

Equations

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

theorem Q2Presentation.Induction.centralCover_candidateFrattiniBaseCoordinateAtData_from_candidateRoute147PointwiseClosers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) (f : centralCoverCandidateSource) : Nonempty (CentralCoverCandidateFrattiniBaseCoordinateAtData B T D f)

The Route147 pointwise Frattini base-coordinate atom is closed from the lower affine-fibre exact-image partition.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniFiberCoordinateAtData_from_candidateRoute147PointwiseClosers_selected {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) (f : centralCoverCandidateSource) : Nonempty ((C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) × CentralCoverCandidateFrattiniFiberCoordinateAtData C f)

Selected pointwise Frattini fibre-coordinate data. The original Route147 atom is over an arbitrary base-coordinate map; here it is lowered to the base coordinate induced by the semantic Frattini partition.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniFiberRealizationAtData_from_candidateRoute147PointwiseClosers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) (x : CentralCoverCandidateFrattiniBaseTarget B T D) (y : D.affineFiberTorsorData.F.Lift x) : Nonempty (CentralCoverCandidateFrattiniFiberRealizationAtData B T D x y)

The Route147 pointwise Frattini realization atom is closed from the inverse of the lower affine-fibre exact-image partition.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniRealizeLiftCoordinateAtData_from_candidateRoute147PointwiseClosers_selected {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) (f : centralCoverCandidateSource) : Nonempty ((C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) × (F : CentralCoverCandidateFrattiniFiberCoordinateData C) × (R : CentralCoverCandidateFrattiniFiberRealizationData B T D) × CentralCoverCandidateFrattiniRealizeLiftCoordinateAtData C F R f)

Selected pointwise realization-after-coordinate law.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniLiftCoordinateRealizeAtData_from_candidateRoute147PointwiseClosers_selected {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) (y : CentralCoverCandidateFrattiniAffineFiberTarget B T D) : Nonempty ((C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) × (F : CentralCoverCandidateFrattiniFiberCoordinateData C) × (R : CentralCoverCandidateFrattiniFiberRealizationData B T D) × CentralCoverCandidateFrattiniLiftCoordinateRealizeAtData C F R y)

Selected pointwise coordinate-after-realization law.

theorem Q2Presentation.Induction.centralCover_candidateRoute147FrattiniCoordinateSystemData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : Nonempty (CentralCoverCandidateRoute85FrattiniCoordinateSystemData B T D)

Route147 Frattini coordinate system for a supplied middle obstruction, assembled from the lower affine-fibre exact-image partition.

Route147 pointwise reassembly

structure Q2Presentation.Induction.CentralCoverCandidateRoute147PointwiseData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Type

Coherent Route147 packet: selected scalar data and selected Frattini coordinate data attached to the same lower middle obstruction map.

• middleObstruction : CentralCoverCandidateMiddleRLiftObstructionMapData B T
• scalar : CentralCoverCandidateRoute106ScalarPushoutData B T
• frattini : CentralCoverCandidateRoute85FrattiniCoordinateSystemData B T self.middleObstruction

def Q2Presentation.Induction.CentralCoverCandidateRoute147PointwiseData.directExactImageResidualData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (S : CentralCoverCandidateRoute147PointwiseData B T) : CentralCoverCandidateDirectExactImageResidualData B T

Reassemble direct exact-image residual data from Route147 pointwise lowerings.

Equations

• S.directExactImageResidualData = { middleObstruction := S.middleObstruction, frattiniPartition := S.frattini.frattiniExactImage }

def Q2Presentation.Induction.CentralCoverCandidateRoute147PointwiseData.liftPartitionData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (S : CentralCoverCandidateRoute147PointwiseData B T) (Q : CentralCoverCandidateQuotientFrameMapData B T) : CentralCoverCandidateLiftPartitionData B

Reassemble the candidate lift partition from Route147 pointwise lowerings and the route-supplied quotient-frame map.

Equations

• S.liftPartitionData Q = S.directExactImageResidualData.liftPartitionData Q

theorem Q2Presentation.Induction.centralCover_candidateRoute147PointwiseData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverCandidateRoute147PointwiseData B T)

Coherent Route147 pointwise-lowered data.

theorem Q2Presentation.Induction.centralCover_candidateDirectExactImageResidualData_from_candidateRoute147PointwiseClosers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverCandidateDirectExactImageResidualData B T)

Direct exact-image residual data with the Route147 pointwise atoms lowered through semantic obstruction and Frattini partition packets.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_candidateRoute147PointwiseClosers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B T) : Nonempty (CentralCoverCandidateLiftPartitionData B)

Drop-in Route147 candidate lift-partition provider.

This has the same B T Q call shape as centralCover_candidateLiftPartitionData_from_candidateRoute146Closers.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_candidateRoute147PointwiseClosers_canonical {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B D.tower) : Nonempty (CentralCoverCandidateLiftPartitionData B)

Canonical-tower spelling matching integrated routes that keep the canonical quotient tower in scope.

theorem Q2Presentation.Induction.centralCover_candidateRoute147PointwiseAudit {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B T) : Nonempty ((_ : CentralCoverCandidateRoute147PointwiseData B T) × CentralCoverCandidateLiftPartitionData B)

Audit surface exposing the selected Route147 packet together with the route-ready lift partition it determines.