Candidate Route106 coordinate closers

This sidecar is candidate Section 8 only. It does not edit any integrated route file.

The Route103 coordinate provider lowers the current candidate exact-image residuals to scalar pushout value/additivity leaves plus the base/fibre Frattini coordinate system. This file lowers the scalar part one step further:

• the zero scalar pushout is theorem-level, with value identically 0;
• full additivity is recovered from the zero case, the equal-parameter case over ZMod 2, and one residual only for nonzero distinct scalar parameters.

The Frattini side remains at the Route85 base/fibre/realization split, so the final theorem has the same route-ready shape as the Route103 coordinate provider, with a strictly smaller scalar-pushout frontier.

Scalar pushout values with the zero scalar split off

structure Q2Presentation.Induction.CentralCoverCandidateMiddleScalarPushoutNonzeroValueAtData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (lam : ↥B.XR) : Type

Scalar-pushout value for a nonzero invariant scalar pushout. The zero scalar pushout is closed theorem-level below by the constant-zero value.

• valueAt : centralCoverCandidateMiddleSource T → ZMod 2

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

Repackage a nonzero scalar-pushout value as the existing pointwise value packet for that scalar.

Equations

• D.valueData = { valueAt := D.valueAt }

def Q2Presentation.Induction.centralCover_candidateMiddleZeroScalarPushoutValueAtData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : CentralCoverCandidateMiddleScalarPushoutValueAtData B T 0

The theorem-level value packet for the zero scalar pushout.

Equations

• Q2Presentation.Induction.centralCover_candidateMiddleZeroScalarPushoutValueAtData B T = { valueAt := fun (x : Q2Presentation.Induction.centralCoverCandidateMiddleSource T) => 0 }

axiom Q2Presentation.Induction.centralCover_candidateMiddleScalarPushoutNonzeroValueAtData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (lam : ↥B.XR) (h : lam ≠ 0) : Nonempty (CentralCoverCandidateMiddleScalarPushoutNonzeroValueAtData B T lam)

Remaining value residual, only for nonzero scalar pushouts.

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

Pointwise scalar-pushout values recovered from the nonzero-only residual plus the theorem-level zero scalar value.

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

The selected scalar-pushout family used by the Route106 coordinate closer. It is definitionally zero at lambda = 0 and otherwise uses the nonzero value residual.

Equations

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

