Route145 same-tower target closers

Route144 closes the target decoration-kernel packet through the broad actual same-tower leaves

• TargetKmodRSameTowerActualClosers.centralCover_targetCanonicalLowerQuotientEquivData;
• TargetKmodRSameTowerActualClosers.centralCover_targetKmodRAmbientActionData.

This sidecar keeps the same downstream shape, but routes the target side through the lower Section 8 bridge atoms already isolated in the same-tower target API:

• a concrete lower projection Y -> B.C with kernel K;
• one representative action law for that same projection.

The upgrade from one representative to all representatives is theorem-level, using the closed inner-conjugation result for the realized quotient K/R ~= M.

Bundled lower bridge packet

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

Route145 same-tower bridge data: the concrete quotient projection and the representative action law are tied to the same selected projection.

• lowerProjectionBridgeData : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetLowerProjectionBridgeData B D
• representativeActionBridgeData : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (TargetKmodRSameTowerBridgeClosers.lowerProjectionData_of_bridge B D self.lowerProjectionBridgeData)

def Q2Presentation.Induction.TargetKmodRRoute145SameTowerClosers.canonicalLowerQuotientEquivData_of_route145BridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute145BridgeData B D) : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D

The quotient equivalence Y/K ~= B.C induced by Route145 bridge data.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute145SameTowerClosers.projectedConjugationActionData_of_route145BridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute145BridgeData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (TargetKmodRSameTowerBridgeClosers.lowerProjectionData_of_bridge B D H.lowerProjectionBridgeData)

The projected conjugation action induced by Route145 bridge data.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute145SameTowerClosers.ambientActionData_of_route145BridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute145BridgeData B D) : TargetKmodRSameTowerActualClosers.CentralCoverTargetKmodRAmbientActionData B D (TargetKmodRSameTowerBridgeClosers.lowerProjectionData_of_bridge B D H.lowerProjectionBridgeData)

The actual ambient-action packet, for the projection selected by Route145 bridge data.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.TargetKmodRRoute145SameTowerClosers.centralCover_targetRoute145BridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute145BridgeData B D)

Route145 bridge data assembled from the lower same-tower bridge residuals.

Lowered replacements for the Route144 actual same-tower leaves

theorem Q2Presentation.Induction.TargetKmodRRoute145SameTowerClosers.centralCover_targetCanonicalLowerQuotientEquivData_from_route145SameTower {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D)

Route145 replacement for the actual lower-quotient leaf.

Axiom delta: replaces TargetKmodRSameTowerActualClosers.centralCover_targetCanonicalLowerQuotientEquivData by the lower bridge projection atom TargetKmodRSameTowerBridgeClosers.centralCover_targetLowerProjectionBridgeData.

theorem Q2Presentation.Induction.TargetKmodRRoute145SameTowerClosers.centralCover_targetKmodRAmbientActionData_from_route145SameTower {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : Nonempty (TargetKmodRSameTowerActualClosers.CentralCoverTargetKmodRAmbientActionData B D P)

Route145 replacement for the actual all-ambient action leaf.

Axiom delta: replaces TargetKmodRSameTowerActualClosers.centralCover_targetKmodRAmbientActionData by the lower representative-action bridge atom TargetKmodRSameTowerBridgeClosers.centralCover_targetKmodRRepresentativeActionBridgeData.

Drop-in target providers

def Q2Presentation.Induction.TargetKmodRRoute145SameTowerClosers.quotientActionData_of_route145BridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute145BridgeData B D) : TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D

Route145 quotient-action provider through the lowered same-tower bridge.

Equations

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

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

Route145 replacement for the target K/R quotient-action hook.

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

Drop-in target decoration-kernel provider for Route145.

This has the same theorem shape as TargetKmodRRoute144SameTowerClosers.centralCover_targetDecorationKernelData_from_route144SameTower, but its target-side non-local assumptions are the lower same-tower bridge atoms.

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

Convenience framed-quotient provider downstream of the Route145 target closer.