Documentation

Q2Presentation.Induction.CandidateScalarFrattiniRoute30Proofs

Candidate scalar/Frattini route30 proofs #

Route30 keeps the route29 downstream provider shape

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

and removes the two route28 candidate residual names from the provider closure. It also narrows the route29 scalar-linearity packet: the only scalar linearity content left as a residual is additivity in lambda : B.XR; homogeneity over ZMod 2 is proved below by the two scalar cases.

The final Frattini cardinality input remains the route29 Fourier zero-locus packet, because that is the manuscript's prop:finalfourier statement tying the top exact-image count to the unobstructed middle locus. The affine fibre sigma-cardinality factor is theorem-level from the existing torsor mechanism.

Route30 scalar additivity residual #

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

Additivity in lambda for a fixed route29-style scalar-pushout value packet. This local route30 structure avoids importing the broader pointwise actual-closer sidecar just for its additivity wrapper.

Instances For
    source
    axiom Q2Presentation.Induction.centralCover_candidateRoute30CanonicalScalarPushoutAdditivityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (V : CentralCoverCandidateMiddleScalarPushoutValueData B T) :
    Nonempty (CentralCoverCandidateRoute30ScalarPushoutAdditivityData V)

    Route30 scalar-pushout additivity packet.

    Manuscript anchor: Section 8, lem:obstructionseparation. Once the scalar pushout values are fixed, additivity in the invariant character lambda : X_R is the only nontrivial F_2-linearity law left as a residual here; homogeneity is discharged theorem-level by centralCover_candidateRoute30ScalarPushoutHomogeneity.

    source
    theorem Q2Presentation.Induction.centralCover_candidateRoute30ScalarPushoutHomogeneity {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (V : CentralCoverCandidateMiddleScalarPushoutValueData B T) (A : CentralCoverCandidateRoute30ScalarPushoutAdditivityData V) (x : centralCoverCandidateMiddleSource T) (a : ZMod 2) (lam : ↥B.XR) :
    V.scalarPushoutValue (a • lam) x = a • V.scalarPushoutValue lam x

    Additivity of scalar-pushout values over ZMod 2 implies homogeneity.

    This is the small theorem-level replacement for the homogeneity half of the route29 full-linearity packet. The a = 0 case uses additivity at 0 + 0 to show the zero scalar value is zero; the a = 1 case is definitional.

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

    Route30 linearly assembles the scalar-pushout values from value data plus additivity only; scalar homogeneity is proved over ZMod 2.

    Route30 provider #

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

    Route30 scalar evaluator assembled without the route29 full-linearity residual and without either route28 canonical residual name.

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

    Route30 middle R-lift obstruction map on the canonical middle exact-image source.

    source
    theorem Q2Presentation.Induction.centralCover_candidateFrattiniExactImageCardinalityData_from_scalarFrattiniRoute30 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) :
    Nonempty (CentralCoverCandidateFrattiniExactImageCardinalityData B T D.obstructionIndexToBaseMapData.O D.affineFiberTorsorData.Z D.affineFiberTorsorData.F)

    Route30 derives the full Frattini exact-image cardinality packet from the route29 Fourier zero-obstruction count plus theorem-level affine-fibre torsor cardinality.

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

    Route30 Frattini exact-image partition for the selected middle obstruction map.

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

    Route30 coherent direct exact-image residual data assembled from the additivity-only scalar-pushout route and the Frattini Fourier count.

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

    Route30 final exact-image residual for the selected middle obstruction and matching Frattini exact-image partition.

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

    Route30 middle exact-image obstruction evaluation.

    source
    theorem Q2Presentation.Induction.centralCover_candidateTopExactImageAffineFiberEquivSigma_from_scalarFrattiniRoute30 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) :
    Nonempty ((E : CentralCoverCandidateMiddleExactImageObstructionEvaluationData B T) × CentralCoverCandidateTopExactImageAffineFiberEquivData B T E)

    Route30 dependent top affine-fibre packet, retaining the selected middle obstruction evaluation.

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

    Semantic central R-lift data from route30 and a supplied quotient-frame map.

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

    Route30 candidate lift-partition provider in the same B T Q shape as the route28/route29 providers, with no dependency on either route28 residual name.