theorem Q2Presentation.Induction.centralCover_candidateRoute106ScalarPushoutFamily_zero_value {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (x : centralCoverCandidateMiddleSource T) : ((centralCover_candidateRoute106ScalarPushoutFamily B T).valueAt 0).valueAt x = 0

Additivity reduced to nonzero distinct scalar pushouts

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

Additivity only in the genuinely residual case: both scalar pushouts are nonzero and distinct. The zero and equal-parameter cases are proved theorem-level over ZMod 2.

• map_add_nonzero_distinct (x : centralCoverCandidateMiddleSource T) (lam mu : ↥B.XR) : lam ≠ 0 → mu ≠ 0 → lam ≠ mu → (V.valueAt (lam + mu)).valueAt x = (V.valueAt lam).valueAt x + (V.valueAt mu).valueAt x

axiom Q2Presentation.Induction.centralCover_candidateMiddleScalarPushoutNonzeroDistinctAdditivityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (V : CentralCoverCandidateMiddleScalarPushoutFamilyData B T) : Nonempty (CentralCoverCandidateMiddleScalarPushoutNonzeroDistinctAdditivityData V)

Remaining additivity residual, restricted to nonzero distinct scalar pushout parameters for the selected family.

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

Route106 scalar packet: the selected scalar-pushout family, its theorem-level zero value, and additivity only for nonzero distinct scalar parameters.

• scalarFamily : CentralCoverCandidateMiddleScalarPushoutFamilyData B T
• zero_value (x : centralCoverCandidateMiddleSource T) : (self.scalarFamily.valueAt 0).valueAt x = 0
• additivityNonzeroDistinct : CentralCoverCandidateMiddleScalarPushoutNonzeroDistinctAdditivityData self.scalarFamily

def Q2Presentation.Induction.CentralCoverCandidateRoute106ScalarPushoutData.additivityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (S : CentralCoverCandidateRoute106ScalarPushoutData B T) : CentralCoverCandidateMiddleScalarPushoutAdditivityData S.scalarFamily

Full scalar-pushout additivity recovered from the nonzero-distinct residual. The cases with a zero parameter and the case lambda = mu are theorem-level.

Equations

• S.additivityData = { map_add := ⋯ }

def Q2Presentation.Induction.CentralCoverCandidateRoute106ScalarPushoutData.homogeneityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (S : CentralCoverCandidateRoute106ScalarPushoutData B T) : CentralCoverCandidateMiddleScalarPushoutHomogeneityData S.scalarFamily

Homogeneity over ZMod 2 follows from full additivity by the existing Route36 theorem.

Equations

• S.homogeneityData = Classical.choice ⋯

def Q2Presentation.Induction.CentralCoverCandidateRoute106ScalarPushoutData.valueData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (S : CentralCoverCandidateRoute106ScalarPushoutData B T) : CentralCoverCandidateMiddleScalarPushoutValueData B T

The all-lambda value packet carried by the selected scalar family.

Equations

• S.valueData = S.scalarFamily.valueData

def Q2Presentation.Induction.CentralCoverCandidateRoute106ScalarPushoutData.linearityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (S : CentralCoverCandidateRoute106ScalarPushoutData B T) : CentralCoverCandidateMiddleScalarPushoutLinearityData S.valueData

The old linearity packet recovered from the selected reduced scalar data.

Equations

• S.linearityData = S.scalarFamily.linearityData S.additivityData S.homogeneityData

def Q2Presentation.Induction.CentralCoverCandidateRoute106ScalarPushoutData.evaluatorData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (S : CentralCoverCandidateRoute106ScalarPushoutData B T) : CentralCoverCandidateMiddleScalarObstructionEvaluatorData B T

Scalar-obstruction evaluator assembled from the reduced scalar frontier.

Equations

• S.evaluatorData = S.scalarFamily.evaluatorData S.additivityData S.homogeneityData

def Q2Presentation.Induction.CentralCoverCandidateRoute106ScalarPushoutData.middleObstructionMapData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (S : CentralCoverCandidateRoute106ScalarPushoutData B T) : CentralCoverCandidateMiddleRLiftObstructionMapData B T

The middle R-lift obstruction map selected by the Route106 scalar data.

Equations

• S.middleObstructionMapData = { obstruction := S.evaluatorData.obstructionEvaluator }

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

Route106 scalar data from nonzero scalar values and nonzero-distinct additivity.

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

The selected value/additivity pair after the Route106 scalar lowering.

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

The selected value/linearity pair after the Route106 scalar lowering. Homogeneity is theorem-level from additivity over ZMod 2.

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

Route106 middle R-lift obstruction map from the reduced scalar frontier.

Route-ready scalar/Frattini reassembly

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

Route106 selected scalar/Frattini coordinate packet.

The scalar part uses the reduced Route106 frontier above. The Frattini part is the existing Route85 base/fibre/realization coordinate system attached to the middle obstruction selected by that scalar data.

• scalar : CentralCoverCandidateRoute106ScalarPushoutData B T
• middleObstruction : CentralCoverCandidateMiddleRLiftObstructionMapData B T
• middleObstruction_eq : self.middleObstruction = self.scalar.middleObstructionMapData
• frattini : CentralCoverCandidateRoute85FrattiniCoordinateSystemData B T self.middleObstruction

def Q2Presentation.Induction.CentralCoverCandidateRoute106SelectedScalarFrattiniData.directExactImageResidualData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (S : CentralCoverCandidateRoute106SelectedScalarFrattiniData B T) : CentralCoverCandidateDirectExactImageResidualData B T

Reassemble coherent direct exact-image residual data from the Route106 selected scalar/Frattini packet.

Equations

• S.directExactImageResidualData = { middleObstruction := S.middleObstruction, frattiniPartition := S.frattini.frattiniExactImage }

def Q2Presentation.Induction.CentralCoverCandidateRoute106SelectedScalarFrattiniData.liftPartitionData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (S : CentralCoverCandidateRoute106SelectedScalarFrattiniData B T) (Q : CentralCoverCandidateQuotientFrameMapData B T) : CentralCoverCandidateLiftPartitionData B

Reassemble the candidate lift-partition packet from Route106 coordinate data and the route-supplied quotient-frame map.

Equations

• S.liftPartitionData Q = S.directExactImageResidualData.liftPartitionData Q

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

The coherent Route106 selected packet: reduced scalar pushout data plus the Route85 Frattini coordinate system.

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

Coherent direct exact-image residual data through the Route106 coordinate lowering.

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

Route103-shaped drop-in candidate provider with the scalar coordinate frontier lowered to nonzero values and nonzero-distinct additivity.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_route106CoordinateClosers_canonical {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B D.tower) : Nonempty (CentralCoverCandidateLiftPartitionData B)

Route106 integrated-route shape, matching the current exact-image-final provider's canonical tower call site.