Route22 actual bridge for the target K/R tower

Route21 reduced the target K/R branch to two packets:

• an actual lower projection Y -> B.C with kernel K;
• representative action data for the selected lower projection.

This sidecar keeps route21 untouched, but supplies route22 replacements from a stricter same-tower interface. The remaining leaves are:

• the canonical same-tower equivalence Y/K ~= B.C;
• a representative action law for the canonical projection induced by that equivalence.

The quotient projection, its surjectivity, and the kernel equality are then plain quotient bookkeeping. The upgrade from representatives to all ambient representatives is still the route21 theorem-level conversion, which uses the already closed inner-conjugation theorem.

Route22 narrower same-tower leaves

axiom Q2Presentation.Induction.TargetKmodRRoute22ActualProofs.centralCover_targetRoute22CanonicalLowerActionEquivData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRSameTowerLowerClosers.CentralCoverTargetCanonicalLowerActionEquivData B D)

Route22 lower leaf: identify the abstract lower action group B.C with the literal lower quotient Y/K. The actual projection Y -> B.C and its kernel are constructed from this by quotient APIs below.

Theorem-level construction of the route21 packets

def Q2Presentation.Induction.TargetKmodRRoute22ActualProofs.canonicalLowerProjectionData_of_route22LowerActionEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerLowerClosers.CentralCoverTargetCanonicalLowerActionEquivData B D) : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetCanonicalLowerProjectionData B D

The canonical projection packet induced by the route22 same-tower equivalence.

Equations

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

axiom Q2Presentation.Induction.TargetKmodRRoute22ActualProofs.centralCover_targetRoute22CanonicalRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerLowerClosers.CentralCoverTargetCanonicalLowerActionEquivData B D) : Nonempty (TargetKmodRSameTowerSemanticClosers.CentralCoverTargetKmodRCanonicalRepresentativeActionData B D (canonicalLowerProjectionData_of_route22LowerActionEquiv B D E))

Route22 action leaf: representatives for the canonical projection induced by Y/K ~= B.C realize the abstract B.C action on M by conjugation on the literal quotient K/R.

def Q2Presentation.Induction.TargetKmodRRoute22ActualProofs.route21LowerProjectionBridgeData_of_route22LowerActionEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerLowerClosers.CentralCoverTargetCanonicalLowerActionEquivData B D) : TargetKmodRRoute21ActualProofs.CentralCoverTargetRoute21LowerProjectionBridgeData B D

Route21 lower projection bridge built from the canonical same-tower equivalence Y/K ~= B.C.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute22ActualProofs.route21RepresentativeActionData_of_route22CanonicalRepresentative {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerLowerClosers.CentralCoverTargetCanonicalLowerActionEquivData B D) (A : TargetKmodRSameTowerSemanticClosers.CentralCoverTargetKmodRCanonicalRepresentativeActionData B D (canonicalLowerProjectionData_of_route22LowerActionEquiv B D E)) : TargetKmodRRoute21ActualProofs.CentralCoverTargetRoute21RepresentativeActionData B D (route21LowerProjectionBridgeData_of_route22LowerActionEquiv B D E)

Route21 representative action data for the route22-induced lower projection.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute22ActualProofs.centralCover_targetRoute21LowerProjectionBridgeData_from_route22 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute21ActualProofs.CentralCoverTargetRoute21LowerProjectionBridgeData B D)

Replacement for route21's lower projection residual, using the narrower route22 lower leaf.

theorem Q2Presentation.Induction.TargetKmodRRoute22ActualProofs.centralCover_targetRoute21RepresentativeActionData_from_route22 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRSameTowerLowerClosers.CentralCoverTargetCanonicalLowerActionEquivData B D) : Nonempty (TargetKmodRRoute21ActualProofs.CentralCoverTargetRoute21RepresentativeActionData B D (route21LowerProjectionBridgeData_of_route22LowerActionEquiv B D E))

Replacement for route21's representative action residual, for the canonical route22 lower projection.

theorem Q2Presentation.Induction.TargetKmodRRoute22ActualProofs.centralCover_targetRoute21ActualBridgeData_from_route22 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute21ActualProofs.CentralCoverTargetRoute21ActualBridgeData B D)

Route22 bridge provenance, closing the route21 target branch for the canonically induced lower projection.

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

Direct route22 quotient-action provider. The all-ambient action law is obtained by route21's existing representative-to-projected conversion, which uses the closed inner-conjugation theorem for K/R.

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

Decoration-kernel provider downstream of the route22 target bridge.