Candidate scalar and Frattini actual closers

This sidecar refines the five current candidate Section 8 leaves exposed by CandidateScalarFrattiniSemanticClosers.lean.

The scalar obstruction is split into the manuscript's scalar-pushout tests, one packet for each lambda : X_R, together with the two linearity laws used to assemble the R-valued obstruction. The Frattini equivalence is split into a base exact-image coordinate, an affine R-lift coordinate over that base, a curried realization map, and the two inverse laws.

Scalar pushout values, one scalar test at a time

structure Q2Presentation.Induction.CentralCoverCandidateMiddleScalarPushoutValueAtData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (lam : ↥B.XR) : Type

Value of one invariant scalar pushout on the candidate middle exact-image source. This is the lambda-indexed scalar test in lem:obstructionseparation and prop:finalfourier.

• valueAt : centralCoverCandidateMiddleSource T → ZMod 2

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

The family of scalar-pushout values over all invariant scalar pushouts.

• valueAt (lam : ↥B.XR) : CentralCoverCandidateMiddleScalarPushoutValueAtData B T lam

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

Reassemble the previous all-lambda value packet from pointwise scalar pushout values.

Equations

• V.valueData = { scalarPushoutValue := fun (lam : ↥B.XR) (x : Q2Presentation.Induction.centralCoverCandidateMiddleSource T) => (V.valueAt lam).valueAt x }

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

Additivity in the invariant scalar-pushout parameter.

• map_add (x : centralCoverCandidateMiddleSource T) (lam mu : ↥B.XR) : (V.valueAt (lam + mu)).valueAt x = (V.valueAt lam).valueAt x + (V.valueAt mu).valueAt x

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

Homogeneity in the invariant scalar-pushout parameter.

• map_smul (x : centralCoverCandidateMiddleSource T) (a : ZMod 2) (lam : ↥B.XR) : (V.valueAt (a • lam)).valueAt x = a • (V.valueAt lam).valueAt x

def Q2Presentation.Induction.CentralCoverCandidateMiddleScalarPushoutFamilyData.linearityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (V : CentralCoverCandidateMiddleScalarPushoutFamilyData B T) (A : CentralCoverCandidateMiddleScalarPushoutAdditivityData V) (H : CentralCoverCandidateMiddleScalarPushoutHomogeneityData V) : CentralCoverCandidateMiddleScalarPushoutLinearityData V.valueData

Reassemble the old linearity packet for the value data determined by this pointwise scalar-pushout family.

Equations

