Candidate scalar/Frattini route23 proofs

Route23 targets the actual scalar/Frattini leaves left visible by route22.

The arbitrary-packet statements in CandidateScalarFrattiniActualClosers are stronger than the data needed by the route: additivity/homogeneity are only needed for the scalar family generated by the chosen evaluator, and the Frattini fibre/inverse laws are only needed for the coordinates generated by a chosen affine-fibre equivalence. This file therefore proves the concrete route-needed versions and reassembles the route22 lift-partition shape without using the eight actual-leaf axioms.

Scalar pushout leaves for the evaluator-generated family

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

The pointwise scalar-pushout family generated by one scalar value packet.

Equations

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

def Q2Presentation.Induction.CentralCoverCandidateMiddleScalarPushoutValueData.route23AdditivityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleScalarPushoutValueData B T) (L : CentralCoverCandidateMiddleScalarPushoutLinearityData D) : CentralCoverCandidateMiddleScalarPushoutAdditivityData D.route23FamilyData

Additivity for the evaluator-generated pointwise scalar family.

Equations

• D.route23AdditivityData L = { map_add := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateMiddleScalarPushoutValueData.route23HomogeneityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleScalarPushoutValueData B T) (L : CentralCoverCandidateMiddleScalarPushoutLinearityData D) : CentralCoverCandidateMiddleScalarPushoutHomogeneityData D.route23FamilyData

Homogeneity for the evaluator-generated pointwise scalar family.

Equations

• D.route23HomogeneityData L = { map_smul := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateMiddleScalarPushoutValueData.route23EvaluatorData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleScalarPushoutValueData B T) (L : CentralCoverCandidateMiddleScalarPushoutLinearityData D) : CentralCoverCandidateMiddleScalarObstructionEvaluatorData B T

Reassemble the current scalar-obstruction evaluator through the concrete route23 scalar leaves.

Equations

• D.route23EvaluatorData L = D.route23FamilyData.evaluatorData (D.route23AdditivityData L) (D.route23HomogeneityData L)

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

Pointwise scalar-pushout values from the current scalar value packet.

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

The scalar leaves actually needed downstream: one evaluator-generated pointwise family together with additivity and homogeneity for that same family.

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

Current scalar-obstruction evaluator assembled through route23's concrete scalar leaves, not the actual-leaf axioms.

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

Middle R-lift obstruction map assembled through route23 scalar leaves.

Frattini leaves for the coordinate-generated maps

def Q2Presentation.Induction.CentralCoverCandidateFrattiniLiftCoordinateData.route23BaseCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (L : CentralCoverCandidateFrattiniLiftCoordinateData B T D) : CentralCoverCandidateFrattiniBaseCoordinateData B T D

Base coordinate obtained by projecting the affine-fibre coordinate.

Equations

• L.route23BaseCoordinateData = { baseCoordinate := fun (f : Q2Presentation.Induction.centralCoverCandidateSource) => (L.liftCoordinate f).fst }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniLiftCoordinateData.route23FiberCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (L : CentralCoverCandidateFrattiniLiftCoordinateData B T D) : CentralCoverCandidateFrattiniFiberCoordinateData L.route23BaseCoordinateData

Fibre coordinate obtained by projecting the affine-fibre coordinate.

Equations

• L.route23FiberCoordinateData = { fiberCoordinate := fun (f : Q2Presentation.Induction.centralCoverCandidateSource) => (L.liftCoordinate f).snd }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniRealizationData.route23FiberRealizationData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (R : CentralCoverCandidateFrattiniRealizationData B T D) : CentralCoverCandidateFrattiniFiberRealizationData B T D

Curried fibre realization obtained from the affine-fibre realization map.

Equations

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

