Blueprint (GPT formalization): a profinite presentation of the absolute Galois group of ℚ₂

9. Proof of the boundary-framed theorem🔗

Lemma9.1
✓L∃∀Nused by 0

Lemma 9.2 of the paper (Targets with only trivial module factors).

Suppose every chief factor of L_Y is a trivial H-module. Let H_2 be the maximal 2-quotient of H and let N=\ker(H\to H_2). Then N has odd order, has a unique normal lift \widetilde N\triangleleft Y centralizing L_Y, and

Y\cong H\times_{H_2}Q, \qquad Q=Y/\widetilde N\text{ a finite $2$-group}.

Projection to Q identifies exact-image subgroups of Y projecting onto H with subgroups Q'\le Q that map onto H_2.

Lean code for Lemma9.1●4 declarations
  • defdefined in Q2Presentation/Induction/Recursion.lean
    complete
    def Q2Presentation.Induction.ScalarTerminalTarget
  (YtQ2Presentation.BoundaryFramedTarget : Q2Presentation.BoundaryFramedTargetQ2Presentation.BoundaryFramedTarget : Type 1A **boundary-framed marked target** `𝒴 = (Y, L_Y, π_Y, θ_Y)` (manuscript
Definition 4.1, `def:framed`): a finite group `Y` with a normal finite `2`-subgroup
`L_Y`, a surjection `π_Y : Y ↠ H` onto a finite *tame* quotient with kernel exactly
`L_Y`, and an *elementary decoration* `θ_Y : Y → Multiplicative E` into the
multiplicative image of a finite `𝔽₂`-vector space `E`.  The pair
`q_Y = (π_Y, θ_Y)` fixes both the tame quotient `Y / L_Y ≅ H` and the decoration. ) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    def Q2Presentation.Induction.ScalarTerminalTarget
  (YtQ2Presentation.BoundaryFramedTarget :
    Q2Presentation.BoundaryFramedTargetQ2Presentation.BoundaryFramedTarget : Type 1A **boundary-framed marked target** `𝒴 = (Y, L_Y, π_Y, θ_Y)` (manuscript
Definition 4.1, `def:framed`): a finite group `Y` with a normal finite `2`-subgroup
`L_Y`, a surjection `π_Y : Y ↠ H` onto a finite *tame* quotient with kernel exactly
`L_Y`, and an *elementary decoration* `θ_Y : Y → Multiplicative E` into the
multiplicative image of a finite `𝔽₂`-vector space `E`.  The pair
`q_Y = (π_Y, θ_Y)` fixes both the tame quotient `Y / L_Y ≅ H` and the decoration. ) :
  PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    **Scalar-terminal target** (`lem:scalarterminal` hypothesis): every `Y`-chief factor
