Target decoration-kernel proof packet

This sidecar narrows the remaining target-side decoration residual centralCover_targetDecorationKernelData.

Manuscript anchor: §8, lem:decorationblock. The decoration kills R = Phi(K), descends to a C-invariant linear map on the elementary block M = K/R, and then vanishes because (M^vee)^C = 0.

The current subgroup packet knows K/R ≃ M, but it does not expose the conjugation/action compatibility needed to construct the descended decoration map from thetaY. The residual below is exactly that missing compatibility: it supplies the descended block map, proves it is C-invariant, and records its agreement with the original decoration on K.

The narrowed manuscript packet

def Q2Presentation.Induction.TargetDecorationKernelProofs.kmodRPoint {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (k : ↥D.Ksub) : ↥(Subgroup.map (QuotientGroup.mk' D.Rsub) D.Ksub)

The image in K/R of an element of the realized subgroup K.

Equations

• Q2Presentation.Induction.TargetDecorationKernelProofs.kmodRPoint B D k = ⟨(QuotientGroup.mk' D.Rsub) ↑k, ⋯⟩

def Q2Presentation.Induction.TargetDecorationKernelProofs.kmodRVector {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (k : ↥D.Ksub) : B.M

The corresponding vector in the abstract elementary block M.

Equations

• Q2Presentation.Induction.TargetDecorationKernelProofs.kmodRVector B D k = Multiplicative.toAdd (D.KmodR_equivM (Q2Presentation.Induction.TargetDecorationKernelProofs.kmodRPoint B D k))

structure Q2Presentation.Induction.TargetDecorationKernelProofs.CentralCoverTargetDecorationBlockMapData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Type

Narrow decoration-block compatibility packet.

This is the Lean form of the manuscript proof of lem:decorationblock, before the final vanishing step:

• the decoration descends from K to a linear map on M = K/R;
• that map is invariant under the lower quotient action;
• the descended map agrees with thetaY on elements of K.

• blockMap : B.M →ₗ[ZMod 2] p.fst.E
• blockMap_invariant (c : B.C) : self.blockMap ∘ₗ ↑(B.actM c) = self.blockMap
• thetaY_eq_on_Ksub (k : ↥D.Ksub) : p.fst.thetaY ↑k = Multiplicative.ofAdd (self.blockMap (kmodRVector B D k))

The vanishing step from (M^vee)^C = 0

theorem Q2Presentation.Induction.TargetDecorationKernelProofs.invariant_blockMap_eq_zero {p : FramedPair} (B : MinimalBlock p) (f : B.M →ₗ[ZMod 2] p.fst.E) (hf : ∀ (c : B.C), f ∘ₗ ↑(B.actM c) = f) : f = 0

Any C-invariant linear map from the block module M to the elementary decoration module is zero.

This is the formal content of the last sentence of manuscript lem:decorationblock: a nonzero value in E is detected by a linear functional E -> F_2, contradicting (M^vee)^C = 0.

def Q2Presentation.Induction.TargetDecorationKernelProofs.decorationKernelData_of_blockMap {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetDecorationBlockMapData B D) : CentralCoverTargetDecorationKernelData B D

The narrowed block-map packet implies that the decoration kills K.

Equations

• ⋯ = ⋯

axiom Q2Presentation.Induction.centralCover_targetDecorationBlockMapData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetDecorationKernelProofs.CentralCoverTargetDecorationBlockMapData B D)

Narrow residual replacing centralCover_targetDecorationKernelData.

It asks for the descended invariant decoration block map and its agreement with thetaY, rather than directly asking for D.Ksub <= thetaY.ker.

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

Route-ready proof of the current final decoration-kernel packet from the narrowed manuscript block-map packet.

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

The broad canonical framed quotient packet follows without using the old direct decoration-kernel axiom.