def Q2Presentation.Induction.centralCover_candidateFrattiniRealizeLiftCoordinateData_of_route23Maps {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (L : CentralCoverCandidateFrattiniLiftCoordinateData B T D) (R : CentralCoverCandidateFrattiniRealizationData B T D) (I : CentralCoverCandidateFrattiniCoordinateInverseData L R) : CentralCoverCandidateFrattiniRealizeLiftCoordinateData L.route23BaseCoordinateData L.route23FiberCoordinateData R.route23FiberRealizationData

Realization after route23 base/fibre coordinates is the original map.

Equations

• Q2Presentation.Induction.centralCover_candidateFrattiniRealizeLiftCoordinateData_of_route23Maps L R I = { realize_liftCoordinate := ⋯ }

def Q2Presentation.Induction.centralCover_candidateFrattiniLiftCoordinateRealizeData_of_route23Maps {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (L : CentralCoverCandidateFrattiniLiftCoordinateData B T D) (R : CentralCoverCandidateFrattiniRealizationData B T D) (I : CentralCoverCandidateFrattiniCoordinateInverseData L R) : CentralCoverCandidateFrattiniLiftCoordinateRealizeData L.route23BaseCoordinateData L.route23FiberCoordinateData R.route23FiberRealizationData

Route23 base/fibre coordinates after realization recover the original affine-fibre point.

Equations

• Q2Presentation.Induction.centralCover_candidateFrattiniLiftCoordinateRealizeData_of_route23Maps L R I = { liftCoordinate_realize := ⋯ }

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

Base-coordinate packet from the current Frattini coordinate map.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniFiberCoordinateData_from_route23Map {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (L : CentralCoverCandidateFrattiniLiftCoordinateData B T D) : Nonempty (CentralCoverCandidateFrattiniFiberCoordinateData L.route23BaseCoordinateData)

Fibre-coordinate packet for the base coordinate projected from the same Frattini coordinate map.

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

Fibre-realization packet from the current Frattini realization map.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniRealizeLiftCoordinateData_from_route23Maps {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (L : CentralCoverCandidateFrattiniLiftCoordinateData B T D) (R : CentralCoverCandidateFrattiniRealizationData B T D) (I : CentralCoverCandidateFrattiniCoordinateInverseData L R) : Nonempty (CentralCoverCandidateFrattiniRealizeLiftCoordinateData L.route23BaseCoordinateData L.route23FiberCoordinateData R.route23FiberRealizationData)

One inverse law for the route23-projected Frattini coordinates.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniLiftCoordinateRealizeData_from_route23Maps {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (L : CentralCoverCandidateFrattiniLiftCoordinateData B T D) (R : CentralCoverCandidateFrattiniRealizationData B T D) (I : CentralCoverCandidateFrattiniCoordinateInverseData L R) : Nonempty (CentralCoverCandidateFrattiniLiftCoordinateRealizeData L.route23BaseCoordinateData L.route23FiberCoordinateData R.route23FiberRealizationData)

The other inverse law for the route23-projected Frattini coordinates.

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

The Frattini leaves actually needed downstream: one projected base/fibre/realization coordinate system and both inverse laws for that same system.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniCoordinateInverseData_from_route23Leaves {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) (F : CentralCoverCandidateFrattiniFiberCoordinateData C) (R : CentralCoverCandidateFrattiniFiberRealizationData B T D) (LR : CentralCoverCandidateFrattiniRealizeLiftCoordinateData C F R) (RL : CentralCoverCandidateFrattiniLiftCoordinateRealizeData C F R) : Nonempty (CentralCoverCandidateFrattiniCoordinateInverseData (C.liftCoordinateData F) R.realizationData)

Assemble the semantic inverse-law packet from route23's two concrete inverse leaves.

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

Current Frattini affine-fibre coordinate data assembled through route23's concrete Frattini leaves.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniAffineFiberPartition_from_route23ActualLeaves {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 assembled through route23 Frattini leaves.

Route-ready reassembly

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

Route23 direct exact-image residual data assembled from route23 scalar and Frattini leaves, avoiding the eight actual-leaf axioms used by route22.

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

Route23 coherent final exact-image residual for the selected middle obstruction and matching Frattini exact-image equivalence.

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

Route23 middle exact-image obstruction evaluation.

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

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

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

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

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

Route23 candidate lift-partition provider in the same B T Q shape as route22, but without the eight actual scalar/Frattini leaf axioms.