inside `L_Y` is a trivial `H`-module.
  • defdefined in Q2Presentation/Induction/ScalarTerminal.lean
    complete
    def Q2Presentation.Induction.TerminalReduction
  (YtQ2Presentation.BoundaryFramedTarget : Q2Presentation.BoundaryFramedTargetQ2Presentation.BoundaryFramedTarget : Type 1A **boundary-framed marked target** `𝒴 = (Y, L_Y, π_Y, θ_Y)` (manuscript
Definition 4.1, `def:framed`): a finite group `Y` with a normal finite `2`-subgroup
`L_Y`, a surjection `π_Y : Y ↠ H` onto a finite *tame* quotient with kernel exactly
`L_Y`, and an *elementary decoration* `θ_Y : Y → Multiplicative E` into the
multiplicative image of a finite `𝔽₂`-vector space `E`.  The pair
`q_Y = (π_Y, θ_Y)` fixes both the tame quotient `Y / L_Y ≅ H` and the decoration. ) : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    def Q2Presentation.Induction.TerminalReduction
  (YtQ2Presentation.BoundaryFramedTarget :
    Q2Presentation.BoundaryFramedTargetQ2Presentation.BoundaryFramedTarget : Type 1A **boundary-framed marked target** `𝒴 = (Y, L_Y, π_Y, θ_Y)` (manuscript
Definition 4.1, `def:framed`): a finite group `Y` with a normal finite `2`-subgroup
`L_Y`, a surjection `π_Y : Y ↠ H` onto a finite *tame* quotient with kernel exactly
`L_Y`, and an *elementary decoration* `θ_Y : Y → Multiplicative E` into the
multiplicative image of a finite `𝔽₂`-vector space `E`.  The pair
`q_Y = (π_Y, θ_Y)` fixes both the tame quotient `Y / L_Y ≅ H` and the decoration. ) :
  PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    **The terminal Schur–Zassenhaus reduction datum** (manuscript `lem:scalarterminal`,
`eq:terminalpullback`).  For a scalar-terminal boundary-framed target the wild kernel's
odd complement splits off: there is a *normal* subgroup `Ñ ◁ Y` of **odd order** with
`2`-group quotient `Q = Y/Ñ`, **centralizing** `L_Y`.  Equivalently `Y ≅ H ×_{H₂} Q`
with `Q` a finite `2`-group: the terminal exact-image problem is governed entirely by
the `2`-group `Q`, hence (downstream) by the maximal pro-`2` data of the source.
  • theoremdefined in Q2Presentation/Induction/ScalarTerminal.lean
    complete
    theorem Q2Presentation.Induction.terminalSplit_of_scalarTerminal
  (YtQ2Presentation.BoundaryFramedTarget : Q2Presentation.BoundaryFramedTargetQ2Presentation.BoundaryFramedTarget : Type 1A **boundary-framed marked target** `𝒴 = (Y, L_Y, π_Y, θ_Y)` (manuscript
Definition 4.1, `def:framed`): a finite group `Y` with a normal finite `2`-subgroup
`L_Y`, a surjection `π_Y : Y ↠ H` onto a finite *tame* quotient with kernel exactly
`L_Y`, and an *elementary decoration* `θ_Y : Y → Multiplicative E` into the
multiplicative image of a finite `𝔽₂`-vector space `E`.  The pair
`q_Y = (π_Y, θ_Y)` fixes both the tame quotient `Y / L_Y ≅ H` and the decoration. ) (sYt.H tYt.H : YtQ2Presentation.BoundaryFramedTarget.HQ2Presentation.BoundaryFramedTarget.H (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite tame quotient group `H`. )
  (hgenSubgroup.closure {s, t} = ⊤ : Subgroup.closureSubgroup.closure.{u_1} {G : Type u_1} [Group G] (k : Set G) : Subgroup GThe `Subgroup` generated by a set.  {Insert.insert.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Insert α γ] : α → γ → γ`insert x xs` inserts the element `x` into the collection `xs`. sYt.H,Insert.insert.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Insert α γ] : α → γ → γ`insert x xs` inserts the element `x` into the collection `xs`.  tYt.H}Insert.insert.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Insert α γ] : α → γ → γ`insert x xs` inserts the element `x` into the collection `xs`.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. ⊤Top.top.{u_1} {α : Type u_1} [self : Top α] : αThe top (`⊤`, `\top`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊤` in identifiers is `top`.)
  (htameQ2Presentation.rconj t s = t ^ 2 : Q2Presentation.rconjQ2Presentation.rconj.{u_1} {G : Type u_1} [Group G] (x g : G) : GRight conjugation `x^g = g⁻¹ * x * g` (manuscript convention).  tYt.H sYt.H =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. tYt.H ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. 2)
  (hQ2Presentation.Induction.ScalarTerminalTarget Yt : Q2Presentation.Induction.ScalarTerminalTargetQ2Presentation.Induction.ScalarTerminalTarget (Yt : Q2Presentation.BoundaryFramedTarget) : Prop**Scalar-terminal target** (`lem:scalarterminal` hypothesis): every `Y`-chief factor
inside `L_Y` is a trivial `H`-module.  YtQ2Presentation.BoundaryFramedTarget) :
  Q2Presentation.Induction.TerminalReductionQ2Presentation.Induction.TerminalReduction (Yt : Q2Presentation.BoundaryFramedTarget) : Prop**The terminal Schur–Zassenhaus reduction datum** (manuscript `lem:scalarterminal`,
`eq:terminalpullback`).  For a scalar-terminal boundary-framed target the wild kernel's
odd complement splits off: there is a *normal* subgroup `Ñ ◁ Y` of **odd order** with
`2`-group quotient `Q = Y/Ñ`, **centralizing** `L_Y`.  Equivalently `Y ≅ H ×_{H₂} Q`
with `Q` a finite `2`-group: the terminal exact-image problem is governed entirely by
the `2`-group `Q`, hence (downstream) by the maximal pro-`2` data of the source.  YtQ2Presentation.BoundaryFramedTarget
    theorem Q2Presentation.Induction.terminalSplit_of_scalarTerminal
  (YtQ2Presentation.BoundaryFramedTarget :
    Q2Presentation.BoundaryFramedTargetQ2Presentation.BoundaryFramedTarget : Type 1A **boundary-framed marked target** `𝒴 = (Y, L_Y, π_Y, θ_Y)` (manuscript
Definition 4.1, `def:framed`): a finite group `Y` with a normal finite `2`-subgroup
`L_Y`, a surjection `π_Y : Y ↠ H` onto a finite *tame* quotient with kernel exactly
`L_Y`, and an *elementary decoration* `θ_Y : Y → Multiplicative E` into the
multiplicative image of a finite `𝔽₂`-vector space `E`.  The pair
`q_Y = (π_Y, θ_Y)` fixes both the tame quotient `Y / L_Y ≅ H` and the decoration. )
  (sYt.H tYt.H : YtQ2Presentation.BoundaryFramedTarget.HQ2Presentation.BoundaryFramedTarget.H (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite tame quotient group `H`. )
  (hgenSubgroup.closure {s, t} = ⊤ : Subgroup.closureSubgroup.closure.{u_1} {G : Type u_1} [Group G] (k : Set G) : Subgroup GThe `Subgroup` generated by a set.  {Insert.insert.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Insert α γ] : α → γ → γ`insert x xs` inserts the element `x` into the collection `xs`. sYt.H,Insert.insert.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Insert α γ] : α → γ → γ`insert x xs` inserts the element `x` into the collection `xs`.  tYt.H}Insert.insert.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Insert α γ] : α → γ → γ`insert x xs` inserts the element `x` into the collection `xs`.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. ⊤Top.top.{u_1} {α : Type u_1} [self : Top α] : αThe top (`⊤`, `\top`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊤` in identifiers is `top`.)
  (htameQ2Presentation.rconj t s = t ^ 2 :
    Q2Presentation.rconjQ2Presentation.rconj.{u_1} {G : Type u_1} [Group G] (x g : G) : GRight conjugation `x^g = g⁻¹ * x * g` (manuscript convention).  tYt.H sYt.H =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. tYt.H ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. 2)
  (hQ2Presentation.Induction.ScalarTerminalTarget Yt :
    Q2Presentation.Induction.ScalarTerminalTargetQ2Presentation.Induction.ScalarTerminalTarget (Yt : Q2Presentation.BoundaryFramedTarget) : Prop**Scalar-terminal target** (`lem:scalarterminal` hypothesis): every `Y`-chief factor
inside `L_Y` is a trivial `H`-module. 
      YtQ2Presentation.BoundaryFramedTarget) :
  Q2Presentation.Induction.TerminalReductionQ2Presentation.Induction.TerminalReduction (Yt : Q2Presentation.BoundaryFramedTarget) : Prop**The terminal Schur–Zassenhaus reduction datum** (manuscript `lem:scalarterminal`,
`eq:terminalpullback`).  For a scalar-terminal boundary-framed target the wild kernel's
odd complement splits off: there is a *normal* subgroup `Ñ ◁ Y` of **odd order** with
`2`-group quotient `Q = Y/Ñ`, **centralizing** `L_Y`.  Equivalently `Y ≅ H ×_{H₂} Q`
with `Q` a finite `2`-group: the terminal exact-image problem is governed entirely by
the `2`-group `Q`, hence (downstream) by the maximal pro-`2` data of the source. 
    YtQ2Presentation.BoundaryFramedTarget
    **STANDARD FINITE GROUP THEORY (isolated; Schur–Zassenhaus + coprime stability).**
