Route146 same-tower target bridge closers

Route145's target side leaves two same-tower bridge residuals:

• TargetKmodRSameTowerBridgeClosers.centralCover_targetLowerProjectionBridgeData;
• TargetKmodRSameTowerBridgeClosers.centralCover_targetKmodRRepresentativeActionBridgeData.

This sidecar keeps the same downstream decoration-kernel shape as TargetKmodRRoute145SameTowerClosers.centralCover_targetDecorationKernelData_from_route145SameTower, but replaces those bridge residuals by lower quotient/action atoms:

• the manuscript lower target is the literal quotient C = Y/K, identified with the abstract action group B.C;
• the B.C action is checked on theorem-level representatives of literal Y/K classes.

The projection Y -> B.C, its kernel, representatives over B.C, and the extension to the Route145 bridge-data surface are theorem-level quotient bookkeeping. This is a strict lowering, not a full target closure.

Route146 quotient/action atoms

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

Route146 lower quotient atom.

Manuscript anchor: in the tower retained for the central-cover recursion, the lower target is the literal quotient C = Y/K. The current Lean MinimalBlock interface stores the action group as the abstract finite group B.C, so the remaining semantic content is this quotient identification.

• lowerActionEquiv : p.fst.Y ⧸ D.Ksub ≃* B.C

def Q2Presentation.Induction.TargetKmodRRoute146BridgeClosers.literalQuotientRepresentative {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (q : p.fst.Y ⧸ D.Ksub) : p.fst.Y

The theorem-level representative of a literal quotient class in Y/K.

Equations

• Q2Presentation.Induction.TargetKmodRRoute146BridgeClosers.literalQuotientRepresentative B D q = Classical.choose ⋯

theorem Q2Presentation.Induction.TargetKmodRRoute146BridgeClosers.literalQuotientRepresentative_spec {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (q : p.fst.Y ⧸ D.Ksub) : (QuotientGroup.mk' D.Ksub) (literalQuotientRepresentative B D q) = q

The chosen literal representative maps to its quotient class.

structure Q2Presentation.Induction.TargetKmodRRoute146BridgeClosers.CentralCoverTargetRoute146LiteralRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute146LowerQuotientEquivData B D) : Prop

Route146 literal representative action atom.

This is the action-side manuscript atom: after the lower quotient identification Y/K ~= B.C, the selected representative of each literal lower class realizes the abstract B.C action on M = K/R by conjugation on the literal quotient.

• literal_representative_action_realizes_conjugation (q : p.fst.Y ⧸ D.Ksub) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM (E.lowerActionEquiv q)) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D (literalQuotientRepresentative B D q) (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

axiom Q2Presentation.Induction.TargetKmodRRoute146BridgeClosers.centralCover_targetRoute146LowerQuotientEquivData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute146LowerQuotientEquivData B D)

Route146 lower residual: identify the literal lower quotient Y/K with the abstract action group B.C.

axiom Q2Presentation.Induction.TargetKmodRRoute146BridgeClosers.centralCover_targetRoute146LiteralRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute146LowerQuotientEquivData B D) : Nonempty (CentralCoverTargetRoute146LiteralRepresentativeActionData B D E)

Route146 action residual: prove the representative action law for the theorem-level representatives of literal Y/K classes.

Reassembly of the Route145 bridge surface

def Q2Presentation.Induction.TargetKmodRRoute146BridgeClosers.lowerProjectionBridgeData_of_route146LowerQuotientEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute146LowerQuotientEquivData B D) : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetLowerProjectionBridgeData B D

The Route146 quotient identification induces Route145's lower projection bridge Y -> B.C with kernel K.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute146BridgeClosers.representativeActionBridgeData_of_route146Literal {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute146LowerQuotientEquivData B D) (A : CentralCoverTargetRoute146LiteralRepresentativeActionData B D E) : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (TargetKmodRSameTowerBridgeClosers.lowerProjectionData_of_bridge B D (lowerProjectionBridgeData_of_route146LowerQuotientEquiv B D E))

The Route146 literal representative action atom gives Route145's representative bridge for the projection induced by the same lower quotient identification.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute146BridgeClosers.centralCover_targetLowerProjectionBridgeData_from_route146 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRSameTowerBridgeClosers.CentralCoverTargetLowerProjectionBridgeData B D)

Route146 replacement for Route145's lower-projection bridge residual.

theorem Q2Presentation.Induction.TargetKmodRRoute146BridgeClosers.centralCover_targetKmodRRepresentativeActionBridgeData_from_route146 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute146LowerQuotientEquivData B D) : Nonempty (TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (TargetKmodRSameTowerBridgeClosers.lowerProjectionData_of_bridge B D (lowerProjectionBridgeData_of_route146LowerQuotientEquiv B D E)))

Route146 replacement for Route145's representative-action bridge residual on the projection induced by the same Route146 lower quotient data.

Route145-shaped downstream provider

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

Route146 bridge packet: the lower quotient identification and its literal representative action law are tied to the same selected quotient.

• lowerQuotientEquivData : CentralCoverTargetRoute146LowerQuotientEquivData B D
• literalRepresentativeActionData : CentralCoverTargetRoute146LiteralRepresentativeActionData B D self.lowerQuotientEquivData

def Q2Presentation.Induction.TargetKmodRRoute146BridgeClosers.route145BridgeData_of_route146BridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute146BridgeData B D) : TargetKmodRRoute145SameTowerClosers.CentralCoverTargetRoute145BridgeData B D

Convert Route146 bridge data to the Route145 bridge-data surface.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute146BridgeClosers.centralCover_targetRoute146BridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute146BridgeData B D)

Route146 bridge data assembled from the two lowered Route146 atoms.

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

Route145's bundled bridge surface, supplied through Route146 atoms instead of Route145's bridge residuals.

def Q2Presentation.Induction.TargetKmodRRoute146BridgeClosers.quotientActionData_of_route146BridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute146BridgeData B D) : TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D

Route146 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.TargetKmodRRoute146BridgeClosers.centralCover_targetKmodRQuotientActionData_from_route146BridgeClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D)

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

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

Drop-in target decoration-kernel provider for Route146.

This has the same downstream theorem shape as TargetKmodRRoute145SameTowerClosers.centralCover_targetDecorationKernelData_from_route145SameTower, but its target-side non-local assumptions are the Route146 literal quotient/action atoms above.

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

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