Candidate scalar/Frattini route29 proofs

Route29 keeps the route28 downstream provider shape

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

but does not use the two route28 candidate residual names. It strictly refines them as follows.

• The canonical middle R-obstruction map is assembled from scalar-pushout values on the middle exact-image source and their linearity in lambda : B.XR.
• The route28 Frattini cardinality packet is reduced to the Fourier zero-obstruction count #X_top = z_R * #{x : X_mid // o x = 0}. The sigma-cardinality of the canonical affine lift fibres is then theorem-level from the existing torsor-count lemma and the canonical affine-fibre torsor.

Route29 scalar-pushout residuals

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

Route29 canonical scalar-pushout value packet.

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

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

Route29 scalar-pushout linearity packet.

Manuscript anchor: Section 8, lem:obstructionseparation. This records that the selected scalar-pushout values are linear in the invariant character lambda : X_R, allowing Lean to assemble an R-valued obstruction.

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

Route29 scalar evaluator assembled from scalar-pushout values and linearity.

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

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

Route29 Frattini/Fourier residual

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

Route29 Frattini Fourier count packet.

Manuscript anchor: Section 8, prop:finalfourier. This is the numerator form of the final Frattini obstruction count for the chosen canonical middle obstruction: top exact-image candidate maps are counted as z_R times the unobstructed middle exact-image locus. The conversion from this statement to the full route28 cardinality packet is theorem-level below.

• top_count_eq : Nat.card centralCoverCandidateSource = B.zR * Nat.card { x : D.obstructionIndexToBaseMapData.O.X // D.obstructionIndexToBaseMapData.O.o x = 0 }

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

Route29 residual for the final Fourier zero-obstruction count.

theorem Q2Presentation.Induction.centralCover_candidateRoute29CanonicalAffineFiberSigmaCardinality {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : Nat.card ((x : { x : D.obstructionIndexToBaseMapData.O.X // D.obstructionIndexToBaseMapData.O.o x = 0 }) × D.affineFiberTorsorData.F.Lift x) = B.zR * Nat.card { x : D.obstructionIndexToBaseMapData.O.X // D.obstructionIndexToBaseMapData.O.o x = 0 }

The sigma-cardinality of the canonical affine fibres is theorem-level from the existing torsor-count mechanism.

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

Route29 derives the full Frattini exact-image cardinality packet from the strictly smaller Fourier zero-obstruction count plus theorem-level fibre cardinality.

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

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

Route-ready reassembly

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

Route29 coherent direct exact-image residual data assembled from the scalar-pushout obstruction and the Frattini Fourier count.

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

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

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

Route29 middle exact-image obstruction evaluation.

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

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

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

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

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

Route29 candidate lift-partition provider in the same B T Q shape as the route28 provider, with no dependency on the route28 residual names.