Candidate Frattini Route56 proofs

This sidecar is a candidate-only §8 refinement over Route54. The earlier Route54 coherent exact-image packet is useful, but it is built through the Route53/Route36 scalar-coordinate path, so its transitive axiom closure can still expose the seven coordinate leaves

• centralCover_candidateMiddleScalarPushoutValueAtData,
• centralCover_candidateMiddleScalarPushoutAdditivityData,
• centralCover_candidateFrattiniBaseCoordinateData,
• centralCover_candidateFrattiniFiberCoordinateData,
• centralCover_candidateFrattiniFiberRealizationData,
• centralCover_candidateFrattiniRealizeLiftCoordinateData, and
• centralCover_candidateFrattiniLiftCoordinateRealizeData.

The manuscript construction is more coherent at this point: choose the final middle R-obstruction and the Frattini exact-image equivalence attached to that same obstruction. Route56 packages exactly that pair and projects all route-needed scalar/Frattini data from it theorem-level. Thus the candidate closure is reduced from the seven coordinate leaves to the two actual §8 inputs already isolated in CandidateMiddleFrattiniActualProofs.

Route56 coherent exact-image packet

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

Route56 candidate exact-image datum.

This is the manuscript-shaped candidate datum for the final Frattini step: the selected middle R-valued obstruction on the canonical middle exact-image source, together with the Frattini exact-image equivalence for the affine fibres attached to that same obstruction.

• middleObstruction : CentralCoverCandidateMiddleRLiftObstructionMapData B T
• frattiniEquiv : CentralCoverCandidateFrattiniExactImageEquivData B T self.middleObstruction.obstructionIndexToBaseMapData.O self.middleObstruction.affineFiberTorsorData.Z self.middleObstruction.affineFiberTorsorData.F

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

Route56 residual provider from the two actual manuscript-shaped inputs.

This theorem intentionally does not use the seven scalar/Frattini coordinate residuals. Its expected axiom closure is exactly the two actual candidate inputs:

• centralCover_candidateActualMiddleRLiftObstructionMapData;
• centralCover_candidateActualFrattiniAffineFiberExactImageEquivData.

Scalar projections

def Q2Presentation.Induction.CentralCoverCandidateRoute56ExactImageData.scalarPushoutValueAtData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute56ExactImageData B T) (lam : ↥B.XR) : CentralCoverCandidateMiddleScalarPushoutValueAtData B T lam

Scalar-pushout value at lambda, obtained by evaluating the selected R-obstruction against lambda.

Equations

• D.scalarPushoutValueAtData lam = { valueAt := fun (x : Q2Presentation.Induction.centralCoverCandidateMiddleSource T) => (D.middleObstruction.obstruction x) lam }

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

The selected scalar-pushout family induced by the middle obstruction.

Equations

• D.scalarPushoutFamilyData = { valueAt := fun (lam : ↥B.XR) => D.scalarPushoutValueAtData lam }

def Q2Presentation.Induction.CentralCoverCandidateRoute56ExactImageData.scalarPushoutAdditivityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute56ExactImageData B T) : CentralCoverCandidateMiddleScalarPushoutAdditivityData D.scalarPushoutFamilyData

Additivity in lambda, inherited from the selected linear obstruction.

Equations

• D.scalarPushoutAdditivityData = { map_add := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateRoute56ExactImageData.scalarPushoutHomogeneityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute56ExactImageData B T) : CentralCoverCandidateMiddleScalarPushoutHomogeneityData D.scalarPushoutFamilyData

Homogeneity in lambda, inherited from the selected linear obstruction.

Equations

• D.scalarPushoutHomogeneityData = { map_smul := ⋯ }

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

Route52/Route53 scalar evaluator shape recovered from the coherent Route56 datum.

Equations

• D.scalarObstructionEvaluatorData = D.scalarPushoutFamilyData.evaluatorData D.scalarPushoutAdditivityData D.scalarPushoutHomogeneityData

Frattini-coordinate projections

