Documentation

Q2Presentation.Induction.TargetKmodRRoute53BridgeProofs

Route53 target K/R selected-section closure for Route52 #

Route52 leaves one coherent literal packet:

This sidecar proves that fixed-literal packet from the earlier Route45 selected-section packet. Route45 asks for a coherent identification of the literal lower child Y/K with B.C and an action law for some selected section. Route53 upgrades that selected section to Route52's theorem-level literalQuotientRepresentative using the already closed same-coset theorem on K/R.

Route52 packet from Route45 selected representatives #

source
def Q2Presentation.Induction.TargetKmodRRoute53BridgeProofs.route52CoherentLiteralActionData_of_route45 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A45 : TargetKmodRRoute45BridgeProofs.CentralCoverTargetRoute45LiteralSelectedActionData B D) :
TargetKmodRRoute52BridgeProofs.CentralCoverTargetRoute52CoherentLiteralActionData B D

Route45's selected-section action packet implies Route52's fixed literal representative packet.

The only extra step is replacing the Route45 selected representative of a literal lower class by Route52/Route37's theorem-level quotient representative. Both map to the same class in Y/K, so their quotient-conjugation actions on K/R agree by the closed inner-conjugation bridge.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Q2Presentation.Induction.TargetKmodRRoute53BridgeProofs.centralCover_targetRoute52CoherentLiteralActionData_from_route53 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
    Nonempty (TargetKmodRRoute52BridgeProofs.CentralCoverTargetRoute52CoherentLiteralActionData B D)

    Route53 replacement for Route52's coherent literal action residual.

    The visible target leaf is now the selected-section Route45 packet, which is weaker than Route52's fixed-literal statement: the fixed representatives are recovered theorem-level from same-coset independence on K/R.

    Route-compatible providers #

    source
    theorem Q2Presentation.Induction.TargetKmodRRoute53BridgeProofs.centralCover_targetKmodRQuotientActionData_from_route53 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
    Nonempty (TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D)

    Route53 quotient-action provider.

    This follows the Route52 reassembly path, but sources the Route52 coherent packet from Route45 selected-section data instead of Route52's axiom.

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

    Route53 decoration-kernel provider, drop-in compatible with Route52's target hook.

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

    Convenience Route53 framed-quotient provider for downstream integration.