• V.linearityData A H = { map_add := ⋯, map_smul := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateMiddleScalarPushoutFamilyData.evaluatorData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (V : CentralCoverCandidateMiddleScalarPushoutFamilyData B T) (A : CentralCoverCandidateMiddleScalarPushoutAdditivityData V) (H : CentralCoverCandidateMiddleScalarPushoutHomogeneityData V) : CentralCoverCandidateMiddleScalarObstructionEvaluatorData B T

Assemble the current scalar-obstruction evaluator directly from the pointwise scalar pushouts and their linearity.

Equations

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

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

Pointwise scalar-pushout value packet.

axiom Q2Presentation.Induction.centralCover_candidateMiddleScalarPushoutAdditivityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (V : CentralCoverCandidateMiddleScalarPushoutFamilyData B T) : Nonempty (CentralCoverCandidateMiddleScalarPushoutAdditivityData V)

Additivity packet for the pointwise scalar-pushout family.

axiom Q2Presentation.Induction.centralCover_candidateMiddleScalarPushoutHomogeneityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (V : CentralCoverCandidateMiddleScalarPushoutFamilyData B T) : Nonempty (CentralCoverCandidateMiddleScalarPushoutHomogeneityData V)

Homogeneity packet for the pointwise scalar-pushout family.

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

Scalar value family assembled from pointwise scalar tests.

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

Previous value packet reduced to pointwise scalar-pushout tests.

theorem Q2Presentation.Induction.centralCover_candidateMiddleScalarPushoutLinearityData_from_actualClosers {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (V : CentralCoverCandidateMiddleScalarPushoutFamilyData B T) : Nonempty (CentralCoverCandidateMiddleScalarPushoutLinearityData V.valueData)

Previous linearity packet reduced to additivity and homogeneity for the chosen pointwise scalar-pushout family.

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

Current scalar-obstruction evaluator from pointwise scalar-pushout values, additivity, and homogeneity.

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

Middle R-lift obstruction map through the pointwise scalar-pushout packets.

Frattini coordinates split into base and fibre data

@[reducible, inline]

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

The unobstructed middle exact-image index used by the Frattini affine fibres.

Equations

• Q2Presentation.Induction.CentralCoverCandidateFrattiniBaseTarget B T D = { x : D.obstructionIndexToBaseMapData.O.X // D.obstructionIndexToBaseMapData.O.o x = 0 }

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

Base exact-image coordinate of a top candidate map.

• baseCoordinate : centralCoverCandidateSource → CentralCoverCandidateFrattiniBaseTarget B T D

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

Affine R-lift coordinate over the selected base exact-image coordinate.

• fiberCoordinate (f : centralCoverCandidateSource) : D.affineFiberTorsorData.F.Lift (C.baseCoordinate f)

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

Curried realization from an unobstructed base point and its affine R-lift coordinate.

• realizeFiber (x : CentralCoverCandidateFrattiniBaseTarget B T D) : D.affineFiberTorsorData.F.Lift x → centralCoverCandidateSource

def Q2Presentation.Induction.CentralCoverCandidateFrattiniBaseCoordinateData.liftCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) (F : CentralCoverCandidateFrattiniFiberCoordinateData C) : CentralCoverCandidateFrattiniLiftCoordinateData B T D

Reassemble the old lift-coordinate map from base and fibre coordinates.

Equations

• C.liftCoordinateData F = { liftCoordinate := fun (f : Q2Presentation.Induction.centralCoverCandidateSource) => ⟨C.baseCoordinate f, F.fiberCoordinate f⟩ }

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

Reassemble the old realization map from its curried fibre form.

Equations

• R.realizationData = { realizeCoordinate := fun (y : Q2Presentation.Induction.CentralCoverCandidateFrattiniAffineFiberTarget B T D) => R.realizeFiber y.fst y.snd }

structure Q2Presentation.Induction.CentralCoverCandidateFrattiniRealizeLiftCoordinateData {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) : Type

Realization after taking base and affine fibre coordinates is the original top exact-image map.

• realize_liftCoordinate (f : centralCoverCandidateSource) : R.realizeFiber (C.baseCoordinate f) (F.fiberCoordinate f) = f

structure Q2Presentation.Induction.CentralCoverCandidateFrattiniLiftCoordinateRealizeData {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) : Type

Taking base and affine fibre coordinates after realization recovers the original unobstructed affine fibre point.

• liftCoordinate_realize (y : CentralCoverCandidateFrattiniAffineFiberTarget B T D) : ⟨C.baseCoordinate (R.realizeFiber y.fst y.snd), F.fiberCoordinate (R.realizeFiber y.fst y.snd)⟩ = y

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

Frattini base-coordinate packet.

axiom Q2Presentation.Induction.centralCover_candidateFrattiniFiberCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) : Nonempty (CentralCoverCandidateFrattiniFiberCoordinateData C)

Frattini affine fibre-coordinate packet over the selected base coordinate.

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

Frattini realization packet in curried base/fibre form.

axiom Q2Presentation.Induction.centralCover_candidateFrattiniRealizeLiftCoordinateData {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) : Nonempty (CentralCoverCandidateFrattiniRealizeLiftCoordinateData C F R)

One inverse law for the Frattini coordinate/realization pair.

axiom Q2Presentation.Induction.centralCover_candidateFrattiniLiftCoordinateRealizeData {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) : Nonempty (CentralCoverCandidateFrattiniLiftCoordinateRealizeData C F R)

The other inverse law for the Frattini coordinate/realization pair.

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

Previous lift-coordinate packet reduced to base and fibre coordinates.

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

Previous realization packet reduced to curried base/fibre realization.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniCoordinateInverseData_from_actualClosers {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) : Nonempty (CentralCoverCandidateFrattiniCoordinateInverseData (C.liftCoordinateData F) R.realizationData)

Coordinate inverse laws for the maps assembled from base/fibre coordinate and curried realization packets.

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

Current Frattini affine-fibre coordinate data through the lower base/fibre coordinate and realization packets.

theorem Q2Presentation.Induction.centralCover_candidateFrattiniAffineFiberPartition_residual_from_actualClosers {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 through the lower coordinate/realization packets.

Route-ready reassembly

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

Coherent direct exact-image residual data using the lower scalar and Frattini packets in this file.

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

Candidate lift-partition data through the lower scalar and Frattini packets, with the quotient-frame map supplied by the current route.