def Q2Presentation.Induction.CentralCoverCandidateRoute56ExactImageData.frattiniExactImage {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute56ExactImageData B T) : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.middleObstruction.obstructionIndexToBaseMapData.O D.middleObstruction.affineFiberTorsorData.Z D.middleObstruction.affineFiberTorsorData.F

Frattini exact-image partition carried by the Route56 equivalence.

Equations

• D.frattiniExactImage = D.frattiniEquiv.frattiniExactImage

def Q2Presentation.Induction.CentralCoverCandidateRoute56ExactImageData.baseCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute56ExactImageData B T) : CentralCoverCandidateFrattiniBaseCoordinateData B T D.middleObstruction

Base coordinate induced by the exact-image equivalence.

Equations

• D.baseCoordinateData = { baseCoordinate := fun (f : Q2Presentation.Induction.centralCoverCandidateSource) => (D.frattiniEquiv.equiv f).fst }

def Q2Presentation.Induction.CentralCoverCandidateRoute56ExactImageData.fiberCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute56ExactImageData B T) : CentralCoverCandidateFrattiniFiberCoordinateData D.baseCoordinateData

Fibre coordinate induced by the exact-image equivalence.

Equations

• D.fiberCoordinateData = { fiberCoordinate := fun (f : Q2Presentation.Induction.centralCoverCandidateSource) => (D.frattiniEquiv.equiv f).snd }

def Q2Presentation.Induction.CentralCoverCandidateRoute56ExactImageData.fiberRealizationData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute56ExactImageData B T) : CentralCoverCandidateFrattiniFiberRealizationData B T D.middleObstruction

Curried realization induced by the inverse exact-image equivalence.

Equations

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

def Q2Presentation.Induction.CentralCoverCandidateRoute56ExactImageData.realizeLiftCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute56ExactImageData B T) : CentralCoverCandidateFrattiniRealizeLiftCoordinateData D.baseCoordinateData D.fiberCoordinateData D.fiberRealizationData

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

Equations

• D.realizeLiftCoordinateData = { realize_liftCoordinate := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateRoute56ExactImageData.liftCoordinateRealizeData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute56ExactImageData B T) : CentralCoverCandidateFrattiniLiftCoordinateRealizeData D.baseCoordinateData D.fiberCoordinateData D.fiberRealizationData

Route56 coordinates after realization recover the original affine-fibre point.

Equations

• D.liftCoordinateRealizeData = { liftCoordinate_realize := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateRoute56ExactImageData.affineFiberCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute56ExactImageData B T) : CentralCoverCandidateFrattiniAffineFiberCoordinateData B T D.middleObstruction

Current coordinate/realization packet recovered from the Route56 exact-image equivalence.

Equations

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

def Q2Presentation.Induction.CentralCoverCandidateRoute56ExactImageData.liftPartitionData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute56ExactImageData B T) : CentralCoverCandidateLiftPartitionData B

Candidate lift partition recovered from the coherent exact-image datum.

Equations

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

Projections from the Route56 packet

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

Pointwise scalar value packet for the selected Route56 family.

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

Additivity for the selected scalar family carried by Route56.

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

Scalar evaluator recovered from the coherent Route56 datum.

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

Middle R-lift obstruction map recovered from Route56.

theorem Q2Presentation.Induction.centralCover_candidateSelectedFrattiniCoordinateData_from_frattiniRoute56 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty ((D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) × (C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) × (F : CentralCoverCandidateFrattiniFiberCoordinateData C) × (R : CentralCoverCandidateFrattiniFiberRealizationData B T D) × CentralCoverCandidateFrattiniRealizeLiftCoordinateData C F R × CentralCoverCandidateFrattiniLiftCoordinateRealizeData C F R)

Selected Frattini base/fibre/realization coordinate packet recovered from Route56.

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

Frattini affine-fibre coordinate data recovered from Route56.

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

Coherent Route56 candidate exact-image pair.

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

Drop-in candidate lift-partition provider whose closure bypasses the seven Route36 coordinate leaves.