Current candidate semantic closers

This sidecar owns the current candidate Section 8 semantic packets consumed by CandidateCurrentPacketSplitClosers.lean.

The two exported constants keep the current downstream names, but their axiom closure is split into more manuscript-shaped data:

• the R-valued middle obstruction evaluator is assembled from scalar pushout evaluations that are linear in lambda in X_R;
• the Frattini affine-fibre exact-image equivalence is assembled from explicit coordinate and realization maps between top exact-image maps and unobstructed canonical affine fibres.

No retired obstruction/cardinality packet is used here.

Scalar-pushout construction of the middle R-obstruction evaluator

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

Scalar-pushout evaluations of the candidate middle obstruction.

For every middle exact-image map, the values against invariant scalar pushouts are linear in lambda : X_R; by B.obstructionSpace = Dual X_R, this assembles the R-valued obstruction used in the current route.

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

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

Assemble the scalar-pushout evaluations into the R-valued obstruction function on the canonical middle exact-image source.

Equations

• D.obstructionEvaluator x = { toFun := fun (lam : ↥B.XR) => D.scalarObstruction x lam, map_add' := ⋯, map_smul' := ⋯ }

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

Remaining scalar-pushout semantic packet for the current middle obstruction evaluator.

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

Current middle R-lift obstruction evaluator, assembled from scalar pushout evaluations rather than asserted as a primitive R-valued map.

Equations

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

Frattini affine-fibre coordinates and realization

@[reducible, inline]

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

The dependent sum of unobstructed canonical affine fibres for a selected middle obstruction map.

Equations

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

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

Coordinate/realization form of the Frattini affine-fibre exact-image equivalence.

liftCoordinate sends a top exact-image candidate map to its unobstructed middle obstruction index plus affine R-lift coordinate. realizeCoordinate is the Frattini realization map back to a top exact-image map.

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

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

Convert coordinate/realization data into the exact-image equivalence used by the existing partition wrapper.

Equations

• E.equiv = { toFun := E.liftCoordinate, invFun := E.realizeCoordinate, left_inv := ⋯, right_inv := ⋯ }

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

Remaining Frattini affine-fibre semantic packet for the current selected middle obstruction map.

def Q2Presentation.Induction.centralCover_candidateFrattiniAffineFiberExactImageEquiv {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : centralCoverCandidateSource ≃ (x : { x : D.obstructionIndexToBaseMapData.O.X // D.obstructionIndexToBaseMapData.O.o x = 0 }) × D.affineFiberTorsorData.F.Lift x

Current Frattini affine-fibre exact-image equivalence, assembled from coordinate and realization maps rather than asserted as a primitive equivalence.

Equations

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