Candidate scalar/Frattini route34 proofs

Route34 keeps the route31-compatible provider shape

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

but avoids the two route33 candidate residual names:

• centralCover_candidateMiddleScalarPushoutCoherentData;
• centralCover_candidateFrattiniCoordinateCoherentData.

The replacement route is lower in the exact-image stack:

• the scalar coherent evaluator is recovered by evaluating the canonical middle R-obstruction map against lambda : X_R;
• the Frattini coordinate/realization equivalence is recovered from the canonical affine-fibre exact-image partition.

Thus the visible frontier moves from route33's coherent scalar/coordinate packets to the stricter manuscript-shaped exact-image packets: centralCover_candidateObstructionMapData and centralCover_candidateFrattiniExactImageCardinalityData.

Scalar coherence from the middle R-obstruction map

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

Scalar-pushout values obtained by evaluating the selected R-obstruction map against invariant characters lambda : X_R.

Equations

• D.scalarPushoutValueData = { scalarPushoutValue := fun (lam : ↥B.XR) (x : Q2Presentation.Induction.centralCoverCandidateMiddleSource T) => (D.obstruction x) lam }

def Q2Presentation.Induction.CentralCoverCandidateMiddleRLiftObstructionMapData.scalarPushoutLinearityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : CentralCoverCandidateMiddleScalarPushoutLinearityData D.scalarPushoutValueData

Linearity of the scalar-pushout values follows theorem-level from the linear-map structure of B.obstructionSpace = Dual X_R.

Equations

• D.scalarPushoutLinearityData = { map_add := ⋯, map_smul := ⋯ }

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

Coherent scalar-pushout data recovered from the selected middle R-obstruction map.

Equations

• D.scalarPushoutCoherentData = { valueData := D.scalarPushoutValueData, linearityData := D.scalarPushoutLinearityData }

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

Route34 scalar coherent packet, derived from the canonical middle exact-image R-obstruction map rather than assumed as route33's coherent scalar residual.

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

Route34 scalar-obstruction evaluator assembled through the lower middle-obstruction map packet.

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

Route34 middle R-lift obstruction map. This is the same selected map used to define scalar coherence above, exposed in the route31 wrapper shape.

Frattini coordinates from the affine-fibre partition

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.liftCoordinateData {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) : CentralCoverCandidateFrattiniLiftCoordinateData B T D

The lift-coordinate map induced by the partition bijection.

Equations

• P.liftCoordinateData = { liftCoordinate := P.partition.bij.toFun }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.realizationData {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) : CentralCoverCandidateFrattiniRealizationData B T D

The realization map induced by the inverse partition bijection.

Equations

• P.realizationData = { realizeCoordinate := P.partition.bij.invFun }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.coordinateInverseData {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) : CentralCoverCandidateFrattiniCoordinateInverseData P.liftCoordinateData P.realizationData

The inverse laws are the inverse laws of the partition bijection.

Equations

• P.coordinateInverseData = { realize_liftCoordinate := ⋯, liftCoordinate_realize := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.coordinateCoherentData {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) : CentralCoverCandidateFrattiniCoordinateCoherentData B T D

Coherent coordinate/realization data recovered from the affine-fibre exact-image partition.

Equations

• P.coordinateCoherentData = { liftData := P.liftCoordinateData, realizationData := P.realizationData, inverseData := P.coordinateInverseData }

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

Route34 Frattini coordinate packet, derived from the lower exact-image partition/cardinality route rather than assumed as route33's coherent Frattini coordinate residual.

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

Route34 Frattini affine-fibre coordinate data.

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

Route34 Frattini exact-image partition for the selected middle obstruction.

Route-ready reassembly

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

Route34 coherent direct exact-image residual data assembled from the lower middle-obstruction map and matching Frattini exact-image partition.

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

Route34 semantic central R-lift data from the direct exact-image split and a route-supplied quotient-frame map.

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

Route34 candidate lift-partition provider in the same B T Q shape as route31, with no dependency on the two route33 candidate residual names.