Candidate Route190 pointwise scalar/Frattini lowering

This sidecar is candidate Section 8 only. It is intended as a drop-in replacement for the Route189 candidate provider centralCover_candidateLiftPartitionData_from_candidateRoute188ScalarFrattiniLowerClosers.

Route189 exposes five candidate scalar/Frattini atoms:

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

Route190 reroutes the candidate lift partition through the existing Route146 pointwise coordinate layer. Thus those five Route189 atoms are replaced by the more local manuscript-shaped pointwise residuals used by Route146:

• pointwise nonzero scalar-pushout values;
• pointwise nonzero-distinct scalar additivity;
• pointwise Frattini base coordinates;
• pointwise Frattini fibre coordinates;
• pointwise Frattini fibre realization;
• pointwise realization-after-coordinate;
• pointwise coordinate-after-realization.

No new axioms or theorem-level assumptions are introduced in this file; the residual frontier is inherited from CandidateRoute146Closers.

Route190 drop-in candidate provider

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

Route190 selected scalar/Frattini packet, replayed through the Route146 pointwise coordinate lowering.

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

Direct exact-image residual data through the Route190 pointwise scalar and Frattini coordinate lowering.

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

Route190 candidate lift-partition provider.

This has the same call shape as the Route189 candidate provider, but its candidate axiom closure goes through the Route146 pointwise residuals rather than the five Route189 scalar/Frattini packets.

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

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

Audit surface exposing the exact Route146-selected scalar/Frattini packet and the resulting Route190 lift partition.