Candidate Route146 pointwise coordinate closers

Route145 lowers the candidate Section 8 frontier to seven scalar/Frattini coordinate atoms. This sidecar keeps the Route145 downstream shape, but replaces those whole-function and global-law residuals by pointwise atoms:

• nonzero scalar-pushout values are supplied one middle exact-image point at a time;
• nonzero-distinct additivity is supplied one (x, lambda, mu) test at a time;
• Frattini base/fibre coordinates and fibre realization are supplied pointwise;
• both inverse laws are supplied pointwise.

The old Route145 theorem is untouched. The final provider below has the same B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B) shape, so it can be used as a drop-in candidate replacement in an integrated Route146 file.

Pointwise scalar-pushout values

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

Pointwise value of a nonzero scalar pushout at one middle exact-image map.

• value : ZMod 2

axiom Q2Presentation.Induction.centralCover_candidateMiddleScalarPushoutNonzeroValueAtPointData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (lam : ↥B.XR) (h : lam ≠ 0) (x : centralCoverCandidateMiddleSource T) : Nonempty (CentralCoverCandidateMiddleScalarPushoutNonzeroValueAtPointData B T lam x)

Route146 candidate residual: pointwise nonzero scalar-pushout value.

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

Assemble the Route145 nonzero value packet from pointwise Route146 values.

Equations

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

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

Route146 replacement for the Route145 nonzero scalar value leaf.

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

Route146 scalar-pushout family: zero is theorem-level, nonzero values are assembled from pointwise residuals.

Equations

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

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

The selected Route146 family is still definitionally zero at the zero scalar.

Pointwise nonzero-distinct additivity

structure Q2Presentation.Induction.CentralCoverCandidateMiddleScalarPushoutNonzeroDistinctAdditivityAtData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (V : CentralCoverCandidateMiddleScalarPushoutFamilyData B T) (x : centralCoverCandidateMiddleSource T) (lam mu : ↥B.XR) (hlam : lam ≠ 0) (hmu : mu ≠ 0) (hdiff : lam ≠ mu) : Type

One nonzero-distinct scalar additivity equality.

• map_add_at : (V.valueAt (lam + mu)).valueAt x = (V.valueAt lam).valueAt x + (V.valueAt mu).valueAt x

axiom Q2Presentation.Induction.centralCover_candidateMiddleScalarPushoutNonzeroDistinctAdditivityAtData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (V : CentralCoverCandidateMiddleScalarPushoutFamilyData B T) (x : centralCoverCandidateMiddleSource T) (lam mu : ↥B.XR) (hlam : lam ≠ 0) (hmu : mu ≠ 0) (hdiff : lam ≠ mu) : Nonempty (CentralCoverCandidateMiddleScalarPushoutNonzeroDistinctAdditivityAtData V x lam mu hlam hmu hdiff)

Route146 candidate residual: pointwise nonzero-distinct additivity.

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

Assemble the Route145 nonzero-distinct additivity packet from pointwise Route146 equalities.

Equations

• Q2Presentation.Induction.centralCover_candidateMiddleScalarPushoutNonzeroDistinctAdditivityData_of_route146Points V = { map_add_nonzero_distinct := ⋯ }

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

Route146 replacement for the Route145 nonzero-distinct scalar additivity leaf.

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

Route146 scalar packet: selected scalar family, theorem-level zero case, and pointwise nonzero-distinct additivity.

Pointwise Frattini base and fibre coordinates

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

Pointwise base exact-image coordinate.

• baseCoordinateAt : CentralCoverCandidateFrattiniBaseTarget B T D

axiom Q2Presentation.Induction.centralCover_candidateFrattiniBaseCoordinateAtData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) (f : centralCoverCandidateSource) : Nonempty (CentralCoverCandidateFrattiniBaseCoordinateAtData B T D f)

Route146 candidate residual: pointwise Frattini base coordinate.

def Q2Presentation.Induction.centralCover_candidateFrattiniBaseCoordinateData_of_route146Points {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : CentralCoverCandidateFrattiniBaseCoordinateData B T D

Assemble the old base-coordinate packet from pointwise Route146 base coordinates.

Equations

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

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

Route146 replacement for the Route145 base-coordinate leaf.

structure Q2Presentation.Induction.CentralCoverCandidateFrattiniFiberCoordinateAtData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) (f : centralCoverCandidateSource) : Type

Pointwise affine fibre coordinate over the selected base coordinate.

• fiberCoordinateAt : D.affineFiberTorsorData.F.Lift (C.baseCoordinate f)

axiom Q2Presentation.Induction.centralCover_candidateFrattiniFiberCoordinateAtData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) (f : centralCoverCandidateSource) : Nonempty (CentralCoverCandidateFrattiniFiberCoordinateAtData C f)

Route146 candidate residual: pointwise Frattini fibre coordinate.

def Q2Presentation.Induction.centralCover_candidateFrattiniFiberCoordinateData_of_route146Points {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) : CentralCoverCandidateFrattiniFiberCoordinateData C

Assemble the old fibre-coordinate packet from pointwise Route146 fibre coordinates.

Equations

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

theorem Q2Presentation.Induction.centralCover_candidateFrattiniFiberCoordinateData_from_route146 {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) : Nonempty (CentralCoverCandidateFrattiniFiberCoordinateData C)

Route146 replacement for the Route145 fibre-coordinate leaf.

Pointwise Frattini realization and inverse laws

structure Q2Presentation.Induction.CentralCoverCandidateFrattiniFiberRealizationAtData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) (x : CentralCoverCandidateFrattiniBaseTarget B T D) (y : D.affineFiberTorsorData.F.Lift x) : Type

