Documentation

Q2Presentation.Induction.CandidateScalarFrattiniRoute38Proofs

Candidate scalar/Frattini route38 proofs #

Route38 keeps the Route37 drop-in provider shape

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

but it does not call the two Route37 candidate residual axioms

Instead it exposes smaller Section 8 packets.

This is not a full closure of the candidate calculation: the actual word-level scalar pushout values and the finite central-cover transform remain manuscript inputs. The lowering is strict at the Route37 frontier because the exported provider's axiom closure no longer contains either Route37 residual name.

Route38 scalar-pushout packets #

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

Route38 scalar-pushout value packet.

For one invariant scalar pushout lambda : X_R, this is the scalar obstruction value on the candidate middle exact-image source. Manuscript anchor: Section 8, lem:obstructionseparation.

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

Route38 scalar-pushout additivity packet.

The additivity is asserted only for the selected pointwise family assembled from the route38 value packets, which is the family used to build the middle R-obstruction. Homogeneity over ZMod 2 is theorem-level, inherited from the Route36 additivity argument.

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

The selected Route38 pointwise scalar-pushout family.

source
theorem Q2Presentation.Induction.centralCover_candidateScalarFrattiniRoute37ScalarData_from_scalarFrattiniRoute38 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) :
Nonempty (CentralCoverCandidateScalarFrattiniRoute37ScalarData B T)

Route38 replacement for Route37's broad scalar packet.

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

Route38 scalar-obstruction evaluator from pointwise scalar pushouts and additivity.

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

Route38 middle R-lift obstruction map.

Route38 Frattini central-cover transform packet #

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

Route38 Frattini exact-image transform in finite-cardinal form.

This is the cardinal shadow of the central-cover exact-image transform used in Section 8 (lem:covertransform, prop:finalfourier) for the selected middle obstruction and canonical affine R-lift fibres.

Instances For
    source
    axiom Q2Presentation.Induction.centralCover_candidateRoute38FrattiniExactImageTransformData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) :
    Nonempty (CentralCoverCandidateRoute38FrattiniExactImageTransformData B T D)

    Route38 Frattini central-cover transform packet.

    The actual bijective partition is not asserted here. Only the finite exact-image transform/cardinality statement remains as an input.

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

    Route38 replacement for Route37's broad Frattini partition packet.

    Route-ready reassembly #

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

    Route38 direct exact-image residual data from the lowered scalar and Frattini packets.

    source
    theorem Q2Presentation.Induction.centralCover_candidateRLiftSemanticData_from_scalarFrattiniRoute38 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B T) :
    Nonempty (CentralCoverCandidateRLiftSemanticData B T)

    Route38 semantic central R-lift data from the direct exact-image split and a route-supplied quotient-frame map.

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

    Route38 candidate lift-partition provider in the same B T Q shape as Route37, with both Route37 candidate residual names replaced by lower Section 8 packets.