Candidate scalar/Frattini Route63 closers

Route63 is a candidate Section 8 sidecar. It keeps the drop-in call shape of centralCover_candidateLiftPartitionData_from_frattiniRoute58 and centralCover_candidateLiftPartitionData_from_frattiniRoute60, but routes the candidate contribution through the lower exact-image R-lift/Frattini semantic proofs.

The five Route62-visible scalar/coordinate atoms are treated as follows.

• scalar-pushout values are closed by evaluating the selected R-valued obstruction map against lambda : X_R;
• scalar-pushout linearity is provided for that same selected value family;
• Frattini lift coordinates and realizations are the two directions of the selected exact-image partition equivalence;
• Frattini inverse laws are provided for that same selected coordinate and realization pair.

Thus the arbitrary-linearity and arbitrary-inverse-law leaves are strictly lowered to coherent selected-data packets, and the route-ready provider has no dependency on the five Route62 scalar/coordinate axioms.

Scalar pushout projections from the lower R-obstruction map

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

Route63 scalar-pushout values obtained by evaluating the selected R-obstruction against invariant scalar pushouts.

Equations

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

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

Route63 linearity for the selected scalar-pushout value family.

Equations

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

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

Route63 closes the scalar-pushout value packet from the lower exact-image R-obstruction map.

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

Route63 supplies scalar-pushout linearity for the selected value family.

This is intentionally the coherent selected-data replacement for the stronger Route62 atom that asked for linearity of an arbitrary externally supplied value packet.

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

The current scalar-obstruction evaluator assembled from the Route63 selected scalar value family and its linearity.

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

The middle R-lift obstruction map reassembled through the Route63 selected scalar-pushout evaluator.

Frattini coordinates from the lower exact-image partition

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route63LiftCoordinateData {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

Route63 lift-coordinate map carried by the selected exact-image partition.

Equations

• P.route63LiftCoordinateData = { liftCoordinate := ⇑P.partition.bij }

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route63RealizationData {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

Route63 realization map carried by the inverse exact-image partition.

Equations

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

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageSurjectivityData.route63CoordinateInverseData {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.route63LiftCoordinateData P.route63RealizationData

Route63 inverse laws for the selected coordinate and realization maps.

Equations

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

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

The current Frattini coordinate packet induced by the selected exact-image partition.

Equations

• P.route63AffineFiberCoordinateData = P.route63LiftCoordinateData.coordinateData P.route63RealizationData P.route63CoordinateInverseData

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

Route63 closes the Frattini lift-coordinate packet from the lower exact-image partition.

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

Route63 closes the Frattini realization packet from the inverse of the lower exact-image partition.

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

Route63 supplies inverse laws for the selected coordinate and realization maps.

This is intentionally the coherent selected-data replacement for the stronger Route62 atom that asked for inverse laws for arbitrary externally supplied coordinate and realization maps.

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

The full current Frattini affine-fibre coordinate packet from the lower exact-image partition.

Route-ready coherent providers

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

Route63 coherent direct exact-image data, using the lower obstruction map and its matching Frattini partition.

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

Drop-in candidate lift-partition provider for the active Route58/Route60 call shape.

This can replace centralCover_candidateLiftPartitionData_from_frattiniRoute58 B T Qframe or centralCover_candidateLiftPartitionData_from_frattiniRoute60 B T Qframe in an integration experiment.

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

Route63 also exposes the no-extra-Qframe packet-closer route, useful when the exact-image base quotient is supplied by the lower boundary-postcomposition packet rather than by the integrated route.