Candidate scalar/Frattini route39 proofs

Route39 keeps the Route38 integration shape

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

but avoids the three Route38 candidate residual names.

• Scalar side: instead of pointwise values plus additivity for an arbitrary externally supplied family, Route39 asks for one selected scalar-pushout value family together with additivity for that same family. Homogeneity over ZMod 2 is theorem-level from the Route36 argument.
• Frattini side: instead of the finite exact-image transform packet, Route39 asks for the final Fourier zero-locus count. The sigma-cardinality of the regular affine R-fibres is theorem-level, so this recovers the Route38 cardinal transform without using the Route38 transform axiom.

This is a strict lowering of the Route38 candidate frontier: the exported provider's axiom closure names the two Route39 packets below, not centralCover_candidateRoute38ScalarPushoutValueAtData, centralCover_candidateRoute38ScalarPushoutAdditivityData, or centralCover_candidateRoute38FrattiniExactImageTransformData.

Route39 scalar packet: one selected scalar-pushout family

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

Additivity in lambda : B.XR for one selected scalar-pushout value family.

This is intentionally not quantified over arbitrary pointwise families. It is the selected family used to assemble the middle R-obstruction in Section 8, lem:obstructionseparation.

• map_add (x : centralCoverCandidateMiddleSource T) (lam mu : ↥B.XR) : V.scalarPushoutValue (lam + mu) x = V.scalarPushoutValue lam x + V.scalarPushoutValue mu x

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

Route39 selected scalar-pushout family.

This coherent packet replaces Route38's pointwise value axiom plus its arbitrary-family additivity axiom for the route-needed construction.

• valueData : CentralCoverCandidateMiddleScalarPushoutValueData B T
• additivity : CentralCoverCandidateRoute39ScalarPushoutAdditivityData self.valueData

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

Route39 scalar-pushout selected-family packet.

def Q2Presentation.Induction.CentralCoverCandidateRoute39ScalarPushoutSelectedFamilyData.pointwiseFamily {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute39ScalarPushoutSelectedFamilyData B T) : CentralCoverCandidateMiddleScalarPushoutFamilyData B T

The Route39 value family as the pointwise family expected by the current scalar-pushout API.

Equations

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

def Q2Presentation.Induction.CentralCoverCandidateRoute39ScalarPushoutSelectedFamilyData.valueAtData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute39ScalarPushoutSelectedFamilyData B T) (lam : ↥B.XR) : CentralCoverCandidateMiddleScalarPushoutValueAtData B T lam

A pointwise Route38-style value extracted from the selected Route39 family.

Equations

• D.valueAtData lam = D.pointwiseFamily.valueAt lam

def Q2Presentation.Induction.CentralCoverCandidateRoute39ScalarPushoutSelectedFamilyData.pointwiseAdditivityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute39ScalarPushoutSelectedFamilyData B T) : CentralCoverCandidateMiddleScalarPushoutAdditivityData D.pointwiseFamily

Additivity for the pointwise family extracted from the selected Route39 family.

Equations

• D.pointwiseAdditivityData = { map_add := ⋯ }

theorem Q2Presentation.Induction.centralCover_candidateRoute38ScalarPushoutValueAtData_from_scalarFrattiniRoute39 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (lam : ↥B.XR) : Nonempty (CentralCoverCandidateMiddleScalarPushoutValueAtData B T lam)

Route38's pointwise value shape, recovered from the selected Route39 scalar family rather than from the Route38 value axiom.

theorem Q2Presentation.Induction.centralCover_candidateRoute39SelectedScalarPushoutAdditivityData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty ((V : CentralCoverCandidateMiddleScalarPushoutFamilyData B T) × CentralCoverCandidateMiddleScalarPushoutAdditivityData V)

The selected Route39 scalar family and its additivity, in the route-needed existential form. This is the replacement for Route38's arbitrary-family additivity residual.

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

Route37 scalar packet recovered from the selected Route39 scalar family.

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

Route39 scalar-obstruction evaluator. Homogeneity is derived from the selected additivity law over ZMod 2.

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

Route39 middle R-lift obstruction map.

Route39 Frattini packet: final Fourier zero-locus count

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

Route39 Frattini/Fourier zero-locus packet.

This is the numerator count in manuscript prop:finalfourier: top exact-image candidate maps are counted as z_R times the unobstructed middle exact-image locus for the selected R-obstruction.

• 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_candidateRoute39FrattiniFourierZeroLocusData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : Nonempty (CentralCoverCandidateRoute39FrattiniFourierZeroLocusData B T D)

Route39 residual for the final Frattini Fourier zero-obstruction count.

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

Route39 recovers the finite Frattini exact-image cardinality packet from the final Fourier zero-locus count.

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

Route38's Frattini transform shape, recovered from the Route39 Fourier zero-locus packet rather than from the Route38 transform axiom.

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

Route39 Frattini exact-image partition for the selected middle obstruction.

Route-ready reassembly

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

Route39 direct exact-image residual data from the selected scalar family and the final Fourier zero-locus packet.

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

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

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

Route39 candidate lift-partition provider in the same B T Q shape as Route38, with the three Route38 candidate residual names replaced by two selected manuscript-shaped Route39 packets.