Documentation

Q2Presentation.Induction.CandidateScalarFrattiniCurrentProofs

Current candidate scalar/Frattini proof refinement #

This sidecar refines the five route8 candidate scalar/Frattini residuals without editing the routed files.

The current scalar API asks for a value packet and then asks for linearity for an arbitrary chosen value packet. The manuscript construction only needs one coherent scalar-pushout evaluator. The current Frattini API similarly asks for coordinate maps, realization maps, and inverse laws separately; the route only needs one coherent coordinate/realization equivalence.

The replacement residuals below record exactly those coherent choices and then reassemble the same route-ready lift-partition theorem shape consumed by the integrated routes.

Coherent scalar-pushout evaluator #

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

Coherent scalar-pushout evaluator data.

This is weaker than the current pair of residuals centralCover_candidateMiddleScalarPushoutValueData and centralCover_candidateMiddleScalarPushoutLinearityData: it asks for one chosen scalar value packet together with linearity for that same chosen packet, not linearity for every possible value packet.

Instances For
    source
    def Q2Presentation.Induction.CentralCoverCandidateMiddleScalarPushoutCoherentData.evaluatorData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateMiddleScalarPushoutCoherentData B T) :
    CentralCoverCandidateMiddleScalarObstructionEvaluatorData B T

    Reassemble the current scalar obstruction evaluator from a coherent chosen scalar-pushout evaluator.

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

      Remaining coherent scalar-pushout evaluator packet.

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

      Current scalar-obstruction evaluator reassembled from the coherent scalar packet, avoiding the over-strong arbitrary-family linearity residual.

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

      Middle R-lift obstruction map from the coherent scalar-pushout evaluator.

      Coherent Frattini coordinate equivalence #

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

      Coherent Frattini coordinate/realization data.

      This replaces the three current Frattini residuals by the actual route-needed existential: one coordinate map, one realization map, and inverse laws for that same pair. It does not assert inverse laws for arbitrary unrelated maps.

      Instances For
        source
        def Q2Presentation.Induction.CentralCoverCandidateFrattiniCoordinateCoherentData.coordinateData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {D : CentralCoverCandidateMiddleRLiftObstructionMapData B T} (E : CentralCoverCandidateFrattiniCoordinateCoherentData B T D) :
        CentralCoverCandidateFrattiniAffineFiberCoordinateData B T D

        Reassemble the current affine-fibre coordinate packet from coherent coordinate/realization data.

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

          Remaining coherent Frattini coordinate/realization packet.

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

          Current Frattini affine-fibre coordinate data from the coherent Frattini coordinate packet.

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

          Frattini exact-image partition from the coherent coordinate equivalence.

          Route-ready reassembly #

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

          Coherent direct exact-image residual data from the two refined current packets in this sidecar.

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

          Route-ready replacement for the current P2 candidate lift-partition provider.

          This has the same target shape as centralCover_candidateLiftPartitionData_from_scalarFrattiniActualProofs, but its axiom closure contains the two coherent residuals introduced in this file rather than the five current scalar/Frattini packet names.