Candidate Route115 semantic closers

This sidecar targets the two candidate-side semantic residuals visible after Route114:

• centralCover_candidateMiddleScalarObstructionEvaluatorData;
• centralCover_candidateFrattiniAffineFiberCoordinateData.

It does not prove the manuscript's scalar/Fourier and Frattini-coordinate content outright. Instead it gives a strictly smaller theorem-level lowering, using the already-isolated scalar/Frattini semantic packets:

• scalar pushout values on the canonical middle exact-image source;
• linearity of those values in lambda : X_R;
• a Frattini lift-coordinate map;
• a Frattini realization map;
• the two inverse laws tying those maps together.

The route-ready provider below has the same downstream target as the Route113 candidate exact-image provider, but its axiom closure should name the five smaller packets above rather than the two Route114 semantic residual axioms. No theorem below touches any local/CFT axiom.

Selected scalar obstruction and matching Frattini coordinates

def Q2Presentation.Induction.centralCover_candidateRoute115MiddleObstructionOfScalar {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (V : CentralCoverCandidateMiddleScalarPushoutValueData B T) (L : CentralCoverCandidateMiddleScalarPushoutLinearityData V) : CentralCoverCandidateMiddleRLiftObstructionMapData B T

The middle R-valued obstruction map assembled from scalar pushout values and their linearity in lambda : X_R.

Equations

• Q2Presentation.Induction.centralCover_candidateRoute115MiddleObstructionOfScalar V L = { obstruction := (V.evaluatorData L).obstructionEvaluator }

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

Route115 candidate semantic data.

This is the coherent selected packet used by the Route115 integrated provider: the scalar pushout value/linearity data selects a middle obstruction map, and the Frattini coordinate/realization/inverse data is attached to that same selected obstruction map.

• scalarValue : CentralCoverCandidateMiddleScalarPushoutValueData B T
• scalarLinearity : CentralCoverCandidateMiddleScalarPushoutLinearityData self.scalarValue
• frattiniLift : CentralCoverCandidateFrattiniLiftCoordinateData B T (centralCover_candidateRoute115MiddleObstructionOfScalar self.scalarValue self.scalarLinearity)
• frattiniRealization : CentralCoverCandidateFrattiniRealizationData B T (centralCover_candidateRoute115MiddleObstructionOfScalar self.scalarValue self.scalarLinearity)
• frattiniInverse : CentralCoverCandidateFrattiniCoordinateInverseData self.frattiniLift self.frattiniRealization

def Q2Presentation.Induction.CentralCoverCandidateRoute115SemanticData.scalarEvaluatorData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute115SemanticData B T) : CentralCoverCandidateMiddleScalarObstructionEvaluatorData B T

The current scalar-obstruction evaluator packet recovered from the selected scalar pushout values and linearity.

Equations

• D.scalarEvaluatorData = D.scalarValue.evaluatorData D.scalarLinearity

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

The selected middle R-lift obstruction map.

Equations

• D.middleObstruction = Q2Presentation.Induction.centralCover_candidateRoute115MiddleObstructionOfScalar D.scalarValue D.scalarLinearity

def Q2Presentation.Induction.CentralCoverCandidateRoute115SemanticData.frattiniCoordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute115SemanticData B T) : CentralCoverCandidateFrattiniAffineFiberCoordinateData B T D.middleObstruction

The current Frattini affine-fibre coordinate packet recovered from the selected coordinate/realization maps and inverse laws.

Equations

• D.frattiniCoordinateData = D.frattiniLift.coordinateData D.frattiniRealization D.frattiniInverse

def Q2Presentation.Induction.CentralCoverCandidateRoute115SemanticData.frattiniExactImage {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateRoute115SemanticData B T) : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.middleObstruction.obstructionIndexToBaseMapData.O D.middleObstruction.affineFiberTorsorData.Z D.middleObstruction.affineFiberTorsorData.F

The exact-image Frattini partition carried by the Route115 coordinates.

Equations

• D.frattiniExactImage = { partition := { bij := D.frattiniCoordinateData.equiv } }

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

Coherent direct exact-image residual data recovered from the Route115 selected semantic packet.

Equations

• D.directExactImageResidualData = { middleObstruction := D.middleObstruction, frattiniPartition := D.frattiniExactImage }

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

Candidate lift-partition data recovered from the Route115 selected semantic packet and a route-supplied quotient-frame map.

Equations

• D.liftPartitionData Q = D.directExactImageResidualData.liftPartitionData Q

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

The coherent Route115 selected semantic packet from the five smaller scalar/Frattini packets.

Projections replacing the two Route114 semantic residual shapes

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

Route115 theorem-level replacement for centralCover_candidateMiddleScalarObstructionEvaluatorData.

Its closure should name only scalar pushout value data and scalar pushout linearity data.

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

Route115 theorem-level replacement for the selected middle obstruction map used by the integrated candidate provider.

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

Route115 theorem-level replacement for centralCover_candidateFrattiniAffineFiberCoordinateData.

This keeps the original arbitrary-obstruction call shape and reduces it to the three Frattini coordinate/realization/inverse packets.

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

Route115 Frattini exact-image partition for an arbitrary supplied middle obstruction map.

Route-ready reassembly

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

Coherent direct exact-image residual data from the Route115 selected semantic packet.

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

Tower-shaped Route115 candidate lift-partition provider.

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

Drop-in Route115 candidate provider for the integrated route.

The call shape matches the Route113 provider: the target canonical quotient tower supplies D.tower, and the route supplies the quotient-frame map.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_route115SemanticAudit {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B D.tower) : Nonempty ((V : CentralCoverCandidateMiddleScalarPushoutValueData B D.tower) × (_ : CentralCoverCandidateMiddleScalarPushoutLinearityData V) × (O : CentralCoverCandidateMiddleRLiftObstructionMapData B D.tower) × (C : CentralCoverCandidateFrattiniLiftCoordinateData B D.tower O) × (R : CentralCoverCandidateFrattiniRealizationData B D.tower O) × CentralCoverCandidateFrattiniCoordinateInverseData C R × CentralCoverCandidateLiftPartitionData B)

Audit surface for the Route115 candidate provider.

The theorem exposes the five smaller packets and the final route-ready lift partition chosen from them.