Route161 target K/R quotient/action closers

Route160's target branch uses Route157's drop-in decoration-kernel provider, whose target frontier is the five Route151 lower projection/action leaves:

• a selected lower projection map Y -> B.C;
• pointwise fibres of that projection;
• the two kernel inclusions identifying its kernel with K;
• the all-ambient projected action law on K/R.

This sidecar keeps the same downstream Route157-shaped conclusion but replaces those leaves by more concrete Route161 packets:

• a raw projection function and its monoid-hom laws;
• pointwise fibre witnesses split from their proof equations;
• pointwise tests for K-membership and projection-triviality;
• a representative selector, its section law, and representative-level action.

The all-ambient action law is then theorem-level from the existing closed fact that inner conjugation by K is trivial on K/R.

Route161 lower projection/action atoms

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

Route161 raw lower projection function.

This is the function-level content behind the Route151 monoid hom Y -> C = Y/K, with C represented by the abstract action group B.C.

• lowerProjectionFun : p.fst.Y → B.C

structure Q2Presentation.Induction.TargetKmodRRoute161Closers.CentralCoverTargetRoute161LowerProjectionHomData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) : Prop

Route161 monoid laws for the raw lower projection function.

• lowerProjection_one : P.lowerProjectionFun 1 = 1
• lowerProjection_mul (y z : p.fst.Y) : P.lowerProjectionFun (y * z) = P.lowerProjectionFun y * P.lowerProjectionFun z

structure Q2Presentation.Induction.TargetKmodRRoute161Closers.CentralCoverTargetRoute161LowerProjectionPreimageData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) (c : B.C) : Type

Route161 pointwise fibre witness, split from the equation proving that it is a fibre point.

• preimage : p.fst.Y

structure Q2Presentation.Induction.TargetKmodRRoute161Closers.CentralCoverTargetRoute161LowerProjectionPreimageSpecData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) (c : B.C) (F : CentralCoverTargetRoute161LowerProjectionPreimageData B D P c) : Prop

Route161 proof that the selected pointwise witness is a fibre point.

• lowerProjection_preimage : P.lowerProjectionFun F.preimage = c

structure Q2Presentation.Induction.TargetKmodRRoute161Closers.CentralCoverTargetRoute161KsubProjectionTrivialData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) : Prop

Route161 pointwise form of K <= ker(Y -> C).

• ksub_projection_eq_one (y : p.fst.Y) : y ∈ D.Ksub → P.lowerProjectionFun y = 1

structure Q2Presentation.Induction.TargetKmodRRoute161Closers.CentralCoverTargetRoute161ProjectionTrivialLeKsubData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) : Prop

Route161 pointwise form of ker(Y -> C) <= K.

• projection_eq_one_mem_ksub (y : p.fst.Y) : P.lowerProjectionFun y = 1 → y ∈ D.Ksub

structure Q2Presentation.Induction.TargetKmodRRoute161Closers.CentralCoverTargetRoute161RepresentativeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) : Type

Route161 selected representatives of the lower classes.

• quotientRepresentative : B.C → p.fst.Y

structure Q2Presentation.Induction.TargetKmodRRoute161Closers.CentralCoverTargetRoute161RepresentativeSectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) (S : CentralCoverTargetRoute161RepresentativeData B D P) : Prop

Route161 proof that the selected representatives form a section of the lower projection.

• lowerProjection_quotientRepresentative (c : B.C) : P.lowerProjectionFun (S.quotientRepresentative c) = c

structure Q2Presentation.Induction.TargetKmodRRoute161Closers.CentralCoverTargetRoute161RepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) (S : CentralCoverTargetRoute161RepresentativeData B D P) : Prop

Route161 representative-level action law on K/R.

The all-ambient projected action law used by Route151 is recovered from this selected-representative law plus theorem-level inner-conjugation triviality on K/R.

