Candidate Route164 closers

Route163's candidate side still exposes the five scalar/Frattini semantic packets from CandidateScalarFrattiniSemanticClosers:

• centralCover_candidateMiddleScalarPushoutValueData;
• centralCover_candidateMiddleScalarPushoutLinearityData;
• centralCover_candidateFrattiniLiftCoordinateData;
• centralCover_candidateFrattiniRealizationData;
• centralCover_candidateFrattiniCoordinateInverseData.

This sidecar is a drop-in candidate replacement for centralCover_candidateLiftPartitionData_from_candidateRoute161Closers. It routes through the stricter Route85 data:

• pointwise scalar-pushout values, plus additivity and homogeneity for the selected scalar family;
• base and fibre Frattini coordinates, curried realization, and the two inverse laws.

The arbitrary scalar-linearity and arbitrary coordinate-inverse Route163 leaves are therefore lowered to coherent selected packets, while the bridge theorem keeps the same B T Q call shape as Route161.

Route164 wrappers for the five Route163 candidate leaves

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

Route164 lowers the Route163 scalar value packet to pointwise scalar pushout values.

theorem Q2Presentation.Induction.centralCover_candidateRoute164SelectedScalarPushoutValueLinearityData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty ((V : CentralCoverCandidateMiddleScalarPushoutValueData B T) × CentralCoverCandidateMiddleScalarPushoutLinearityData V)

Route164 selected scalar family with the two linearity laws. This is the coherent replacement for the stronger Route163 leaf that asked for linearity of an arbitrary externally supplied value packet.

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

Route164 lowers the Route163 Frattini lift-coordinate packet to base and fibre coordinates.

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

Route164 lowers the Route163 Frattini realization packet to curried base/fibre realization data.

theorem Q2Presentation.Induction.centralCover_candidateRoute164SelectedFrattiniCoordinateInverseData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : Nonempty ((L : CentralCoverCandidateFrattiniLiftCoordinateData B T D) × (R : CentralCoverCandidateFrattiniRealizationData B T D) × CentralCoverCandidateFrattiniCoordinateInverseData L R)

Route164 selected Frattini coordinate/realization/inverse tuple for a fixed middle obstruction. This is the coherent replacement for the stronger Route163 leaf that asked for inverse laws for arbitrary externally supplied coordinate and realization maps.

Route161-shaped bridge through the lower Route164 data

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

Route164 coherent direct exact-image residual data through the lower pointwise scalar and base/fibre Frattini packets.

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

Route164 produces the same coherent exact-image packet shape used by the Route161 bridge, but with the five Route163 scalar/Frattini leaves replaced by the lower Route85 frontier.

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

Drop-in Route164 candidate lift-partition provider.

This has the same B T Q call shape and target type as centralCover_candidateLiftPartitionData_from_candidateRoute161Closers.

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

Canonical-tower spelling for integration routes that keep the canonical quotient tower in scope.