Documentation

Q2Presentation.Induction.CandidateScalarFrattiniRoute48Proofs

Candidate scalar/Frattini route48 proofs #

Route48 is a candidate Section 8 sidecar for the current Route47 integration point. It first closes the exact Route46 coherent leaf from the sharper middle/Frattini component packet. The active integrated route consumes only the candidate lift-partition provider

B T Q -> Nonempty (CentralCoverCandidateLiftPartitionData B)

Route46 supplies that shape through the stronger scalar/Frattini coherent leaf

The scalar-pushout evaluator is recovered theorem-level from the selected R-obstruction map by evaluation against lambda : X_R; the Frattini coordinate data is recovered theorem-level from the exact-image equivalence. Thus both the exact Route46 leaf and the drop-in Route48 provider have closure the single coherent component packet

This keeps the final candidate closure at one residual, but moves the remaining obligation closer to the manuscript's Section 8 exact-image recursion.

Route48 coherent middle/Frattini packet #

source
theorem Q2Presentation.Induction.centralCover_candidateRoute48MiddleFrattiniCoherentData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) :
Nonempty (CentralCoverCandidateMiddleFrattiniResidualProofData B T)

Route48's single candidate obligation.

This is the smallest coherent object needed by the integrated central-cover route: one actual middle R-valued obstruction map, together with the Frattini exact-image equivalence for the affine fibres attached to that same map.

Exact Route46 leaf closure #

source
theorem Q2Presentation.Induction.centralCover_candidateScalarFrattiniRoute46CoherentData_from_route48 {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) :
Nonempty (CentralCoverCandidateScalarFrattiniRoute46CoherentData B T)

Route48 closes the exact Route46 coherent scalar/Frattini leaf.

The scalar side is recovered from the selected R-obstruction map by evaluating it at invariant scalar pushouts. The Frattini side is recovered from the matching exact-image equivalence carried by the same coherent middle/Frattini packet.

Drop-in provider for the integrated route #

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

Drop-in Route48 candidate lift-partition provider.

This has the same public target shape as centralCover_candidateLiftPartitionData_from_scalarFrattiniRoute46, while using the Route48 proof of the exact Route46 coherent leaf.