• representative_action_realizes_conjugation (c : B.C) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM c) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D (S.quotientRepresentative c) (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

Route161 residual names

axiom Q2Presentation.Induction.TargetKmodRRoute161Closers.centralCover_targetRoute161LowerProjectionFunctionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute161LowerProjectionFunctionData B D)

Route161 residual: raw lower projection function Y -> C.

axiom Q2Presentation.Induction.TargetKmodRRoute161Closers.centralCover_targetRoute161LowerProjectionHomData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) : Nonempty (CentralCoverTargetRoute161LowerProjectionHomData B D P)

Route161 residual: monoid laws for the raw lower projection function.

axiom Q2Presentation.Induction.TargetKmodRRoute161Closers.centralCover_targetRoute161LowerProjectionPreimageData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) (c : B.C) : Nonempty (CentralCoverTargetRoute161LowerProjectionPreimageData B D P c)

Route161 residual: pointwise preimage witness for the lower projection.

axiom Q2Presentation.Induction.TargetKmodRRoute161Closers.centralCover_targetRoute161LowerProjectionPreimageSpecData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) (c : B.C) (F : CentralCoverTargetRoute161LowerProjectionPreimageData B D P c) : Nonempty (CentralCoverTargetRoute161LowerProjectionPreimageSpecData B D P c F)

Route161 residual: proof that the selected witness maps to the point.

axiom Q2Presentation.Induction.TargetKmodRRoute161Closers.centralCover_targetRoute161KsubProjectionTrivialData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) : Nonempty (CentralCoverTargetRoute161KsubProjectionTrivialData B D P)

Route161 residual: pointwise K <= ker(Y -> C).

axiom Q2Presentation.Induction.TargetKmodRRoute161Closers.centralCover_targetRoute161ProjectionTrivialLeKsubData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) : Nonempty (CentralCoverTargetRoute161ProjectionTrivialLeKsubData B D P)

Route161 residual: pointwise ker(Y -> C) <= K.

axiom Q2Presentation.Induction.TargetKmodRRoute161Closers.centralCover_targetRoute161RepresentativeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) : Nonempty (CentralCoverTargetRoute161RepresentativeData B D P)

Route161 residual: selected representatives of lower classes.

axiom Q2Presentation.Induction.TargetKmodRRoute161Closers.centralCover_targetRoute161RepresentativeSectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) (S : CentralCoverTargetRoute161RepresentativeData B D P) : Nonempty (CentralCoverTargetRoute161RepresentativeSectionData B D P S)

Route161 residual: the selected representatives are a section.

axiom Q2Presentation.Induction.TargetKmodRRoute161Closers.centralCover_targetRoute161RepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) (S : CentralCoverTargetRoute161RepresentativeData B D P) : Nonempty (CentralCoverTargetRoute161RepresentativeActionData B D P S)

Route161 residual: representative-level action on K/R.

Route151-surface adapters

def Q2Presentation.Induction.TargetKmodRRoute161Closers.lowerProjectionMonoidHom_of_route161 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) (H : CentralCoverTargetRoute161LowerProjectionHomData B D P) : p.fst.Y →* B.C

The Route161 raw function and hom laws as a monoid hom.

Equations

• Q2Presentation.Induction.TargetKmodRRoute161Closers.lowerProjectionMonoidHom_of_route161 B D P H = { toFun := P.lowerProjectionFun, map_one' := ⋯, map_mul' := ⋯ }

def Q2Presentation.Induction.TargetKmodRRoute161Closers.route151LowerProjectionMapData_of_route161 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) (H : CentralCoverTargetRoute161LowerProjectionHomData B D P) : TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionMapData B D

Route151 map packet from Route161's raw function and hom laws.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute161Closers.route151LowerProjectionSurjFiberData_of_route161 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) (H : CentralCoverTargetRoute161LowerProjectionHomData B D P) (c : B.C) (F : CentralCoverTargetRoute161LowerProjectionPreimageData B D P c) (S : CentralCoverTargetRoute161LowerProjectionPreimageSpecData B D P c F) : TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionSurjFiberData B D (route151LowerProjectionMapData_of_route161 B D P H) c

