Candidate Frattini Route58 actual proofs

This sidecar is candidate Section 8 only. It does not edit the active Route56 integration file.

Route56 currently exposes two actual candidate leaves:

• centralCover_candidateActualMiddleRLiftObstructionMapData;
• centralCover_candidateActualFrattiniAffineFiberExactImageEquivData.

Route58 proves Route56-compatible replacements for both actual leaves from the coherent scalar/Frattini semantic packets:

• scalar pushout values on the middle exact-image source, with linearity in lambda : B.XR;
• Frattini coordinate, realization, and inverse-law data for the selected middle obstruction map.

This deliberately avoids the older broad pair centralCover_candidateObstructionMapData and centralCover_candidateFrattiniExactImageCardinalityData.

Route58 replacements for the two Route56 actual leaves

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

Route58 proof of the actual middle R-lift obstruction map.

The obstruction is assembled from scalar-pushout values and their linearity, not from the Route56 actual axiom and not from the older broad obstruction-map packet.

theorem Q2Presentation.Induction.centralCover_candidateActualFrattiniAffineFiberExactImageEquivData_from_frattiniRoute58 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (O : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : Nonempty (CentralCoverCandidateFrattiniExactImageEquivData B T O.obstructionIndexToBaseMapData.O O.affineFiberTorsorData.Z O.affineFiberTorsorData.F)

Route58 proof of the actual Frattini affine-fibre exact-image equivalence.

The lower semantic route provides the matching exact-image partition for the selected middle obstruction. The equivalence required by Route56 is exactly that partition bijection.

Coherent Route58 packet

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

Route58 actual exact-image datum.

This has the same mathematical shape as Route56's coherent pair, but the provider below proves the two fields through the finer scalar/Frattini semantic route.

• middleObstruction : CentralCoverCandidateMiddleRLiftObstructionMapData B T
• frattiniEquiv : CentralCoverCandidateFrattiniExactImageEquivData B T self.middleObstruction.obstructionIndexToBaseMapData.O self.middleObstruction.affineFiberTorsorData.Z self.middleObstruction.affineFiberTorsorData.F

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

Route58 actual exact-image provider.

Expected nonstandard candidate axioms in this closure are the coherent scalar/Frattini semantic packets:

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

It should not depend on either Route56 actual axiom or on the older broad candidate obstruction/cardinality pair.

def Q2Presentation.Induction.CentralCoverCandidateRoute58ActualExactImageData.route56ExactImageData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute58ActualExactImageData B T) : CentralCoverCandidateRoute56ExactImageData B T

Repackage Route58 data in the existing Route56 packet type.

Equations

• D.route56ExactImageData = { middleObstruction := D.middleObstruction, frattiniEquiv := D.frattiniEquiv }

def Q2Presentation.Induction.CentralCoverCandidateRoute58ActualExactImageData.liftPartitionData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute58ActualExactImageData B T) : CentralCoverCandidateLiftPartitionData B

Candidate lift partition recovered directly from the Route58 actual pair.

Equations

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

Route56-compatible and drop-in providers

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

Compatibility theorem for code that wants the Route56 packet type, but with the Route58 lower axiom closure.

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

Drop-in candidate lift-partition provider for the active Route56 call site.

To test this sidecar in an integration experiment, replace centralCover_candidateLiftPartitionData_from_frattiniRoute56 B T Qframe by this theorem.