Candidate scalar/Frattini route37 proofs

Route37 keeps the route36 provider shape

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

but no longer routes through the seven route36 candidate residual names.

• On the scalar side, the pointwise scalar-pushout values and additivity are supplied as one coherent selected family. The ZMod 2 homogeneity law is still theorem-level, inherited from route36's additivity argument.
• On the Frattini side, the five base/fibre coordinate, realization, and inverse-law leaves are replaced by the exact affine-fibre partition from the central-cover transform. Coordinates and inverse laws can be recovered from that bijection, but the route only needs the partition itself.

This matches the manuscript direction in Section 8: scalar pushouts separate the middle R-obstruction, while the final Frattini stage is an exact-image partition of unobstructed affine fibres.

Coherent scalar-pushout family

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

Route37 scalar data: one selected pointwise scalar-pushout family together with additivity for that same family.

This is weaker than independently asking for all pointwise values and then asking additivity for an arbitrary family: the manuscript only requires the chosen scalar-pushout evaluator used to assemble the middle obstruction.

• scalarFamily : CentralCoverCandidateMiddleScalarPushoutFamilyData B T
• additivity : CentralCoverCandidateMiddleScalarPushoutAdditivityData self.scalarFamily

axiom Q2Presentation.Induction.centralCover_candidateScalarFrattiniRoute37ScalarData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverCandidateScalarFrattiniRoute37ScalarData B T)

Route37 scalar-pushout packet.

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

Route37 closes a pointwise scalar-pushout value for each lambda from the selected coherent scalar family.

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

Route37 supplies additivity for its selected scalar-pushout family.

The old residual asks for additivity for an arbitrary externally supplied family; that is stronger than the Section 8 construction needs.

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

Route37 scalar-obstruction evaluator. Homogeneity is derived theorem-level from additivity over ZMod 2.

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

Route37 middle R-lift obstruction map from the coherent scalar route.

Frattini coordinates recovered from the exact affine-fibre partition

axiom Q2Presentation.Induction.centralCover_candidateRoute37FrattiniExactImagePartitionData {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)

Route37 Frattini packet: the exact-image affine-fibre partition supplied by the central-cover transform.

This replaces the five split coordinate/realization leaves. If downstream code wants those maps, they are projections and inverse maps of this bijection.

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

Base coordinate induced by the Route37 partition bijection.

Equations

• P.route37BaseCoordinateData = { baseCoordinate := fun (f : Q2Presentation.Induction.centralCoverCandidateSource) => (P.partition.bij.toFun f).fst }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route37FiberCoordinateData {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) : CentralCoverCandidateFrattiniFiberCoordinateData P.route37BaseCoordinateData

Fibre coordinate induced by the Route37 partition bijection.

Equations

• P.route37FiberCoordinateData = { fiberCoordinate := fun (f : Q2Presentation.Induction.centralCoverCandidateSource) => (P.partition.bij.toFun f).snd }

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

Curried realization induced by the inverse Route37 partition bijection.

Equations

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

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route37RealizeLiftCoordinateData {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) : CentralCoverCandidateFrattiniRealizeLiftCoordinateData P.route37BaseCoordinateData P.route37FiberCoordinateData P.route37FiberRealizationData

Realization after the partition-induced coordinates is the original top exact-image map.

Equations

• P.route37RealizeLiftCoordinateData = { realize_liftCoordinate := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route37LiftCoordinateRealizeData {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) : CentralCoverCandidateFrattiniLiftCoordinateRealizeData P.route37BaseCoordinateData P.route37FiberCoordinateData P.route37FiberRealizationData

Partition-induced coordinates after realization recover the original unobstructed affine-fibre point.

Equations

• P.route37LiftCoordinateRealizeData = { liftCoordinate_realize := ⋯ }

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

Route37 closes the base-coordinate leaf from the lower exact partition.

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

Route37 supplies a fibre-coordinate packet for the base coordinate induced by its exact partition. The arbitrary-base version is intentionally not asserted.

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

Route37 closes the curried realization leaf from the inverse exact partition.

theorem Q2Presentation.Induction.centralCover_candidateRoute37FrattiniCoordinateSystemData {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)

Route37 provides the full partition-induced Frattini coordinate system and both inverse laws as one coherent packet.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniAffineFiberPartition_from_scalarFrattiniRoute37 {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)

Route37 exact-image partition for the selected middle obstruction.

Route-ready reassembly

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

Route37 direct exact-image residual data from the coherent scalar route and the exact Frattini partition.

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

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

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

Route37 candidate lift-partition provider in the same B T Q shape as route36, with the route36 seven residuals replaced by one coherent scalar family packet and one exact Frattini partition packet.