Candidate Route152 exact-image closers

Route152 still exposes the two broad candidate exact-image leaves through the Route147 pointwise candidate provider:

• centralCover_candidateObstructionMapData;
• centralCover_candidateFrattiniExactImageCardinalityData.

This sidecar keeps the integrated route untouched and supplies a stricter Section 8 replacement. The source-side residual is the coherent manuscript packet centralCover_candidateMiddleFrattiniResidualProofData: a middle R-valued obstruction on the exact-image index X_Gamma(C), together with the matching Frattini exact-image affine-fibre equivalence. From that packet we recover the Route147 pointwise objects and the route-ready lift partition without invoking either broad exact-image leaf.

Broad-leaf bridges from structured data

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

Coherent split of the two broad Route152 exact-image leaves for a fixed finite obstruction index.

The Frattini side is deliberately an actual exact-image equivalence, not only a cardinality equality. Taking its cardinal shadow recovers the broad cardinality packet for the selected obstruction map.

• obstructionMap : CentralCoverCandidateObstructionMapData B T I
• frattiniEquiv : let Odata := I.sourceObstructionData self.obstructionMap; let A := centralCover_candidateCanonicalAffineFiberTorsorData B Odata; CentralCoverCandidateFrattiniExactImageEquivData B T Odata A.Z A.F

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

The paired broad-leaf output for a selected obstruction map.

• obstructionMap : CentralCoverCandidateObstructionMapData B T I
• frattiniCardinality : let Odata := I.sourceObstructionData self.obstructionMap; let A := centralCover_candidateCanonicalAffineFiberTorsorData B Odata; CentralCoverCandidateFrattiniExactImageCardinalityData B T Odata A.Z A.F

@[reducible, inline]

abbrev Q2Presentation.Induction.CentralCoverCandidateRoute152BroadLeafCardinality {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (I : CentralCoverCandidateObstructionIndexBaseData B T) (O : CentralCoverCandidateObstructionMapData B T I) : Prop

The dependent cardinality predicate for a supplied broad obstruction map.

Equations

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

def Q2Presentation.Induction.CentralCoverCandidateRoute152BroadLeafSplitData.frattiniCardinalityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {I : CentralCoverCandidateObstructionIndexBaseData B T} (D : CentralCoverCandidateRoute152BroadLeafSplitData B T I) : have Odata := I.sourceObstructionData D.obstructionMap; have A := centralCover_candidateCanonicalAffineFiberTorsorData B Odata; CentralCoverCandidateFrattiniExactImageCardinalityData B T Odata A.Z A.F

Cardinality shadow of the structured Frattini exact-image equivalence.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.centralCover_candidateRoute152BroadLeaves_from_leafSplit {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (I : CentralCoverCandidateObstructionIndexBaseData B T) (D : CentralCoverCandidateRoute152BroadLeafSplitData B T I) : Nonempty (CentralCoverCandidateRoute152BroadLeafPair B T I)

Bridge from the structured split residual to the paired broad exact-image leaf data for the selected obstruction map.

Route152 coherent middle/Frattini packet

def Q2Presentation.Induction.CentralCoverCandidateMiddleFrattiniResidualProofData.route152ObstructionMapData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleFrattiniResidualProofData B T) (I : CentralCoverCandidateObstructionIndexBaseData B T) : CentralCoverCandidateObstructionMapData B T I

Pull the selected middle R-obstruction back along any finite index-to-middle-source map. This closes the broad obstruction-map packet from the coherent Section 8 residual.

Equations

• D.route152ObstructionMapData I = { obstruction := fun (x : I.X) => D.middleObstruction.obstruction (I.indexToBase x) }

def Q2Presentation.Induction.CentralCoverCandidateMiddleFrattiniResidualProofData.route152CanonicalFrattiniCardinalityData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleFrattiniResidualProofData B T) : CentralCoverCandidateFrattiniExactImageCardinalityData B T D.middleObstruction.obstructionIndexToBaseMapData.O D.middleObstruction.affineFiberTorsorData.Z D.middleObstruction.affineFiberTorsorData.F

Canonical Frattini cardinality shadow carried by the selected exact-image affine-fibre equivalence.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.CentralCoverCandidateMiddleFrattiniResidualProofData.route152PointwiseData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleFrattiniResidualProofData B T) : CentralCoverCandidateRoute147PointwiseData B T

Route147 pointwise scalar/Frattini data rebuilt from the coherent Route152 middle/Frattini residual, rather than from the two broad exact-image leaves.

Equations

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

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

Lift-partition data through the Route147 pointwise shape, with all selected objects sourced from the coherent Route152 middle/Frattini residual.

Equations

• D.route152LiftPartitionData Q = D.route152PointwiseData.liftPartitionData Q

theorem Q2Presentation.Induction.centralCover_candidateObstructionMapData_from_candidateRoute152Closers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (I : CentralCoverCandidateObstructionIndexBaseData B T) : Nonempty (CentralCoverCandidateObstructionMapData B T I)

The broad obstruction-map leaf is derivable from the coherent Route152 middle/Frattini residual.

theorem Q2Presentation.Induction.centralCover_candidateCanonicalFrattiniExactImageCardinalityData_from_candidateRoute152Closers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : ∃ (O : CentralCoverCandidateMiddleRLiftObstructionMapData B T), CentralCoverCandidateFrattiniExactImageCardinalityData B T O.obstructionIndexToBaseMapData.O O.affineFiberTorsorData.Z O.affineFiberTorsorData.F

Manuscript-shaped Frattini replacement for Route152: the selected middle obstruction and the cardinality shadow of its matching Frattini equivalence.

This is intentionally canonical; the arbitrary-I, O broad cardinality leaf is replaced by the exact-image equivalence attached to the selected obstruction.

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

Coherent Route152 pointwise data replacing centralCover_candidateRoute147PointwiseData.

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

Drop-in Route152 candidate lift-partition provider.

The call shape matches centralCover_candidateLiftPartitionData_from_candidateRoute147PointwiseClosers, but the axiom closure uses only the coherent middle/Frattini source packet.

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

Canonical-tower spelling for supervisors integrating against a stored canonical quotient tower.

theorem Q2Presentation.Induction.centralCover_candidateRoute152Audit {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (Q : CentralCoverCandidateQuotientFrameMapData B T) : Nonempty ((_ : CentralCoverCandidateMiddleFrattiniResidualProofData B T) × (_ : CentralCoverCandidateRoute147PointwiseData B T) × CentralCoverCandidateLiftPartitionData B)

Audit surface exposing the coherent residual, the rebuilt pointwise packet, and the route-ready lift partition it determines.