The group-theoretic core of `lem:scalarterminal` (`eq:terminalpullback`): a finite group
`Y` with a normal `2`-subgroup `L_Y`, *tame* metacyclic quotient `H = Y/L_Y`
(two-generated by `s, t` with `rconj t s = t²`), all of whose `Y`-chief factors inside
`L_Y` are trivial `H`-modules, splits as `Y ≅ H ×_{H₂} Q` — equivalently there is a normal
odd-order subgroup `Ñ ◁ Y`, centralizing `L_Y`, with `2`-group quotient `Q = Y/Ñ`.

PROOF SKETCH (manuscript l.4484–4510).  The tame relation makes `⟨t⟩ ◁ H` odd
(`finite_tame_tau_odd`) with cyclic quotient `H/⟨t⟩`, so `H` is `2`-nilpotent and its
`2`-residual `N = O^{2}(H) = ker(H ↠ H₂)` has odd order.  Let `P = π_Y^{-1}(N)`; then
`L_Y ◁ P` with `[P : L_Y] = |N|` odd, coprime to the `2`-power `|L_Y|`, so Schur–Zassenhaus
(`Subgroup.exists_right_complement'_of_coprime`) gives an odd complement `Ñ ≤ P`.  Coprime
action on the trivial chief series gives `[L_Y, Ñ] = 1` (the **coprime stability** lemma
`[G,A]=[G,A,A]` for coprime `A`), whence `P = L_Y × Ñ`, `Ñ` is the characteristic Hall
`2'`-subgroup of `P` (so `Ñ ◁ Y`), and `Q = Y/Ñ` has order `|L_Y|·|H₂|`, a `2`-group.

