Documentation

Q2Presentation.Induction.CandidateRLiftFrattiniClosers

Candidate R-lift obstruction and Frattini partition closers #

This sidecar continues the Section 8 candidate exact-image de-axiomatization without proving a semantically empty aggregate for an arbitrary bare elementary tower.

It keeps the already-refined quotient-frame input centralCover_candidateQuotientFrameMapData_residual, but replaces the two remaining candidate semantic residuals used by the routed final closure:

The reassembly target is only the downstream semantic packet CentralCoverCandidateRLiftSemanticData, and then the coherent CentralCoverCandidateLiftPartitionData needed by the integrated Section 8 route. We deliberately do not reconstruct CentralCoverCandidateConcreteExactImageData, because that stronger aggregate still asks for more arbitrary data than the final route needs.

R-lift obstruction map on the middle exact-image index #

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

Candidate R-lift obstruction map on the canonical middle exact-image index.

The index is theorem-level: centralCover_candidateMiddleExactImageIndexBaseData B T is the finite set of middle boundary-framed exact-image maps (def:Xgamma). The residual content is only the semantic R-valued obstruction evaluation of lem:obstructionseparation on that index.

Instances For
    source
    def Q2Presentation.Induction.CentralCoverCandidateMiddleRLiftObstructionMapData.obstructionMapData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) :
    CentralCoverCandidateObstructionMapData B T (centralCover_candidateMiddleExactImageIndexBaseData B T)

    Repackage the semantic map as the generic obstruction-map packet over the canonical middle exact-image index.

    Equations
    Instances For
      source
      def Q2Presentation.Induction.CentralCoverCandidateMiddleRLiftObstructionMapData.obstructionIndexToBaseMapData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) :
      CentralCoverCandidateObstructionIndexToBaseMapData B T

      Reassemble the obstruction-index-to-base packet. Since the chosen index is the middle exact-image source itself, the forgetful map is the canonical one already stored in centralCover_candidateMiddleExactImageIndexBaseData.

      Equations
      Instances For
        source
        def Q2Presentation.Induction.CentralCoverCandidateMiddleRLiftObstructionMapData.affineFiberTorsorData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleRLiftObstructionMapData B T) :
        CentralCoverCandidateAffineFiberTorsorData B D.obstructionIndexToBaseMapData.O

        The canonical affine-fibre torsor attached to the semantic obstruction map. This is theorem-level once the obstruction datum has been fixed.

        Equations
        Instances For
          source
          axiom Q2Presentation.Induction.centralCover_candidateMiddleRLiftObstructionMapData_residual {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) :
          Nonempty (CentralCoverCandidateMiddleRLiftObstructionMapData B T)

          Replacement residual for centralCover_candidateRLiftObstructionData_residual.

          This names the actual missing datum more narrowly: the R-valued obstruction map on the canonical middle exact-image index.

          Frattini partition over the canonical affine fibres #

          source
          axiom Q2Presentation.Induction.centralCover_candidateFrattiniAffineFiberPartition_residual {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)

          Replacement residual for centralCover_candidateFrattiniCoverData_residual.

          For the chosen semantic obstruction map, the affine fibres are the canonical regular Z^1(R) fibres. The remaining Frattini content of prop:finalfourier is the exact-image partition of top candidate maps by unobstructed fibres, using R = Phi(K) to ensure the final lifts are exact-image/surjective.

          Reassembly for the downstream route #

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

          The refined quotient-frame map packet supplies the exact-image base quotient used in the semantic R-lift packet.

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

          Candidate semantic R-lift data assembled from the refined quotient-frame packet, the middle exact-image obstruction map, and the canonical affine-fibre Frattini partition.

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

          Coherent candidate lift-partition data routed through the sharper R-lift and Frattini packets. This is the packet consumed by CentralCoverIntegratedRefinement.lean.