Canonical framed quotient target constructor

This sidecar refines the remaining Section 8 target packet centralCover_targetCanonicalFramedQuotientData.

The existing subgroup packet already gives the canonical normal subgroups R <= K <= L_Y, so the tame quotient map piY factors through both quotients Y/R and Y/K. The missing semantic input is the manuscript decoration-block fact (lem:decorationblock): the boundary decoration thetaY vanishes on K. Once that is supplied, the framed quotient targets are canonical, not arbitrary children:

• middle child: Y/R, with marked kernel the image of L_Y;
• lower child: Y/K, with marked kernel the image of L_Y;
• frame: the same (alpha, psi, beta), since H and E are unchanged.

The strictly smaller semantic packet

structure Q2Presentation.Induction.CentralCoverTargetDecorationKernelData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Prop

Decoration-block compatibility for the target tower.

This is the framed part of manuscript lem:decorationblock needed to quotient the boundary-framed target: the elementary decoration thetaY kills the block subgroup K. Since R <= K, this also makes thetaY factor through Y/R.

• Ksub_le_thetaY_ker : D.Ksub ≤ p.fst.thetaY.ker

axiom Q2Presentation.Induction.centralCover_targetDecorationKernelData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetDecorationKernelData B D)

Smaller residual replacing the broad framed quotient-target constructor.

This is intentionally narrower than centralCover_targetCanonicalFramedQuotientData: it asks only for the decoration-block compatibility needed for the explicit quotient construction below.

Quotient-factorization facts

theorem Q2Presentation.Induction.TargetCanonicalFramedQuotientProofs.Rsub_le_piY_ker {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : D.Rsub ≤ p.fst.piY.ker

theorem Q2Presentation.Induction.TargetCanonicalFramedQuotientProofs.Ksub_le_piY_ker {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : D.Ksub ≤ p.fst.piY.ker

theorem Q2Presentation.Induction.TargetCanonicalFramedQuotientProofs.Rsub_le_thetaY_ker {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetDecorationKernelData B D) : D.Rsub ≤ p.fst.thetaY.ker

The two canonical quotient framed targets

def Q2Presentation.Induction.TargetCanonicalFramedQuotientProofs.middleTarget {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetDecorationKernelData B D) : BoundaryFramedTarget

The middle framed target Y/R, with inherited marked kernel and decoration.

Equations

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

def Q2Presentation.Induction.TargetCanonicalFramedQuotientProofs.lowerTarget {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetDecorationKernelData B D) : BoundaryFramedTarget

The lower framed target Y/K, with inherited marked kernel and decoration.

Equations

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

def Q2Presentation.Induction.TargetCanonicalFramedQuotientProofs.middleFrame {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetDecorationKernelData B D) : BoundaryFrame (middleTarget B D H)

The middle quotient inherits the original boundary frame because H and E are preserved definitionally.

Equations

• Q2Presentation.Induction.TargetCanonicalFramedQuotientProofs.middleFrame B D H = { alpha := p.snd.alpha, alpha_surj := ⋯, psi := p.snd.psi, beta := p.snd.beta, beta_def := ⋯ }

def Q2Presentation.Induction.TargetCanonicalFramedQuotientProofs.lowerFrame {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetDecorationKernelData B D) : BoundaryFrame (lowerTarget B D H)

The lower quotient inherits the original boundary frame because H and E are preserved definitionally.

Equations

• Q2Presentation.Induction.TargetCanonicalFramedQuotientProofs.lowerFrame B D H = { alpha := p.snd.alpha, alpha_surj := ⋯, psi := p.snd.psi, beta := p.snd.beta, beta_def := ⋯ }

def Q2Presentation.Induction.TargetCanonicalFramedQuotientProofs.middleChild {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetDecorationKernelData B D) : FramedPair

Equations

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

def Q2Presentation.Induction.TargetCanonicalFramedQuotientProofs.lowerChild {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetDecorationKernelData B D) : FramedPair

Equations

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

Reassembly of the current canonical framed quotient packet

def Q2Presentation.Induction.TargetCanonicalFramedQuotientProofs.framedQuotientDataOfDecorationKernel {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetDecorationKernelData B D) : CentralCoverTargetCanonicalFramedQuotientData B D

Build the current broad framed quotient packet from the single decoration-block compatibility field.

Equations

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

theorem Q2Presentation.Induction.TargetCanonicalFramedQuotientProofs.centralCover_targetCanonicalFramedQuotientData_of_decorationKernel {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : CentralCoverTargetDecorationKernelData B D → Nonempty (CentralCoverTargetCanonicalFramedQuotientData B D)

theorem Q2Presentation.Induction.centralCover_targetCanonicalFramedQuotientData_proven {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetCanonicalFramedQuotientData B D)

Route-ready refinement of the current final-closure packet.

Its axiom closure replaces the old broad residual centralCover_targetCanonicalFramedQuotientData by the narrower manuscript field centralCover_targetDecorationKernelData, and constructs both quotient children canonically as Y/R and Y/K.