Candidate canonical concrete proofs

This sidecar narrows the candidate Section 8 final-closure packet centralCover_candidateCanonicalConcreteProofData.

The manuscript shape is the canonical exact-image tower Y -> B = Y/R -> C = Y/K. The theorem below derives the current aggregate canonical candidate packet from the three smaller component packets already isolated in the tree:

• the actual quotient-frame postcomposition map;
• the middle R-lift obstruction on the canonical exact-image source;
• the Frattini exact-image affine-fibre equivalence for that same obstruction.

No routed file is edited here. The last theorem gives the final count route with the same extraspecial determinant refinement as the current route, but with the candidate call replaced by the narrowed canonical concrete theorem.

Candidate canonical packet narrowed to component packets

theorem Q2Presentation.Induction.centralCover_candidateCanonicalConcreteProofData_proven {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) : Nonempty (CentralCoverCandidateCanonicalConcreteProofData B D)

The canonical candidate concrete packet, proved from the smaller component packets rather than from the aggregate axiom centralCover_candidateCanonicalConcreteProofData.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_from_candidateCanonicalConcreteProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetCanonicalQuotientTowerData B) : Nonempty (CentralCoverCandidateLiftPartitionData B)

Coherent candidate lift-partition data obtained through the narrowed canonical concrete packet.

Current final route with only the candidate packet swapped

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerCandidateCanonicalConcreteProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) (h : ¬ScalarTerminal p) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData G.preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) : Nonempty (CoverRealization (G.toMinimalBlock h Fdet A Rdet))

Cover realization for the current target-framed marked-quotient route, with the candidate side routed through centralCover_candidateCanonicalConcreteProofData_proven instead of the aggregate canonical candidate residual.

theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_targetFramedMarkedQuotientExtraspecialDeterminantCandidateCanonicalProofs (p : FramedPair) : ¬ScalarTerminal p → Nonempty (FourierBranchData p)

Nonterminal Fourier branch for the current extraspecial determinant route, with the candidate canonical concrete packet narrowed to component packets.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_targetFramedMarkedQuotientExtraspecialDeterminantCandidateCanonicalProofs (p : FramedPair) (h : ¬ScalarTerminal p) : ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_targetFramedMarkedQuotientExtraspecialDeterminantCandidateCanonicalProofs (p : FramedPair) : framedCountA p = framedCountQ p ∨ ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

theorem Q2Presentation.Induction.boundaryFramed_counts_equal_targetFramedMarkedQuotientExtraspecialDeterminantCandidateCanonicalProofs (p : FramedPair) : framedCountA p = framedCountQ p

theorem Q2Presentation.Induction.finite_surjection_counts_equal_targetFramedMarkedQuotientExtraspecialDeterminantCandidateCanonicalProofs (G : Type) [Group G] [Finite G] [Nonempty G] : Cardinal.mk (Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.mk (Profinite.SurjContHom GQ2Profinite (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)))

Current final finite-surjection theorem with the candidate canonical concrete packet narrowed to the smaller Section 8 component packets.