This is entirely standard finite group theory.  The required coprime-action stability
lemma is formalized in `Induction/CoprimeStability.lean`; it is not local class field
theory.  The local-CFT content is isolated separately in
`terminalMarkedPro2_countCompatibility`.
  • theoremdefined in Q2Presentation/Induction/ScalarTerminal.lean
    complete
    theorem Q2Presentation.Induction.terminalMarkedPro2_localCFTCompatibility
  (pQ2Presentation.Induction.FramedPair : Q2Presentation.Induction.FramedPairQ2Presentation.Induction.FramedPair : Type 1A **framed pair** `(𝒴, F)`: a boundary-framed marked target together with a
boundary frame for it (manuscript Definition 4.1 + `eq:beta`).  This is the index of
Theorem 4.2: the boundary-framed surjection count `e_Γ^β` is a function of the pair.
The induction of `sec:induction` ranges over *all* such pairs simultaneously
("the induction is stated globally", l.1213), ordered by `|L_Y|`. )
  (hQ2Presentation.Induction.TerminalReduction p.fst : Q2Presentation.Induction.TerminalReductionQ2Presentation.Induction.TerminalReduction (Yt : Q2Presentation.BoundaryFramedTarget) : Prop**The terminal Schur–Zassenhaus reduction datum** (manuscript `lem:scalarterminal`,
`eq:terminalpullback`).  For a scalar-terminal boundary-framed target the wild kernel's
odd complement splits off: there is a *normal* subgroup `Ñ ◁ Y` of **odd order** with
`2`-group quotient `Q = Y/Ñ`, **centralizing** `L_Y`.  Equivalently `Y ≅ H ×_{H₂} Q`
with `Q` a finite `2`-group: the terminal exact-image problem is governed entirely by
the `2`-group `Q`, hence (downstream) by the maximal pro-`2` data of the source.  pQ2Presentation.Induction.FramedPair.fstSigma.fst.{u, v} {α : Type u} {β : α → Type v} (self : Sigma β) : αThe first component of a dependent pair.
) :
  Q2Presentation.Induction.framedCountAQ2Presentation.Induction.framedCountA (p : Q2Presentation.Induction.FramedPair) : Cardinal.{0}The **candidate** boundary-framed surjection count `e_{Γ_A}^β(𝒴)`
