Candidate scalar and Frattini semantic closers

This sidecar pushes the current candidate Section 8 residuals one step lower without routing through retired broad packets.

The current visible residuals are:

• centralCover_candidateMiddleScalarObstructionEvaluatorData;
• centralCover_candidateFrattiniAffineFiberCoordinateData.

Here they are replaced by smaller manuscript-shaped leaves:

• scalar pushout values indexed by lambda in X_R, plus a separate linearity packet in lambda;
• a Frattini lift-coordinate map, a realization map, and the two inverse laws identifying top exact-image maps with unobstructed affine fibres.

The theorem wrappers at the bottom return the current route's packet shapes, so a coordinator can integrate this sidecar without changing downstream target types.

Scalar pushout values and linearity

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

Scalar-pushout values of the middle candidate obstruction.

For each invariant scalar pushout lambda : X_R, this gives the scalar obstruction value on the canonical middle exact-image source. Linearity in lambda is deliberately a separate packet below.

• scalarPushoutValue (lam : ↥B.XR) : centralCoverCandidateMiddleSource T → ZMod 2

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

Linearity of the scalar-pushout obstruction values in the invariant character lambda.

• map_add (x : centralCoverCandidateMiddleSource T) (lam mu : ↥B.XR) : D.scalarPushoutValue (lam + mu) x = D.scalarPushoutValue lam x + D.scalarPushoutValue mu x
• map_smul (x : centralCoverCandidateMiddleSource T) (a : ZMod 2) (lam : ↥B.XR) : D.scalarPushoutValue (a • lam) x = a • D.scalarPushoutValue lam x

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

Reassemble the current scalar-obstruction evaluator packet from scalar pushout values and their linearity in lambda.

Equations

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

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

Remaining scalar pushout value packet for the candidate middle obstruction.

axiom Q2Presentation.Induction.centralCover_candidateMiddleScalarPushoutLinearityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleScalarPushoutValueData B T) : Nonempty (CentralCoverCandidateMiddleScalarPushoutLinearityData D)

Remaining scalar pushout linearity packet for the candidate middle obstruction.

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

Current scalar-obstruction evaluator data reduced to scalar pushout values plus scalar-pushout linearity.

def Q2Presentation.Induction.centralCover_candidateMiddleRLiftObstructionEvaluator_from_scalarFrattiniSemanticClosers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : centralCoverCandidateMiddleSource T → B.obstructionSpace

Middle R-lift obstruction evaluator assembled through the narrower scalar pushout packets from this sidecar.

Equations

• Q2Presentation.Induction.centralCover_candidateMiddleRLiftObstructionEvaluator_from_scalarFrattiniSemanticClosers B T = (Classical.choice ⋯).obstructionEvaluator

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

Current middle obstruction-map packet reduced through scalar pushout values and their linearity.

Frattini coordinate and realization maps

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

Coordinate map from top exact-image candidate maps to the unobstructed middle exact-image point and its canonical affine R-lift fibre.

• liftCoordinate : centralCoverCandidateSource → CentralCoverCandidateFrattiniAffineFiberTarget B T D

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

Realization map from an unobstructed middle exact-image point and affine R-lift coordinate back to a top exact-image candidate map.

• realizeCoordinate : CentralCoverCandidateFrattiniAffineFiberTarget B T D → centralCoverCandidateSource

structure Q2Presentation.Induction.CentralCoverCandidateFrattiniCoordinateInverseData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (L : CentralCoverCandidateFrattiniLiftCoordinateData B T D) (R : CentralCoverCandidateFrattiniRealizationData B T D) : Type

The coordinate and realization maps are inverse to one another.

• realize_liftCoordinate (f : centralCoverCandidateSource) : R.realizeCoordinate (L.liftCoordinate f) = f
• liftCoordinate_realize (y : CentralCoverCandidateFrattiniAffineFiberTarget B T D) : L.liftCoordinate (R.realizeCoordinate y) = y

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

Reassemble the current Frattini affine-fibre coordinate packet from a coordinate map, a realization map, and inverse laws.

Equations

• L.coordinateData R I = { liftCoordinate := L.liftCoordinate, realizeCoordinate := R.realizeCoordinate, realize_liftCoordinate := ⋯, liftCoordinate_realize := ⋯ }

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

Remaining Frattini lift-coordinate packet.

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

Remaining Frattini realization packet.

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

Remaining Frattini inverse-law packet tying the coordinate and realization maps together.

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

Current Frattini affine-fibre coordinate data reduced to coordinate, realization, and inverse-law packets.

def Q2Presentation.Induction.centralCover_candidateFrattiniAffineFiberExactImageEquiv_from_scalarFrattiniSemanticClosers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : centralCoverCandidateSource ≃ CentralCoverCandidateFrattiniAffineFiberTarget B T D

Frattini exact-image equivalence assembled through the narrower coordinate, realization, and inverse-law packets from this sidecar.

Equations

• Q2Presentation.Induction.centralCover_candidateFrattiniAffineFiberExactImageEquiv_from_scalarFrattiniSemanticClosers B T D = (Classical.choice ⋯).equiv

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

Current Frattini partition packet reduced through coordinate, realization, and inverse-law packets.

Route-ready wrappers

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

Coherent direct exact-image residual data using only this sidecar's smaller scalar and Frattini packets.

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

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