Pointwise realization of one affine fibre coordinate.

• realizeFiberAt : centralCoverCandidateSource

axiom Q2Presentation.Induction.centralCover_candidateFrattiniFiberRealizationAtData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) (x : CentralCoverCandidateFrattiniBaseTarget B T D) (y : D.affineFiberTorsorData.F.Lift x) : Nonempty (CentralCoverCandidateFrattiniFiberRealizationAtData B T D x y)

Route146 candidate residual: pointwise Frattini fibre realization.

def Q2Presentation.Induction.centralCover_candidateFrattiniFiberRealizationData_of_route146Points {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) : CentralCoverCandidateFrattiniFiberRealizationData B T D

Assemble the old curried fibre-realization packet from pointwise Route146 realisations.

Equations

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

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

Route146 replacement for the Route145 fibre-realization leaf.

structure Q2Presentation.Induction.CentralCoverCandidateFrattiniRealizeLiftCoordinateAtData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) (F : CentralCoverCandidateFrattiniFiberCoordinateData C) (R : CentralCoverCandidateFrattiniFiberRealizationData B T D) (f : centralCoverCandidateSource) : Type

One pointwise realization-after-coordinate inverse equality.

• realize_liftCoordinate_at : R.realizeFiber (C.baseCoordinate f) (F.fiberCoordinate f) = f

axiom Q2Presentation.Induction.centralCover_candidateFrattiniRealizeLiftCoordinateAtData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) (F : CentralCoverCandidateFrattiniFiberCoordinateData C) (R : CentralCoverCandidateFrattiniFiberRealizationData B T D) (f : centralCoverCandidateSource) : Nonempty (CentralCoverCandidateFrattiniRealizeLiftCoordinateAtData C F R f)

Route146 candidate residual: pointwise realization-after-coordinate law.

def Q2Presentation.Induction.centralCover_candidateFrattiniRealizeLiftCoordinateData_of_route146Points {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) (F : CentralCoverCandidateFrattiniFiberCoordinateData C) (R : CentralCoverCandidateFrattiniFiberRealizationData B T D) : CentralCoverCandidateFrattiniRealizeLiftCoordinateData C F R

Assemble the Route145 realization-after-coordinate law from pointwise Route146 equalities.

Equations

• Q2Presentation.Induction.centralCover_candidateFrattiniRealizeLiftCoordinateData_of_route146Points C F R = { realize_liftCoordinate := ⋯ }

theorem Q2Presentation.Induction.centralCover_candidateFrattiniRealizeLiftCoordinateData_from_route146 {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) (F : CentralCoverCandidateFrattiniFiberCoordinateData C) (R : CentralCoverCandidateFrattiniFiberRealizationData B T D) : Nonempty (CentralCoverCandidateFrattiniRealizeLiftCoordinateData C F R)

Route146 replacement for the Route145 realization-after-coordinate leaf.

structure Q2Presentation.Induction.CentralCoverCandidateFrattiniLiftCoordinateRealizeAtData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) (F : CentralCoverCandidateFrattiniFiberCoordinateData C) (R : CentralCoverCandidateFrattiniFiberRealizationData B T D) (y : CentralCoverCandidateFrattiniAffineFiberTarget B T D) : Type

One pointwise coordinate-after-realization inverse equality.

• liftCoordinate_realize_at : ⟨C.baseCoordinate (R.realizeFiber y.fst y.snd), F.fiberCoordinate (R.realizeFiber y.fst y.snd)⟩ = y

axiom Q2Presentation.Induction.centralCover_candidateFrattiniLiftCoordinateRealizeAtData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) (F : CentralCoverCandidateFrattiniFiberCoordinateData C) (R : CentralCoverCandidateFrattiniFiberRealizationData B T D) (y : CentralCoverCandidateFrattiniAffineFiberTarget B T D) : Nonempty (CentralCoverCandidateFrattiniLiftCoordinateRealizeAtData C F R y)

Route146 candidate residual: pointwise coordinate-after-realization law.

def Q2Presentation.Induction.centralCover_candidateFrattiniLiftCoordinateRealizeData_of_route146Points {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) (F : CentralCoverCandidateFrattiniFiberCoordinateData C) (R : CentralCoverCandidateFrattiniFiberRealizationData B T D) : CentralCoverCandidateFrattiniLiftCoordinateRealizeData C F R

Assemble the Route145 coordinate-after-realization law from pointwise Route146 equalities.

Equations

• Q2Presentation.Induction.centralCover_candidateFrattiniLiftCoordinateRealizeData_of_route146Points C F R = { liftCoordinate_realize := ⋯ }

theorem Q2Presentation.Induction.centralCover_candidateFrattiniLiftCoordinateRealizeData_from_route146 {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (C : CentralCoverCandidateFrattiniBaseCoordinateData B T D) (F : CentralCoverCandidateFrattiniFiberCoordinateData C) (R : CentralCoverCandidateFrattiniFiberRealizationData B T D) : Nonempty (CentralCoverCandidateFrattiniLiftCoordinateRealizeData C F R)

Route146 replacement for the Route145 coordinate-after-realization leaf.

Route146 candidate reassembly

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

Route146 Frattini coordinate system from pointwise base/fibre/realization and pointwise inverse laws.

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

Coherent Route146 selected scalar/Frattini packet.

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

Direct exact-image residual data through the pointwise Route146 coordinate lowering.

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

Drop-in Route146 candidate lift-partition provider.

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

Canonical-tower spelling for integrated routes that keep Dcan in scope.