(`eq:eGamma`), as a cardinal `|boundaryFramedSurj boundaryPackage_GammaA 𝒴 F|`.  pQ2Presentation.Induction.FramedPair =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    Q2Presentation.Induction.framedCountQQ2Presentation.Induction.framedCountQ (p : Q2Presentation.Induction.FramedPair) : Cardinal.{0}The **local** boundary-framed surjection count `e_{G_{ℚ₂}}^β(𝒴)`
(`eq:eGamma`), as a cardinal `|boundaryFramedSurj boundaryPackage_GQ2 𝒴 F|`.  pQ2Presentation.Induction.FramedPair
    theorem Q2Presentation.Induction.terminalMarkedPro2_localCFTCompatibility
  (pQ2Presentation.Induction.FramedPair :
    Q2Presentation.Induction.FramedPairQ2Presentation.Induction.FramedPair : Type 1A **framed pair** `(𝒴, F)`: a boundary-framed marked target together with a
boundary frame for it (manuscript Definition 4.1 + `eq:beta`).  This is the index of
Theorem 4.2: the boundary-framed surjection count `e_Γ^β` is a function of the pair.
The induction of `sec:induction` ranges over *all* such pairs simultaneously
("the induction is stated globally", l.1213), ordered by `|L_Y|`. )
  (hQ2Presentation.Induction.TerminalReduction p.fst :
    Q2Presentation.Induction.TerminalReductionQ2Presentation.Induction.TerminalReduction (Yt : Q2Presentation.BoundaryFramedTarget) : Prop**The terminal Schur–Zassenhaus reduction datum** (manuscript `lem:scalarterminal`,
`eq:terminalpullback`).  For a scalar-terminal boundary-framed target the wild kernel's
odd complement splits off: there is a *normal* subgroup `Ñ ◁ Y` of **odd order** with
`2`-group quotient `Q = Y/Ñ`, **centralizing** `L_Y`.  Equivalently `Y ≅ H ×_{H₂} Q`
with `Q` a finite `2`-group: the terminal exact-image problem is governed entirely by
the `2`-group `Q`, hence (downstream) by the maximal pro-`2` data of the source. 
      pQ2Presentation.Induction.FramedPair.fstSigma.fst.{u, v} {α : Type u} {β : α → Type v} (self : Sigma β) : αThe first component of a dependent pair.
) :
  Q2Presentation.Induction.framedCountAQ2Presentation.Induction.framedCountA (p : Q2Presentation.Induction.FramedPair) : Cardinal.{0}The **candidate** boundary-framed surjection count `e_{Γ_A}^β(𝒴)`
(`eq:eGamma`), as a cardinal `|boundaryFramedSurj boundaryPackage_GammaA 𝒴 F|`. 
      pQ2Presentation.Induction.FramedPair =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    Q2Presentation.Induction.framedCountQQ2Presentation.Induction.framedCountQ (p : Q2Presentation.Induction.FramedPair) : Cardinal.{0}The **local** boundary-framed surjection count `e_{G_{ℚ₂}}^β(𝒴)`
(`eq:eGamma`), as a cardinal `|boundaryFramedSurj boundaryPackage_GQ2 𝒴 F|`. 
      pQ2Presentation.Induction.FramedPair
    **LOCAL MARKED PRO-`2` CFT INPUT** (terminal count bridge, `lem:scalarterminal`
`eq:terminalcompatibility`).  Given the proven Schur–Zassenhaus terminal reduction
`Y ≅ H ×_{H₂} Q` (`TerminalReduction`), the fully marked local pro-`2`
identification gives the compatible-map comparison, hence the two boundary-framed
surjection counts agree.

This is the irreducible **local class field theory** input of the terminal base case:
once the target is reduced to its `2`-group quotient `Q`, the boundary-framed surjections
of either source biject with marking-compatible maps `Π → Q`, and the two resulting
counts coincide *by the fully marked isomorphism of the maximal pro-`2` quotients of
`Γ_A` and `G_{ℚ₂}`* (`prop:pro2`, the project's `labute_GQ2_maxPro2_marked`).

This is **not** derivable from `labute_GQ2_maxPro2_marked` plus the current package by
projection alone.  The existing package proves the two maximal pro-`2` quotients are
fully marked, but it does not yet formalize the terminal pullback/count bijection
turning maps `Γ → Y` into compatible maps `Π → Q`.  The axiom is therefore the atomic
local marked-pro-`2` count primitive left at this interface.  It takes the proven
group-theoretic reduction as a hypothesis, so it asserts strictly less than the original
`boundaryFramed_scalarTerminal_equal`.
Proof

Proved in §9 of the paper. Ingredients: Lemma 3.1.