Candidate Route167 closers

Route166's candidate side still exposes the eight Route85/Route164 scalar-Frattini coordinate leaves:

• centralCover_candidateMiddleScalarPushoutValueAtData;
• centralCover_candidateMiddleScalarPushoutAdditivityData;
• centralCover_candidateMiddleScalarPushoutHomogeneityData;
• centralCover_candidateFrattiniBaseCoordinateData;
• centralCover_candidateFrattiniFiberCoordinateData;
• centralCover_candidateFrattiniFiberRealizationData;
• centralCover_candidateFrattiniRealizeLiftCoordinateData;
• centralCover_candidateFrattiniLiftCoordinateRealizeData.

This sidecar keeps the Route164 downstream call shape while routing through the strictly lower Route146 pointwise scalar/Frattini packets. The scalar additivity and homogeneity statements are provided for the selected Route167 scalar family, as in the selected-packet Route164 bridge; they are not claimed for an arbitrary externally supplied family.

Route167 selected packets

@[reducible, inline]

abbrev Q2Presentation.Induction.CentralCoverCandidateRoute167ScalarPushoutData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Type

Route167 uses the Route106 reduced scalar packet, supplied here by the Route146 pointwise scalar residuals.

Equations

• Q2Presentation.Induction.CentralCoverCandidateRoute167ScalarPushoutData B T = Q2Presentation.Induction.CentralCoverCandidateRoute106ScalarPushoutData B T

@[reducible, inline]

abbrev Q2Presentation.Induction.CentralCoverCandidateRoute167SelectedScalarFrattiniData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Type

Route167 coherent selected scalar/Frattini packet, supplied by the Route146 pointwise closers.

Equations

• Q2Presentation.Induction.CentralCoverCandidateRoute167SelectedScalarFrattiniData B T = Q2Presentation.Induction.CentralCoverCandidateRoute106SelectedScalarFrattiniData B T

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

Route167 scalar data: zero is theorem-level, nonzero scalar values and nonzero-distinct additivity are pointwise Route146 residuals.

theorem Q2Presentation.Induction.centralCover_candidateMiddleScalarPushoutValueAtData_from_candidateRoute167Closers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (lam : ↥B.XR) : Nonempty (CentralCoverCandidateMiddleScalarPushoutValueAtData B T lam)

Route167 pointwise replacement for the old all-scalar value-at leaf.

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

Selected scalar-pushout family with additivity, lowered to Route146 pointwise values and nonzero-distinct pointwise additivity.

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

Selected scalar-pushout family with homogeneity. Homogeneity is theorem-level over ZMod 2 once selected additivity is available.

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

Selected Route164-shaped scalar value and linearity pair through the Route167 lower scalar frontier.

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

Route167 middle R-lift obstruction map from the selected lower scalar packet.

Route167 wrappers for the old Frattini coordinate leaves

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

Route167 lowers the base-coordinate packet to pointwise base coordinates.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniFiberCoordinateData_from_candidateRoute167Closers {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) : Nonempty (CentralCoverCandidateFrattiniFiberCoordinateData C)

Route167 lowers the fibre-coordinate packet to pointwise fibre coordinates.

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

Route167 lowers the curried realization packet to pointwise realizations.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniRealizeLiftCoordinateData_from_candidateRoute167Closers {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) (F : CentralCoverCandidateFrattiniFiberCoordinateData C) (R : CentralCoverCandidateFrattiniFiberRealizationData B T D) : Nonempty (CentralCoverCandidateFrattiniRealizeLiftCoordinateData C F R)

Route167 lowers realization-after-coordinate to pointwise inverse laws.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniLiftCoordinateRealizeData_from_candidateRoute167Closers {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) (F : CentralCoverCandidateFrattiniFiberCoordinateData C) (R : CentralCoverCandidateFrattiniFiberRealizationData B T D) : Nonempty (CentralCoverCandidateFrattiniLiftCoordinateRealizeData C F R)

Route167 lowers coordinate-after-realization to pointwise inverse laws.

theorem Q2Presentation.Induction.centralCover_candidateRoute167SelectedFrattiniCoordinateData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : Nonempty ((C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) × (F : CentralCoverCandidateFrattiniFiberCoordinateData C) × (R : CentralCoverCandidateFrattiniFiberRealizationData B T D) × CentralCoverCandidateFrattiniRealizeLiftCoordinateData C F R × CentralCoverCandidateFrattiniLiftCoordinateRealizeData C F R)

Route167 selected Frattini base/fibre/realization/inverse packet for a fixed middle obstruction.

theorem Q2Presentation.Induction.centralCover_candidateRoute167SelectedFrattiniCoordinateInverseData {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-shaped selected Frattini coordinate/realization/inverse tuple, but with the Route167 pointwise frontier.

Route164-shaped bridge through the lower Route167 data

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

Coherent Route167 selected scalar/Frattini packet.

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

Route167 coherent direct exact-image residual data through pointwise scalar and Frattini packets.

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

Drop-in Route167 candidate lift-partition provider.

This has the same B T Q call shape as centralCover_candidateLiftPartitionData_from_candidateRoute164Closers, but its proof closure replaces the eight Route166 candidate atoms by the Route146 pointwise scalar/Frattini atoms.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_candidateRoute167Closers_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.