Candidate scalar/Frattini route27 proofs

Route27 keeps the route26-compatible provider shape

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

but avoids the five route26 candidate residual axiom names:

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

The replacement data are the stricter Section 8 packets already isolated in CandidateScalarFrattiniActualClosers: pointwise scalar-pushout values with additivity and homogeneity for the selected family, and base/fibre Frattini coordinates with realization and the two inverse laws for that same coordinate system. This file introduces no new axioms.

Route27 scalar-pushout packet

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

Route27 scalar data: a selected pointwise scalar-pushout family together with additivity and homogeneity for that same family.

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

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

The route26 value packet reassembled from the selected pointwise family.

Equations

• D.valueData = D.scalarFamily.valueData

def Q2Presentation.Induction.CentralCoverCandidateScalarFrattiniRoute27MiddleData.linearityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateScalarFrattiniRoute27MiddleData B T) : CentralCoverCandidateMiddleScalarPushoutLinearityData D.valueData

The route26 linearity packet for the selected route27 value data.

Equations

• D.linearityData = D.scalarFamily.linearityData D.additivity D.homogeneity

def Q2Presentation.Induction.CentralCoverCandidateScalarFrattiniRoute27MiddleData.evaluatorData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateScalarFrattiniRoute27MiddleData B T) : CentralCoverCandidateMiddleScalarObstructionEvaluatorData B T

The current scalar obstruction evaluator reassembled from route27 scalar data.

Equations

• D.evaluatorData = D.scalarFamily.evaluatorData D.additivity D.homogeneity

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

The middle R-lift obstruction map reassembled from route27 scalar data.

Equations

• D.middleRLiftObstructionMapData = { obstruction := D.evaluatorData.obstructionEvaluator }

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

Route27 proves the selected scalar-pushout family from the already split pointwise value, additivity, and homogeneity packets.

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

The route26 value-data leaf is closable from the stricter route27 scalar family.

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

Route27 supplies linearity only for its selected value packet, avoiding the over-strong arbitrary-value-packet route26 leaf.

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

Current scalar-obstruction evaluator from route27 scalar data.

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

Middle R-lift obstruction map from route27 scalar data.

Route27 Frattini coordinate packet

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

Route27 Frattini data: base/fibre coordinates, curried realization, and the two inverse laws for that same coordinate system.

• baseCoordinate : CentralCoverCandidateFrattiniBaseCoordinateData B T D
• fiberCoordinate : CentralCoverCandidateFrattiniFiberCoordinateData self.baseCoordinate
• fiberRealization : CentralCoverCandidateFrattiniFiberRealizationData B T D
• realizeLift : CentralCoverCandidateFrattiniRealizeLiftCoordinateData self.baseCoordinate self.fiberCoordinate self.fiberRealization
• liftRealize : CentralCoverCandidateFrattiniLiftCoordinateRealizeData self.baseCoordinate self.fiberCoordinate self.fiberRealization

def Q2Presentation.Induction.CentralCoverCandidateScalarFrattiniRoute27FrattiniData.liftData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (E : CentralCoverCandidateScalarFrattiniRoute27FrattiniData B T D) : CentralCoverCandidateFrattiniLiftCoordinateData B T D

The route26 lift-coordinate packet reassembled from route27 base/fibre data.

Equations

• E.liftData = E.baseCoordinate.liftCoordinateData E.fiberCoordinate

def Q2Presentation.Induction.CentralCoverCandidateScalarFrattiniRoute27FrattiniData.realizationData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (E : CentralCoverCandidateScalarFrattiniRoute27FrattiniData B T D) : CentralCoverCandidateFrattiniRealizationData B T D

The route26 realization packet reassembled from route27 fibre realization.

Equations

• E.realizationData = E.fiberRealization.realizationData

def Q2Presentation.Induction.CentralCoverCandidateScalarFrattiniRoute27FrattiniData.inverseData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (E : CentralCoverCandidateScalarFrattiniRoute27FrattiniData B T D) : CentralCoverCandidateFrattiniCoordinateInverseData E.liftData E.realizationData

The route26 inverse-law packet for the selected route27 coordinate and realization maps.

Equations

• E.inverseData = { realize_liftCoordinate := ⋯, liftCoordinate_realize := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateScalarFrattiniRoute27FrattiniData.coordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (E : CentralCoverCandidateScalarFrattiniRoute27FrattiniData B T D) : CentralCoverCandidateFrattiniAffineFiberCoordinateData B T D

The current Frattini affine-fibre coordinate packet reassembled from route27 Frattini data.

Equations

• E.coordinateData = E.liftData.coordinateData E.realizationData E.inverseData

def Q2Presentation.Induction.CentralCoverCandidateScalarFrattiniRoute27FrattiniData.partitionData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (E : CentralCoverCandidateScalarFrattiniRoute27FrattiniData B T D) : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F

The Frattini exact-image partition reassembled from route27 Frattini data.

Equations

• E.partitionData = { partition := { bij := E.coordinateData.equiv } }

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

Route27 proves the selected Frattini coordinate system from the stricter base/fibre, realization, and inverse-law packets.

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

The route26 lift-coordinate leaf is closable from route27 Frattini data.

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

The route26 realization leaf is closable from route27 Frattini data.

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

Route27 supplies inverse laws only for its selected coordinate and realization maps, avoiding the over-strong arbitrary-pair route26 leaf.

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

Current Frattini affine-fibre coordinate data from route27 Frattini data.

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

Frattini exact-image partition for the selected middle obstruction.

Route-ready reassembly

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

Route27 coherent direct exact-image residual data assembled from the stricter scalar and Frattini packets.

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

Route27 final exact-image residual for the selected middle obstruction and matching Frattini exact-image partition.

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

Route27 middle exact-image obstruction evaluation.

theorem Q2Presentation.Induction.centralCover_candidateTopExactImageAffineFiberEquivSigma_from_scalarFrattiniRoute27 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty ((E : CentralCoverCandidateMiddleExactImageObstructionEvaluationData B T) × CentralCoverCandidateTopExactImageAffineFiberEquivData B T E)

Route27 dependent top affine-fibre packet, retaining the selected middle obstruction evaluation.

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

Semantic central R-lift data from route27 and a supplied quotient-frame map.

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

Route27 candidate lift-partition provider in the same B T Q shape as the route26 provider, with the five route26 candidate residual names refined to the stricter scalar and Frattini packets above.