Candidate scalar/Frattini Route85 closers

This sidecar is a drop-in candidate-side refinement for the Route84 work route. Route84 consumes CandidateScalarFrattiniRoute81Closers, whose axiom closure exposes the five semantic scalar/Frattini packets

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

Route85 does not use those five packets. Instead it routes through the finer manuscript-shaped API isolated in CandidateScalarFrattiniActualClosers: pointwise scalar-pushout tests, additivity and homogeneity for the selected scalar family, a base Frattini coordinate, a fibre coordinate over that base, a curried fibre realization, and the two inverse laws.

The public theorem

centralCover_candidateLiftPartitionData_from_route85

has the same B T Q call shape as the Route81 provider, so an integrated work route can switch to it without changing downstream Fourier/recursion code.

Selected scalar-pushout packet

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

Route85 scalar packet: one selected scalar-pushout family together with the two linearity laws needed to assemble the middle R-valued obstruction.

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

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

The old all-lambda value packet carried by the selected scalar family.

Equations

• S.valueData = S.scalarFamily.valueData

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

The old linearity packet, now projected from additivity and homogeneity of the selected pointwise scalar-pushout family.

Equations

• S.linearityData = S.scalarFamily.linearityData S.additivity S.homogeneity

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

Scalar-obstruction evaluator assembled from the selected pointwise scalar pushout family and its two linearity laws.

Equations

• S.evaluatorData = S.scalarFamily.evaluatorData S.additivity S.homogeneity

def Q2Presentation.Induction.CentralCoverCandidateRoute85ScalarPushoutData.middleObstructionMapData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (S : CentralCoverCandidateRoute85ScalarPushoutData B T) : CentralCoverCandidateMiddleRLiftObstructionMapData B T

The middle R-lift obstruction map selected by the Route85 scalar data.

Equations

• S.middleObstructionMapData = { obstruction := S.evaluatorData.obstructionEvaluator }

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

Route85 scalar data from pointwise scalar-pushout values plus additivity and homogeneity. This is the scalar half of the lower Route85 frontier.

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

The selected value-and-linearity pair replacing the two scalar Route81 semantic packets.

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

Route85 middle R-lift obstruction map from the selected pointwise scalar-pushout family and its additivity/homogeneity laws.

Selected Frattini coordinate packet

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

Route85 Frattini coordinate system for one selected middle obstruction.

This packages the lower base coordinate, fibre coordinate, curried realization, and both inverse laws. It is finer than the three uncurried Route81 semantic Frattini packets.

• base : CentralCoverCandidateFrattiniBaseCoordinateData B T D
• fiber : CentralCoverCandidateFrattiniFiberCoordinateData self.base
• realization : CentralCoverCandidateFrattiniFiberRealizationData B T D
• realize_lift : CentralCoverCandidateFrattiniRealizeLiftCoordinateData self.base self.fiber self.realization
• lift_realize : CentralCoverCandidateFrattiniLiftCoordinateRealizeData self.base self.fiber self.realization

def Q2Presentation.Induction.CentralCoverCandidateRoute85FrattiniCoordinateSystemData.liftCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (S : CentralCoverCandidateRoute85FrattiniCoordinateSystemData B T D) : CentralCoverCandidateFrattiniLiftCoordinateData B T D

Uncurried Frattini lift-coordinate map induced by the selected base/fibre coordinates.

Equations

• S.liftCoordinateData = S.base.liftCoordinateData S.fiber

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

Uncurried Frattini realization map induced by the selected curried fibre realization.

Equations

• S.realizationData = S.realization.realizationData

def Q2Presentation.Induction.CentralCoverCandidateRoute85FrattiniCoordinateSystemData.coordinateInverseData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (S : CentralCoverCandidateRoute85FrattiniCoordinateSystemData B T D) : CentralCoverCandidateFrattiniCoordinateInverseData S.liftCoordinateData S.realizationData

The uncurried inverse-law packet induced by the two lower inverse laws.

Equations

• S.coordinateInverseData = { realize_liftCoordinate := ⋯, liftCoordinate_realize := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateRoute85FrattiniCoordinateSystemData.affineFiberCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (S : CentralCoverCandidateRoute85FrattiniCoordinateSystemData B T D) : CentralCoverCandidateFrattiniAffineFiberCoordinateData B T D

The current Frattini affine-fibre coordinate packet induced by the selected Route85 coordinate system.

Equations

• S.affineFiberCoordinateData = S.liftCoordinateData.coordinateData S.realizationData S.coordinateInverseData

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

The exact-image partition induced by the selected Route85 Frattini coordinate system.

Equations

• S.frattiniExactImage = { partition := { bij := S.affineFiberCoordinateData.equiv } }

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

Route85 Frattini data from base/fibre coordinates, curried realization, and both inverse laws. This is the Frattini half of the lower Route85 frontier.

theorem Q2Presentation.Induction.centralCover_candidateRoute85SelectedFrattiniCoordinateData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty ((D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) × (L : CentralCoverCandidateFrattiniLiftCoordinateData B T D) × (R : CentralCoverCandidateFrattiniRealizationData B T D) × CentralCoverCandidateFrattiniCoordinateInverseData L R)

The selected uncurried Frattini coordinate/realization/inverse tuple replacing the three Frattini Route81 semantic packets.

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

Route85 Frattini exact-image partition for a supplied middle obstruction, assembled from lower base/fibre/realization/inverse-law packets.

Coherent selected scalar/Frattini packet

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

Route85's coherent selected scalar/Frattini packet.

The selected middle obstruction is derived from the selected scalar-pushout family, and the Frattini coordinate system is attached to that same middle obstruction.

• scalar : CentralCoverCandidateRoute85ScalarPushoutData B T
• middleObstruction : CentralCoverCandidateMiddleRLiftObstructionMapData B T
• middleObstruction_eq : self.middleObstruction = self.scalar.middleObstructionMapData
• frattini : CentralCoverCandidateRoute85FrattiniCoordinateSystemData B T self.middleObstruction

def Q2Presentation.Induction.CentralCoverCandidateRoute85SelectedScalarFrattiniData.directExactImageResidualData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (S : CentralCoverCandidateRoute85SelectedScalarFrattiniData B T) : CentralCoverCandidateDirectExactImageResidualData B T

Reassemble coherent direct exact-image residual data from the Route85 selected scalar/Frattini packet.

Equations

• S.directExactImageResidualData = { middleObstruction := S.middleObstruction, frattiniPartition := S.frattini.frattiniExactImage }

def Q2Presentation.Induction.CentralCoverCandidateRoute85SelectedScalarFrattiniData.liftPartitionData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (S : CentralCoverCandidateRoute85SelectedScalarFrattiniData B T) (Q : CentralCoverCandidateQuotientFrameMapData B T) : CentralCoverCandidateLiftPartitionData B

Reassemble the candidate lift-partition packet from Route85 data and the route-supplied quotient-frame map.

Equations

• S.liftPartitionData Q = S.directExactImageResidualData.liftPartitionData Q

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

The single coherent Route85 selected packet, built from the lower actual scalar and Frattini packets.

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

Coherent direct exact-image residual data through the lower Route85 scalar and Frattini packets.

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

Route85 drop-in candidate lift-partition provider for the integrated route.

This has the same public call shape as Route81, but its axiom closure replaces Route81's five semantic scalar/Frattini packets by lower pointwise scalar and base/fibre Frattini packets from CandidateScalarFrattiniActualClosers.