Route151 fibre packet from Route161's split witness/spec atoms.

Equations

• Q2Presentation.Induction.TargetKmodRRoute161Closers.route151LowerProjectionSurjFiberData_of_route161 B D P H c F S = { preimage := F.preimage, lowerProjection_preimage := ⋯ }

def Q2Presentation.Induction.TargetKmodRRoute161Closers.route151LowerProjectionKsubLeKerData_of_route161 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) (H : CentralCoverTargetRoute161LowerProjectionHomData B D P) (K : CentralCoverTargetRoute161KsubProjectionTrivialData B D P) : TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionKsubLeKerData B D (route151LowerProjectionMapData_of_route161 B D P H)

Route151 K <= ker packet from Route161's pointwise triviality law.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute161Closers.route151LowerProjectionKerLeKsubData_of_route161 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) (H : CentralCoverTargetRoute161LowerProjectionHomData B D P) (K : CentralCoverTargetRoute161ProjectionTrivialLeKsubData B D P) : TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionKerLeKsubData B D (route151LowerProjectionMapData_of_route161 B D P H)

Route151 ker <= K packet from Route161's pointwise detection law.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute161Closers.lowerProjectionData_of_route161Pieces {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) (H : CentralCoverTargetRoute161LowerProjectionHomData B D P) (Kle : CentralCoverTargetRoute161KsubProjectionTrivialData B D P) (Kge : CentralCoverTargetRoute161ProjectionTrivialLeKsubData B D P) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

Transport-final projection packet from the Route161 lower projection pieces.

Equations

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

Route161 projected-action and decoration-kernel bridge

def Q2Presentation.Induction.TargetKmodRRoute161Closers.representativeActionBridgeData_of_route161 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) (H : CentralCoverTargetRoute161LowerProjectionHomData B D P) (Kle : CentralCoverTargetRoute161KsubProjectionTrivialData B D P) (Kge : CentralCoverTargetRoute161ProjectionTrivialLeKsubData B D P) (Srep : CentralCoverTargetRoute161RepresentativeData B D P) (Ssec : CentralCoverTargetRoute161RepresentativeSectionData B D P Srep) (A : CentralCoverTargetRoute161RepresentativeActionData B D P Srep) : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (lowerProjectionData_of_route161Pieces B D P H Kle Kge)

Route161 representative bridge over the transport-final projection.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute161Closers.route151ProjectedRepresentativeActionData_of_route161 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute161LowerProjectionFunctionData B D) (H : CentralCoverTargetRoute161LowerProjectionHomData B D P) (Kle : CentralCoverTargetRoute161KsubProjectionTrivialData B D P) (Kge : CentralCoverTargetRoute161ProjectionTrivialLeKsubData B D P) (Srep : CentralCoverTargetRoute161RepresentativeData B D P) (Ssec : CentralCoverTargetRoute161RepresentativeSectionData B D P Srep) (A : CentralCoverTargetRoute161RepresentativeActionData B D P Srep) : TargetKmodRRoute151Closers.CentralCoverTargetRoute151ProjectedRepresentativeActionData B D (route151LowerProjectionMapData_of_route161 B D P H)

Route151 projected-action packet from Route161 representative action plus the theorem-level inner-conjugation closure on K/R.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.TargetKmodRRoute161Closers.centralCover_targetKmodRProjectedConjugationActionData_from_route161Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty ((P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) ×' TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P)

Route161 projected-action provider in the transport-final surface.

theorem Q2Presentation.Induction.TargetKmodRRoute161Closers.centralCover_targetKmodRQuotientActionData_from_route161Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D)

Route161 quotient-action provider.

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

Route161 drop-in target decoration-kernel provider.

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

Name mirroring the Route157 call site for a one-line replacement.

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

Convenience framed-quotient provider through Route161.