theorem Q2Presentation.Induction.towerHead_submodule_dichotomy
  {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|`. }
  (chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p :
    Q2Presentation.Induction.FirstNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA non-scalar chief factor of `L_Y` that is **first**: every chief factor strictly
below it (i.e. with upper term contained in `lower`) is scalar.  This is the manuscript's
choice `S ◁ P` at l.3616–3623 ("all chief factors below `S` are scalar and `V` is the
first non-scalar simple factor"), which `lem:collapse` requires for the coprime step
`[S, Ñ] = 1`. 
      pQ2Presentation.Induction.FramedPair)
  (KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor :
    Q2Presentation.Induction.KernelMinimalQ2Presentation.Induction.KernelMinimal {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : TypeThe manuscript's kernel choice (l.3623): `K ◁ Y`, `K ≤ P`, `KS = P`, and `K` is
**⊆-minimal** with these properties — stated as: any `Y`-normal `K' ≤ K` still joining
with `S` to `P` equals `K`.  (This, not leastness among all candidates, is what
`lem:simplehead` and `lem:collapse` use: both apply it to subgroups of `K`.) 
      chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p.toNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor.toNonScalarChiefFactor {p : Q2Presentation.Induction.FramedPair}
  (self : Q2Presentation.Induction.FirstNonScalarChiefFactor p) : Q2Presentation.Induction.NonScalarChiefFactor p)
  (V'Submodule (ZMod 2) (Q2Presentation.Induction.towerM K ⧸ Q2Presentation.Induction.towerT K) :
    SubmoduleSubmodule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type vA submodule of a module is one which is closed under vector operations.
This is a sufficient condition for the subset of vectors in the submodule
to themselves form a module.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2)
      (HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
Q2Presentation.Induction.towerMQ2Presentation.Induction.towerM {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) : TypeThe additive elementary module layer `M = K/Φ(K)` (`lem:simplehead`).  KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor ⧸HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.

        Q2Presentation.Induction.towerTQ2Presentation.Induction.towerT {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) :
  Submodule (ZMod 2) (Q2Presentation.Induction.towerM K)The manuscript's radical layer `T = (K ∩ S)/R ◁ M` (l.3628), as a
`ZMod 2`-submodule of the additive module `M`. 
          KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
)
  (hact∀ (c : Q2Presentation.Induction.towerC K), ∀ v ∈ V', (Q2Presentation.Induction.headActE chief K c) v ∈ V' :
    ∀
      (cQ2Presentation.Induction.towerC K :
        Q2Presentation.Induction.towerCQ2Presentation.Induction.towerC {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) : TypeThe lower target `C = Y/K` (`eq:targettower`). 
          KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor),
      ∀ vQ2Presentation.Induction.towerM K ⧸ Q2Presentation.Induction.towerT K ∈ V'Submodule (ZMod 2) (Q2Presentation.Induction.towerM K ⧸ Q2Presentation.Induction.towerT K),
        (Q2Presentation.Induction.headActEQ2Presentation.Induction.headActE {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (c : Q2Presentation.Induction.towerC K) :
  Q2Presentation.Induction.towerM K ⧸ Q2Presentation.Induction.towerT K →ₗ[ZMod 2]
    Q2Presentation.Induction.towerM K ⧸ Q2Presentation.Induction.towerT KThe descended `C`-action on the head `V = M/T` (`towerActM` mod the
stable radical layer, via `Submodule.mapQ`). 
              chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor cQ2Presentation.Induction.towerC K)
            vQ2Presentation.Induction.towerM K ⧸ Q2Presentation.Induction.towerT K ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
          V'Submodule (ZMod 2) (Q2Presentation.Induction.towerM K ⧸ Q2Presentation.Induction.towerT K)) :
  V'Submodule (ZMod 2) (Q2Presentation.Induction.towerM K ⧸ Q2Presentation.Induction.towerT K) =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`. ⊥Bot.bot.{u_1} {α : Type u_1} [self : Bot α] : αThe bot (`⊥`, `\bot`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊥` in identifiers is `bot`. ∨Or (a b : Prop) : Prop`Or a b`, or `a ∨ b`, is the disjunction of propositions. There are two
constructors for `Or`, called `Or.inl : a → a ∨ b` and `Or.inr : b → a ∨ b`,
and you can use `match` or `cases` to destruct an `Or` assumption into the
two cases.


Conventions for notations in identifiers:

 * The recommended spelling of `∨` in identifiers is `or`.

 * The recommended spelling of `\/` in identifiers is `or` (prefer `∨` over `\/`). V'Submodule (ZMod 2) (Q2Presentation.Induction.towerM K ⧸ Q2Presentation.Induction.towerT K) =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`.

theorem Q2Presentation.Induction.mChild_hinv
  {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|`. }
  (chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p :
    Q2Presentation.Induction.FirstNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA non-scalar chief factor of `L_Y` that is **first**: every chief factor strictly
below it (i.e. with upper term contained in `lower`) is scalar.  This is the manuscript's
choice `S ◁ P` at l.3616–3623 ("all chief factors below `S` are scalar and `V` is the
first non-scalar simple factor"), which `lem:collapse` requires for the coprime step
`[S, Ñ] = 1`. 
      pQ2Presentation.Induction.FramedPair)
  (KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor :
    Q2Presentation.Induction.KernelMinimalQ2Presentation.Induction.KernelMinimal {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : TypeThe manuscript's kernel choice (l.3623): `K ◁ Y`, `K ≤ P`, `KS = P`, and `K` is
**⊆-minimal** with these properties — stated as: any `Y`-normal `K' ≤ K` still joining
with `S` to `P` equals `K`.  (This, not leastness among all candidates, is what
`lem:simplehead` and `lem:collapse` use: both apply it to subgroups of `K`.) 
      chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p.toNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor.toNonScalarChiefFactor {p : Q2Presentation.Induction.FramedPair}
  (self : Q2Presentation.Induction.FirstNonScalarChiefFactor p) : Q2Presentation.Induction.NonScalarChiefFactor p)
  (fModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.mChildKernel chief K)) :
    Module.DualModule.Dual.{u_4, u_5} (R : Type u_4) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] : Type (max u_5 u_4)The left dual space of an R-module M is the R-module of linear maps `M → R`.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2)
      (Q2Presentation.Lifting.NAddQ2Presentation.Lifting.NAdd {Yt : Q2Presentation.BoundaryFramedTarget}
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) : TypeThe additive `F₂`-carrier of an elementary kernel. 
        (Q2Presentation.Induction.mChildKernelQ2Presentation.Induction.mChildKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) :
  Q2Presentation.Lifting.ElementaryKernel (Q2Presentation.Induction.XRZero.xrChild chief K).fst**The elementary `M`-kernel at the child** `B = Y/Φ(K)`
(`lem:simplehead` carrier for `lem:elementarystage`): `N = M' = K/Φ(K)`. 
          chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor))) :
  (∀
      (y(Q2Presentation.Induction.XRZero.xrChild chief K).fst.Y :
        (Q2Presentation.Induction.XRZero.xrChildQ2Presentation.Induction.XRZero.xrChild {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) : Q2Presentation.Induction.FramedPairThe `𝒳_R = 0` child: the quotient framed pair at `N = Φ`-layer. 
              chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor).fstSigma.fst.{u, v} {α : Type u} {β : α → Type v} (self : Sigma β) : αThe first component of a dependent pair.
.YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. )
      (mQ2Presentation.Lifting.NAdd (Q2Presentation.Induction.mChildKernel chief K) :
        Q2Presentation.Lifting.NAddQ2Presentation.Lifting.NAdd {Yt : Q2Presentation.BoundaryFramedTarget}
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) : TypeThe additive `F₂`-carrier of an elementary kernel. 
          (Q2Presentation.Induction.mChildKernelQ2Presentation.Induction.mChildKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) :
  Q2Presentation.Lifting.ElementaryKernel (Q2Presentation.Induction.XRZero.xrChild chief K).fst**The elementary `M`-kernel at the child** `B = Y/Φ(K)`
(`lem:simplehead` carrier for `lem:elementarystage`): `N = M' = K/Φ(K)`. 
            chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)),
      fModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.mChildKernel chief K))
          ((Q2Presentation.Lifting.conjEndNQ2Presentation.Lifting.conjEndN {Yt : Q2Presentation.BoundaryFramedTarget}
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) (y : Yt.Y) : Module.End (ZMod 2) (Q2Presentation.Lifting.NAdd E)Right conjugation by `y` as an `F₂`-linear endomorphism of `N`. 
              (Q2Presentation.Induction.mChildKernelQ2Presentation.Induction.mChildKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) :
  Q2Presentation.Lifting.ElementaryKernel (Q2Presentation.Induction.XRZero.xrChild chief K).fst**The elementary `M`-kernel at the child** `B = Y/Φ(K)`
(`lem:simplehead` carrier for `lem:elementarystage`): `N = M' = K/Φ(K)`. 
                chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
              y(Q2Presentation.Induction.XRZero.xrChild chief K).fst.Y)
            mQ2Presentation.Lifting.NAdd (Q2Presentation.Induction.mChildKernel chief K)) =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`.
        fModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.mChildKernel chief K)) mQ2Presentation.Lifting.NAdd (Q2Presentation.Induction.mChildKernel chief K)) →
    fModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.mChildKernel chief K)) =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`. 0

theorem Q2Presentation.Induction.mstage_hinv
  {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|`. }
  (chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p :
    Q2Presentation.Induction.FirstNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA non-scalar chief factor of `L_Y` that is **first**: every chief factor strictly
below it (i.e. with upper term contained in `lower`) is scalar.  This is the manuscript's
choice `S ◁ P` at l.3616–3623 ("all chief factors below `S` are scalar and `V` is the
first non-scalar simple factor"), which `lem:collapse` requires for the coprime step
`[S, Ñ] = 1`. 
      pQ2Presentation.Induction.FramedPair)
  (KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor :
    Q2Presentation.Induction.KernelMinimalQ2Presentation.Induction.KernelMinimal {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : TypeThe manuscript's kernel choice (l.3623): `K ◁ Y`, `K ≤ P`, `KS = P`, and `K` is
**⊆-minimal** with these properties — stated as: any `Y`-normal `K' ≤ K` still joining
with `S` to `P` equals `K`.  (This, not leastness among all candidates, is what
`lem:simplehead` and `lem:collapse` use: both apply it to subgroups of `K`.) 
      chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p.toNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor.toNonScalarChiefFactor {p : Q2Presentation.Induction.FramedPair}
  (self : Q2Presentation.Induction.FirstNonScalarChiefFactor p) : Q2Presentation.Induction.NonScalarChiefFactor p)
  (hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1 :
    Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number.
If `α` is infinite, `Nat.card α = 0`. 
        ↥(Q2Presentation.Induction.kernelFrattiniQ2Presentation.Induction.kernelFrattini {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) :
  Subgroup p.fst.YThe literal Frattini subgroup `R = Φ(K)` of the kernel, as a subgroup of `Y`
(the manuscript's `R`, l.3626). 
            KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) =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`.
      1)
  (fModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR)) :
    Module.DualModule.Dual.{u_4, u_5} (R : Type u_4) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] : Type (max u_5 u_4)The left dual space of an R-module M is the R-module of linear maps `M → R`.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2)
      (Q2Presentation.Lifting.NAddQ2Presentation.Lifting.NAdd {Yt : Q2Presentation.BoundaryFramedTarget}
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) : TypeThe additive `F₂`-carrier of an elementary kernel. 
        (Q2Presentation.Induction.mstageKernelQ2Presentation.Induction.mstageKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1) : Q2Presentation.Lifting.ElementaryKernel p.fst**The mstage consumer kernel**, bundled for the cocycle bridge. 
          chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1))) :
  (∀ (yp.fst.Y : pQ2Presentation.Induction.FramedPair.fstSigma.fst.{u, v} {α : Type u} {β : α → Type v} (self : Sigma β) : αThe first component of a dependent pair.
.YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. )
      (mQ2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR) :
        Q2Presentation.Lifting.NAddQ2Presentation.Lifting.NAdd {Yt : Q2Presentation.BoundaryFramedTarget}
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) : TypeThe additive `F₂`-carrier of an elementary kernel. 
          (Q2Presentation.Induction.mstageKernelQ2Presentation.Induction.mstageKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1) : Q2Presentation.Lifting.ElementaryKernel p.fst**The mstage consumer kernel**, bundled for the cocycle bridge. 
            chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1)),
      fModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR))
          ((Q2Presentation.Lifting.conjEndNQ2Presentation.Lifting.conjEndN {Yt : Q2Presentation.BoundaryFramedTarget}
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) (y : Yt.Y) : Module.End (ZMod 2) (Q2Presentation.Lifting.NAdd E)Right conjugation by `y` as an `F₂`-linear endomorphism of `N`. 
              (Q2Presentation.Induction.mstageKernelQ2Presentation.Induction.mstageKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1) : Q2Presentation.Lifting.ElementaryKernel p.fst**The mstage consumer kernel**, bundled for the cocycle bridge. 
                chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1)
              yp.fst.Y)
            mQ2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR)) =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`.
        fModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR)) mQ2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR)) →
    fModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR)) =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`. 0

theorem Q2Presentation.Induction.mChild_conjInvDuals_eq_bot
  {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|`. }
  (chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p :
    Q2Presentation.Induction.FirstNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA non-scalar chief factor of `L_Y` that is **first**: every chief factor strictly
below it (i.e. with upper term contained in `lower`) is scalar.  This is the manuscript's
choice `S ◁ P` at l.3616–3623 ("all chief factors below `S` are scalar and `V` is the
first non-scalar simple factor"), which `lem:collapse` requires for the coprime step
`[S, Ñ] = 1`. 
      pQ2Presentation.Induction.FramedPair)
  (KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor :
    Q2Presentation.Induction.KernelMinimalQ2Presentation.Induction.KernelMinimal {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : TypeThe manuscript's kernel choice (l.3623): `K ◁ Y`, `K ≤ P`, `KS = P`, and `K` is
**⊆-minimal** with these properties — stated as: any `Y`-normal `K' ≤ K` still joining
with `S` to `P` equals `K`.  (This, not leastness among all candidates, is what
`lem:simplehead` and `lem:collapse` use: both apply it to subgroups of `K`.) 
      chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p.toNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor.toNonScalarChiefFactor {p : Q2Presentation.Induction.FramedPair}
  (self : Q2Presentation.Induction.FirstNonScalarChiefFactor p) : Q2Presentation.Induction.NonScalarChiefFactor p) :
  Q2Presentation.Lifting.conjInvDualsQ2Presentation.Lifting.conjInvDuals {Yt : Q2Presentation.BoundaryFramedTarget}
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) :
  Submodule (ZMod 2) (Module.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd E))The conjugation-invariant duals `X = (R^∨)^Y = (R^∨)^C` of an
elementary kernel (consumer spelling of the manuscript's `𝒳_R`,
§7 l.3720–3723). 
      (Q2Presentation.Induction.mChildKernelQ2Presentation.Induction.mChildKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) :
  Q2Presentation.Lifting.ElementaryKernel (Q2Presentation.Induction.XRZero.xrChild chief K).fst**The elementary `M`-kernel at the child** `B = Y/Φ(K)`
(`lem:simplehead` carrier for `lem:elementarystage`): `N = M' = K/Φ(K)`. 
        chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) =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`.
    ⊥Bot.bot.{u_1} {α : Type u_1} [self : Bot α] : αThe bot (`⊥`, `\bot`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊥` in identifiers is `bot`.

theorem Q2Presentation.Induction.sec7_radical_bockstein_witness
  {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|`. }
  (chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p :
    Q2Presentation.Induction.FirstNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA non-scalar chief factor of `L_Y` that is **first**: every chief factor strictly
below it (i.e. with upper term contained in `lower`) is scalar.  This is the manuscript's
choice `S ◁ P` at l.3616–3623 ("all chief factors below `S` are scalar and `V` is the
first non-scalar simple factor"), which `lem:collapse` requires for the coprime step
`[S, Ñ] = 1`. 
      pQ2Presentation.Induction.FramedPair)
  (KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor :
    Q2Presentation.Induction.KernelMinimalQ2Presentation.Induction.KernelMinimal {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : TypeThe manuscript's kernel choice (l.3623): `K ◁ Y`, `K ≤ P`, `KS = P`, and `K` is
**⊆-minimal** with these properties — stated as: any `Y`-normal `K' ≤ K` still joining
with `S` to `P` equals `K`.  (This, not leastness among all candidates, is what
`lem:simplehead` and `lem:collapse` use: both apply it to subgroups of `K`.) 
      chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p.toNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor.toNonScalarChiefFactor {p : Q2Presentation.Induction.FramedPair}
  (self : Q2Presentation.Induction.FirstNonScalarChiefFactor p) : Q2Presentation.Induction.NonScalarChiefFactor p)
  (hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1 :
    Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number.
If `α` is infinite, `Nat.card α = 0`. 
        ↥(Q2Presentation.Induction.kernelFrattiniQ2Presentation.Induction.kernelFrattini {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) :
  Subgroup p.fst.YThe literal Frattini subgroup `R = Φ(K)` of the kernel, as a subgroup of `Y`
(the manuscript's `R`, l.3626). 
            KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) =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`.
      1)
  (gQ2Presentation.boundaryFramedSurj Q2Presentation.boundaryPackage_GammaA
  (Q2Presentation.TorsorProgram.quotientFramedTarget p.fst (Q2Presentation.Induction.mstageKernel chief K hR).N ⋯ ⋯)
  (Q2Presentation.TorsorProgram.quotientFrame p.fst (Q2Presentation.Induction.mstageKernel chief K hR).N ⋯ ⋯ p.snd) :
    Q2Presentation.boundaryFramedSurjQ2Presentation.boundaryFramedSurj {Γ : ProfiniteGrp.{0}} (B : Q2Presentation.BoundaryPackage Γ)
  (Yt : Q2Presentation.BoundaryFramedTarget) (F : Q2Presentation.BoundaryFrame Yt) : TypeThe **boundary-framed surjections** `e_Γ^β(𝒴)` (manuscript `eq:eGamma`): the
continuous surjections `f : Γ ↠ Y` whose induced map to `H × E` is the prescribed
`β ∘ b_Γ`, i.e. `q_Y ∘ f = β ∘ b_Γ`.  This is the subtype counted in Theorem 4.2;
its cardinality is `e_Γ^β(𝒴)`. 
      Q2Presentation.boundaryPackage_GammaAQ2Presentation.boundaryPackage_GammaA : Q2Presentation.BoundaryPackage Q2Presentation.GammaA**The candidate boundary package** (manuscript Prop 3.14, `prop:compatiblemarking`;
plan Turn 4 §6).  The Stage-C data of `Γ_A`: the common tame quotient `gammaTameMap`,
the maximal pro-`2` quotient `p : Γ_A ⟶ Π`, and the common unramified character
`ν = gammaTameMap ≫ ν_t`, through which both factor. 
      (Q2Presentation.TorsorProgram.quotientFramedTargetQ2Presentation.TorsorProgram.quotientFramedTarget (Yt : Q2Presentation.BoundaryFramedTarget) (N : Subgroup Yt.Y)
  [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) : Q2Presentation.BoundaryFramedTarget**The quotient framed target** `Y/N` (same `H`, same `E`, image wild kernel). 
        pQ2Presentation.Induction.FramedPair.fstSigma.fst.{u, v} {α : Type u} {β : α → Type v} (self : Sigma β) : αThe first component of a dependent pair.

        (Q2Presentation.Induction.mstageKernelQ2Presentation.Induction.mstageKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1) : Q2Presentation.Lifting.ElementaryKernel p.fst**The mstage consumer kernel**, bundled for the cocycle bridge. 
            chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1).NQ2Presentation.Lifting.ElementaryKernel.N {Yt : Q2Presentation.BoundaryFramedTarget}
  (self : Q2Presentation.Lifting.ElementaryKernel Yt) : Subgroup Yt.Y
        ⋯ ⋯)
      (Q2Presentation.TorsorProgram.quotientFrameQ2Presentation.TorsorProgram.quotientFrame (Yt : Q2Presentation.BoundaryFramedTarget) (N : Subgroup Yt.Y)
  [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) (F : Q2Presentation.BoundaryFrame Yt) :
  Q2Presentation.BoundaryFrame (Q2Presentation.TorsorProgram.quotientFramedTarget Yt N hNLY hNθ)The frame transports verbatim (`H`, `E`, `α`, `ψ`, `β` unchanged). 
        pQ2Presentation.Induction.FramedPair.fstSigma.fst.{u, v} {α : Type u} {β : α → Type v} (self : Sigma β) : αThe first component of a dependent pair.

        (Q2Presentation.Induction.mstageKernelQ2Presentation.Induction.mstageKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1) : Q2Presentation.Lifting.ElementaryKernel p.fst**The mstage consumer kernel**, bundled for the cocycle bridge. 
            chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1).NQ2Presentation.Lifting.ElementaryKernel.N {Yt : Q2Presentation.BoundaryFramedTarget}
  (self : Q2Presentation.Lifting.ElementaryKernel Yt) : Subgroup Yt.Y
        ⋯ ⋯ pQ2Presentation.Induction.FramedPair.sndSigma.snd.{u, v} {α : Type u} {β : α → Type v} (self : Sigma β) : β self.fstThe second component of a dependent pair. Its type depends on the first component.
))
  (qQ2Presentation.Marking p.fst.Y : Q2Presentation.MarkingQ2Presentation.Marking.{u_1} (G : Type u_1) [Group G] : Type u_1A marking assigns a group element to each of the four generators.  pQ2Presentation.Induction.FramedPair.fstSigma.fst.{u, v} {α : Type u} {β : α → Type v} (self : Sigma β) : αThe first component of a dependent pair.
.YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. )
  (hlift∀ (a : Q2Presentation.Gen),
  (QuotientGroup.mk' (Q2Presentation.Induction.mstageKernel chief K hR).N) (q a) =
    (ProfiniteGrp.Hom.hom (↑g).hom) (Q2Presentation.gammaGen a) :
    ∀ (aQ2Presentation.Gen : Q2Presentation.GenQ2Presentation.Gen : TypeThe four marked generators of the candidate presentation. ),
      (QuotientGroup.mk'QuotientGroup.mk'.{u_1} {G : Type u_1} [Group G] (N : Subgroup G) [nN : N.Normal] : G →* G ⧸ NThe group homomorphism from `G` to `G/N`. 
            (Q2Presentation.Induction.mstageKernelQ2Presentation.Induction.mstageKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1) : Q2Presentation.Lifting.ElementaryKernel p.fst**The mstage consumer kernel**, bundled for the cocycle bridge. 
                chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1).NQ2Presentation.Lifting.ElementaryKernel.N {Yt : Q2Presentation.BoundaryFramedTarget}
  (self : Q2Presentation.Lifting.ElementaryKernel Yt) : Subgroup Yt.Y)
          (qQ2Presentation.Marking p.fst.Y aQ2Presentation.Gen) =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`.
        (ProfiniteGrp.Hom.homProfiniteGrp.Hom.hom.{u} {M N : ProfiniteGrp.{u}} (f : M.Hom N) : ↑M.toProfinite.toTop →ₜ* ↑N.toProfinite.toTopThe underlying `ContinuousMonoidHom`.  (↑gQ2Presentation.boundaryFramedSurj Q2Presentation.boundaryPackage_GammaA
  (Q2Presentation.TorsorProgram.quotientFramedTarget p.fst (Q2Presentation.Induction.mstageKernel chief K hR).N ⋯ ⋯)
  (Q2Presentation.TorsorProgram.quotientFrame p.fst (Q2Presentation.Induction.mstageKernel chief K hR).N ⋯ ⋯ p.snd)).homQ2Presentation.Profinite.SurjContHom.hom.{u} {P Q : ProfiniteGrp.{u}}
  (self : Q2Presentation.Profinite.SurjContHom P Q) : P ⟶ QThe underlying morphism of profinite groups. )
          (Q2Presentation.gammaGenQ2Presentation.gammaGen (a : Q2Presentation.Gen) : ↑Q2Presentation.GammaA.toProfinite.toTopThe four universal generators `σ, τ, x₀, x₁` of `Γ_A`, as the compatible
families of marked generators.  aQ2Presentation.Gen))
  (hframe∀ (a : Q2Presentation.Gen),
  p.fst.qYMap (q a) =
    (ProfiniteGrp.Hom.hom p.snd.beta)
      ((ProfiniteGrp.Hom.hom Q2Presentation.boundaryPackage_GammaA.toBoundary) (Q2Presentation.gammaGen a)) :
    ∀ (aQ2Presentation.Gen : Q2Presentation.GenQ2Presentation.Gen : TypeThe four marked generators of the candidate presentation. ),
      pQ2Presentation.Induction.FramedPair.fstSigma.fst.{u, v} {α : Type u} {β : α → Type v} (self : Sigma β) : αThe first component of a dependent pair.
.qYMapQ2Presentation.BoundaryFramedTarget.qYMap (Yt : Q2Presentation.BoundaryFramedTarget) :
  Yt.Y →* Yt.H × Multiplicative Yt.EThe combined map `q_Y = (π_Y, θ_Y) : Y →* H × Multiplicative E` of manuscript
Definition 4.1: the data the boundary-framed count holds fixed.  (qQ2Presentation.Marking p.fst.Y aQ2Presentation.Gen) =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`.
        (ProfiniteGrp.Hom.homProfiniteGrp.Hom.hom.{u} {M N : ProfiniteGrp.{u}} (f : M.Hom N) : ↑M.toProfinite.toTop →ₜ* ↑N.toProfinite.toTopThe underlying `ContinuousMonoidHom`.  pQ2Presentation.Induction.FramedPair.sndSigma.snd.{u, v} {α : Type u} {β : α → Type v} (self : Sigma β) : β self.fstThe second component of a dependent pair. Its type depends on the first component.
.betaQ2Presentation.BoundaryFrame.beta {Yt : Q2Presentation.BoundaryFramedTarget} (self : Q2Presentation.BoundaryFrame Yt) :
  Q2Presentation.Boundary ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Yt.H × Multiplicative Yt.E))The induced boundary map `β : ∂_bd → H × Multiplicative E`. )
          ((ProfiniteGrp.Hom.homProfiniteGrp.Hom.hom.{u} {M N : ProfiniteGrp.{u}} (f : M.Hom N) : ↑M.toProfinite.toTop →ₜ* ↑N.toProfinite.toTopThe underlying `ContinuousMonoidHom`. 
              Q2Presentation.boundaryPackage_GammaAQ2Presentation.boundaryPackage_GammaA : Q2Presentation.BoundaryPackage Q2Presentation.GammaA**The candidate boundary package** (manuscript Prop 3.14, `prop:compatiblemarking`;
plan Turn 4 §6).  The Stage-C data of `Γ_A`: the common tame quotient `gammaTameMap`,
the maximal pro-`2` quotient `p : Γ_A ⟶ Π`, and the common unramified character
`ν = gammaTameMap ≫ ν_t`, through which both factor. .toBoundaryQ2Presentation.BoundaryPackage.toBoundary {Γ : ProfiniteGrp.{0}} (B : Q2Presentation.BoundaryPackage Γ) :
  Γ ⟶ Q2Presentation.Boundary**The boundary map** `b_Γ : Γ ⟶ ∂_bd` (manuscript `eq:boundarymap`), the universal
map into the fibre product induced by the compatible pair `(tameMap, pro2Map)`. )
            (Q2Presentation.gammaGenQ2Presentation.gammaGen (a : Q2Presentation.Gen) : ↑Q2Presentation.GammaA.toProfinite.toTopThe four universal generators `σ, τ, x₀, x₁` of `Γ_A`, as the compatible
families of marked generators.  aQ2Presentation.Gen)))
  (WSubmodule (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR)) :
    SubmoduleSubmodule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type vA submodule of a module is one which is closed under vector operations.
This is a sufficient condition for the subset of vectors in the submodule
to themselves form a module.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2)
      (Q2Presentation.Lifting.NAddQ2Presentation.Lifting.NAdd {Yt : Q2Presentation.BoundaryFramedTarget}
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) : TypeThe additive `F₂`-carrier of an elementary kernel. 
        (Q2Presentation.Induction.mstageKernelQ2Presentation.Induction.mstageKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1) : Q2Presentation.Lifting.ElementaryKernel p.fst**The mstage consumer kernel**, bundled for the cocycle bridge. 
          chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1)))
  (hWst∀ (y : p.fst.Y),
  ∀ m ∈ W, ((Q2Presentation.Lifting.conjFamily (Q2Presentation.Induction.mstageKernel chief K hR)).op y) m ∈ W :
    ∀ (yp.fst.Y : pQ2Presentation.Induction.FramedPair.fstSigma.fst.{u, v} {α : Type u} {β : α → Type v} (self : Sigma β) : αThe first component of a dependent pair.
.YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. ),
      ∀ mQ2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR) ∈ WSubmodule (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR)),
        ((Q2Presentation.Lifting.conjFamilyQ2Presentation.Lifting.conjFamily {Yt : Q2Presentation.BoundaryFramedTarget}
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) :
  Q2Presentation.Lifting.OperatorFamily Yt (Q2Presentation.Lifting.NAdd E)The concrete conjugation family of an elementary kernel. 
                  (Q2Presentation.Induction.mstageKernelQ2Presentation.Induction.mstageKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1) : Q2Presentation.Lifting.ElementaryKernel p.fst**The mstage consumer kernel**, bundled for the cocycle bridge. 
                    chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1)).opQ2Presentation.Lifting.OperatorFamily.op {Yt : Q2Presentation.BoundaryFramedTarget} {V : Type} [AddCommGroup V]
  [Module (ZMod 2) V] (self : Q2Presentation.Lifting.OperatorFamily Yt V) : Yt.Y → Module.End (ZMod 2) V
              yp.fst.Y)
            mQ2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR) ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
          WSubmodule (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR)))
  (wQ2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR) :
    Q2Presentation.Lifting.NAddQ2Presentation.Lifting.NAdd {Yt : Q2Presentation.BoundaryFramedTarget}
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) : TypeThe additive `F₂`-carrier of an elementary kernel. 
      (Q2Presentation.Induction.mstageKernelQ2Presentation.Induction.mstageKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1) : Q2Presentation.Lifting.ElementaryKernel p.fst**The mstage consumer kernel**, bundled for the cocycle bridge. 
        chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1))
  (hwfix∀ (y : p.fst.Y), ((Q2Presentation.Lifting.conjFamily (Q2Presentation.Induction.mstageKernel chief K hR)).op y) w - w ∈ W :
    ∀ (yp.fst.Y : pQ2Presentation.Induction.FramedPair.fstSigma.fst.{u, v} {α : Type u} {β : α → Type v} (self : Sigma β) : αThe first component of a dependent pair.
.YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. ),
      ((Q2Presentation.Lifting.conjFamilyQ2Presentation.Lifting.conjFamily {Yt : Q2Presentation.BoundaryFramedTarget}
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) :
  Q2Presentation.Lifting.OperatorFamily Yt (Q2Presentation.Lifting.NAdd E)The concrete conjugation family of an elementary kernel. 
                  (Q2Presentation.Induction.mstageKernelQ2Presentation.Induction.mstageKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1) : Q2Presentation.Lifting.ElementaryKernel p.fst**The mstage consumer kernel**, bundled for the cocycle bridge. 
                    chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1)).opQ2Presentation.Lifting.OperatorFamily.op {Yt : Q2Presentation.BoundaryFramedTarget} {V : Type} [AddCommGroup V]
  [Module (ZMod 2) V] (self : Q2Presentation.Lifting.OperatorFamily Yt V) : Yt.Y → Module.End (ZMod 2) V
              yp.fst.Y)
            wQ2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR) -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).
          wQ2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR) ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
        WSubmodule (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR)))
  (hwWw ∉ W : wQ2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR) ∉ WSubmodule (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR))) :
  ∃ nQ2Presentation.Gen → Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR),
    Q2Presentation.Lifting.foxShadowGenQ2Presentation.Lifting.foxShadowGen {Yt : Q2Presentation.BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V]
  [Module (ZMod 2) V] (Φ : Yt.Y → Module.End (ZMod 2) V) (q : Q2Presentation.Marking Yt.Y)
  (n : Q2Presentation.Gen → V) : Q2Presentation.GExpr → VThe shadow recursion over an abstract operator family. 
            (Q2Presentation.Lifting.conjFamilyQ2Presentation.Lifting.conjFamily {Yt : Q2Presentation.BoundaryFramedTarget}
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) :
  Q2Presentation.Lifting.OperatorFamily Yt (Q2Presentation.Lifting.NAdd E)The concrete conjugation family of an elementary kernel. 
                (Q2Presentation.Induction.mstageKernelQ2Presentation.Induction.mstageKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1) : Q2Presentation.Lifting.ElementaryKernel p.fst**The mstage consumer kernel**, bundled for the cocycle bridge. 
                  chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1)).opQ2Presentation.Lifting.OperatorFamily.op {Yt : Q2Presentation.BoundaryFramedTarget} {V : Type} [AddCommGroup V]
  [Module (ZMod 2) V] (self : Q2Presentation.Lifting.OperatorFamily Yt V) : Yt.Y → Module.End (ZMod 2) V
            qQ2Presentation.Marking p.fst.Y nQ2Presentation.Gen → Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR)
            Q2Presentation.Q2Word.tameRelatorQ2Presentation.Q2Word.tameRelator : Q2Presentation.GExprThe tame relator `τ^σ · (τ²)⁻¹` (the relation `τ^σ = τ²`).  -HSub.hSub.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HSub α β γ] : α → β → γ`a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator).
          wQ2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR) ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
        WSubmodule (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR)) ∧And (a b : Prop) : Prop`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.

 * The recommended spelling of `/\` in identifiers is `and` (prefer `∧` over `/\`).
      Q2Presentation.Lifting.foxShadowGenQ2Presentation.Lifting.foxShadowGen {Yt : Q2Presentation.BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V]
  [Module (ZMod 2) V] (Φ : Yt.Y → Module.End (ZMod 2) V) (q : Q2Presentation.Marking Yt.Y)
  (n : Q2Presentation.Gen → V) : Q2Presentation.GExpr → VThe shadow recursion over an abstract operator family. 
          (Q2Presentation.Lifting.conjFamilyQ2Presentation.Lifting.conjFamily {Yt : Q2Presentation.BoundaryFramedTarget}
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) :
  Q2Presentation.Lifting.OperatorFamily Yt (Q2Presentation.Lifting.NAdd E)The concrete conjugation family of an elementary kernel. 
              (Q2Presentation.Induction.mstageKernelQ2Presentation.Induction.mstageKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (hR : Nat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1) : Q2Presentation.Lifting.ElementaryKernel p.fst**The mstage consumer kernel**, bundled for the cocycle bridge. 
                chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor hRNat.card ↥(Q2Presentation.Induction.kernelFrattini K) = 1)).opQ2Presentation.Lifting.OperatorFamily.op {Yt : Q2Presentation.BoundaryFramedTarget} {V : Type} [AddCommGroup V]
  [Module (ZMod 2) V] (self : Q2Presentation.Lifting.OperatorFamily Yt V) : Yt.Y → Module.End (ZMod 2) V
          qQ2Presentation.Marking p.fst.Y nQ2Presentation.Gen → Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR)
          Q2Presentation.Q2Word.wildRelatorQ2Presentation.Q2Word.wildRelator : Q2Presentation.GExprThe wild relator `h₀ · u₁⁻¹ · x₁^σ · c₀` (the relation `h₀ u₁⁻¹ x₁^σ c₀ = 1`).  ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
        WSubmodule (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.mstageKernel chief K hR))

theorem Q2Presentation.Induction.towerDualInv_zero
  {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|`. }
  {chiefQ2Presentation.Induction.NonScalarChiefFactor p :
    Q2Presentation.Induction.NonScalarChiefFactorQ2Presentation.Induction.NonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA concrete non-scalar chief factor in the marked wild kernel `L_Y`.

This is the Lean form of the Section 7 entry point: choose `S triangleleft P <= L_Y`
with `P/S` the first non-scalar simple factor.  Here the existing project predicate
`ChiefFactorInLY` supplies the chief-factor condition, and `not ChiefFactorTrivial`
records non-scalarity. 
      pQ2Presentation.Induction.FramedPair}
  (KQ2Presentation.Induction.KernelMinimal chief :
    Q2Presentation.Induction.KernelMinimalQ2Presentation.Induction.KernelMinimal {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : TypeThe manuscript's kernel choice (l.3623): `K ◁ Y`, `K ≤ P`, `KS = P`, and `K` is
**⊆-minimal** with these properties — stated as: any `Y`-normal `K' ≤ K` still joining
with `S` to `P` equals `K`.  (This, not leastness among all candidates, is what
`lem:simplehead` and `lem:collapse` use: both apply it to subgroups of `K`.) 
      chiefQ2Presentation.Induction.NonScalarChiefFactor p)
  (φModule.Dual (ZMod 2) (Q2Presentation.Induction.towerM K) :
    Module.DualModule.Dual.{u_4, u_5} (R : Type u_4) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] : Type (max u_5 u_4)The left dual space of an R-module M is the R-module of linear maps `M → R`.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2)
      (Q2Presentation.Induction.towerMQ2Presentation.Induction.towerM {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) : TypeThe additive elementary module layer `M = K/Φ(K)` (`lem:simplehead`).  KQ2Presentation.Induction.KernelMinimal chief))
  (hinv∀ (c : Q2Presentation.Induction.towerC K), φ ∘ₗ ↑((Q2Presentation.Induction.towerActM K) c) = φ :
    ∀
      (cQ2Presentation.Induction.towerC K :
        Q2Presentation.Induction.towerCQ2Presentation.Induction.towerC {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) : TypeThe lower target `C = Y/K` (`eq:targettower`). 
          KQ2Presentation.Induction.KernelMinimal chief),
      φModule.Dual (ZMod 2) (Q2Presentation.Induction.towerM K) ∘ₗLinearMap.comp.{u_2, u_3, u_4, u_9, u_10, u_11} {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9}
  {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂]
  [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) :
  M₁ →ₛₗ[σ₁₃] M₃Composition of two linear maps is a linear map 
          ↑((Q2Presentation.Induction.towerActMQ2Presentation.Induction.towerActM {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) :
  Q2Presentation.Induction.towerC K →* Q2Presentation.Induction.towerM K ≃ₗ[ZMod 2] Q2Presentation.Induction.towerM KThe conjugation action of the lower target `C = Y/K` on the additive module
`M = K/Φ(K)`, as `ZMod 2`-linear equivalences — the manuscript's `𝔽₂[C]`-module
structure on `M` (`lem:simplehead`), fully constructed. 
                KQ2Presentation.Induction.KernelMinimal chief)
              cQ2Presentation.Induction.towerC K) =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`.
        φModule.Dual (ZMod 2) (Q2Presentation.Induction.towerM K)) :
  φModule.Dual (ZMod 2) (Q2Presentation.Induction.towerM K) =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`. 0

theorem Q2Presentation.Induction.Section7KernelRoute180Closers.rawSimpleHeadActualData_from_route180Pieces
  {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|`. }
  {chiefQ2Presentation.Induction.NonScalarChiefFactor p :
    Q2Presentation.Induction.NonScalarChiefFactorQ2Presentation.Induction.NonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA concrete non-scalar chief factor in the marked wild kernel `L_Y`.

This is the Lean form of the Section 7 entry point: choose `S triangleleft P <= L_Y`
with `P/S` the first non-scalar simple factor.  Here the existing project predicate
`ChiefFactorInLY` supplies the chief-factor condition, and `not ChiefFactorTrivial`
records non-scalarity. 
      pQ2Presentation.Induction.FramedPair}
  (DQ2Presentation.Induction.MinimalBlockRawTowerData p chief :
    Q2Presentation.Induction.MinimalBlockRawTowerDataQ2Presentation.Induction.MinimalBlockRawTowerData (p : Q2Presentation.Induction.FramedPair)
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : Type 1The raw module-level quotient tower supplied by the Section 7 choice of the
minimal normal subgroup `K`.

This deliberately stops before the simple-head representation input, determinant
characters, and pushouts.  It records only the finite `F_2` modules
`R = Phi(K)`, `M = K/R`, the submodule `T`, the quotient group `C = Y/K`, the two
actions, and stability of `T`. 
      pQ2Presentation.Induction.FramedPair chiefQ2Presentation.Induction.NonScalarChiefFactor p) :
  NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.

    (Q2Presentation.Induction.Section7KernelRoute143RawActualClosers.RawSimpleHeadActualDataQ2Presentation.Induction.Section7KernelRoute143RawActualClosers.RawSimpleHeadActualData
  {p : Q2Presentation.Induction.FramedPair} {chief : Q2Presentation.Induction.NonScalarChiefFactor p}
  (D : Q2Presentation.Induction.MinimalBlockRawTowerData p chief) : PropRoute143 raw simple-head packet on one selected raw tower. 
      DQ2Presentation.Induction.MinimalBlockRawTowerData p chief)

theorem Q2Presentation.Induction.sec7_stable_submodule_dichotomy
  {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|`. }
  (chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p :
    Q2Presentation.Induction.FirstNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA non-scalar chief factor of `L_Y` that is **first**: every chief factor strictly
below it (i.e. with upper term contained in `lower`) is scalar.  This is the manuscript's
choice `S ◁ P` at l.3616–3623 ("all chief factors below `S` are scalar and `V` is the
first non-scalar simple factor"), which `lem:collapse` requires for the coprime step
`[S, Ñ] = 1`. 
      pQ2Presentation.Induction.FramedPair)
  (KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor :
    Q2Presentation.Induction.KernelMinimalQ2Presentation.Induction.KernelMinimal {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : TypeThe manuscript's kernel choice (l.3623): `K ◁ Y`, `K ≤ P`, `KS = P`, and `K` is
**⊆-minimal** with these properties — stated as: any `Y`-normal `K' ≤ K` still joining
with `S` to `P` equals `K`.  (This, not leastness among all candidates, is what
`lem:simplehead` and `lem:collapse` use: both apply it to subgroups of `K`.) 
      chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p.toNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor.toNonScalarChiefFactor {p : Q2Presentation.Induction.FramedPair}
  (self : Q2Presentation.Induction.FirstNonScalarChiefFactor p) : Q2Presentation.Induction.NonScalarChiefFactor p)
  (WSubmodule (ZMod 2) (Q2Presentation.Induction.towerM K) :
    SubmoduleSubmodule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type vA submodule of a module is one which is closed under vector operations.
This is a sufficient condition for the subset of vectors in the submodule
to themselves form a module.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2)
      (Q2Presentation.Induction.towerMQ2Presentation.Induction.towerM {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) : TypeThe additive elementary module layer `M = K/Φ(K)` (`lem:simplehead`).  KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor))
  (hstable∀ (c : Q2Presentation.Induction.towerC K), ∀ m ∈ W, ((Q2Presentation.Induction.towerActM K) c) m ∈ W :
    ∀
      (cQ2Presentation.Induction.towerC K :
        Q2Presentation.Induction.towerCQ2Presentation.Induction.towerC {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) : TypeThe lower target `C = Y/K` (`eq:targettower`). 
          KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor),
      ∀ mQ2Presentation.Induction.towerM K ∈ WSubmodule (ZMod 2) (Q2Presentation.Induction.towerM K),
        ((Q2Presentation.Induction.towerActMQ2Presentation.Induction.towerActM {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) :
  Q2Presentation.Induction.towerC K →* Q2Presentation.Induction.towerM K ≃ₗ[ZMod 2] Q2Presentation.Induction.towerM KThe conjugation action of the lower target `C = Y/K` on the additive module
`M = K/Φ(K)`, as `ZMod 2`-linear equivalences — the manuscript's `𝔽₂[C]`-module
structure on `M` (`lem:simplehead`), fully constructed. 
                KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
              cQ2Presentation.Induction.towerC K)
            mQ2Presentation.Induction.towerM K ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
          WSubmodule (ZMod 2) (Q2Presentation.Induction.towerM K))
  (hTWQ2Presentation.Induction.towerT K ≤ W :
    Q2Presentation.Induction.towerTQ2Presentation.Induction.towerT {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) :
  Submodule (ZMod 2) (Q2Presentation.Induction.towerM K)The manuscript's radical layer `T = (K ∩ S)/R ◁ M` (l.3628), as a
`ZMod 2`-submodule of the additive module `M`.  KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`).
      WSubmodule (ZMod 2) (Q2Presentation.Induction.towerM K)) :
  WSubmodule (ZMod 2) (Q2Presentation.Induction.towerM K) =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.towerTQ2Presentation.Induction.towerT {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) :
  Submodule (ZMod 2) (Q2Presentation.Induction.towerM K)The manuscript's radical layer `T = (K ∩ S)/R ◁ M` (l.3628), as a
`ZMod 2`-submodule of the additive module `M`.  KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor ∨Or (a b : Prop) : Prop`Or a b`, or `a ∨ b`, is the disjunction of propositions. There are two
constructors for `Or`, called `Or.inl : a → a ∨ b` and `Or.inr : b → a ∨ b`,
and you can use `match` or `cases` to destruct an `Or` assumption into the
two cases.


Conventions for notations in identifiers:

 * The recommended spelling of `∨` in identifiers is `or`.

 * The recommended spelling of `\/` in identifiers is `or` (prefer `∨` over `\/`).
    WSubmodule (ZMod 2) (Q2Presentation.Induction.towerM K) =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`.

theorem Induction3EShearBuild.Vq_stable_bot_or_top
  {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|`. }
  (chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p :
    Q2Presentation.Induction.FirstNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA non-scalar chief factor of `L_Y` that is **first**: every chief factor strictly
below it (i.e. with upper term contained in `lower`) is scalar.  This is the manuscript's
choice `S ◁ P` at l.3616–3623 ("all chief factors below `S` are scalar and `V` is the
first non-scalar simple factor"), which `lem:collapse` requires for the coprime step
`[S, Ñ] = 1`. 
      pQ2Presentation.Induction.FramedPair)
  (KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor :
    Q2Presentation.Induction.KernelMinimalQ2Presentation.Induction.KernelMinimal {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : TypeThe manuscript's kernel choice (l.3623): `K ◁ Y`, `K ≤ P`, `KS = P`, and `K` is
**⊆-minimal** with these properties — stated as: any `Y`-normal `K' ≤ K` still joining
with `S` to `P` equals `K`.  (This, not leastness among all candidates, is what
`lem:simplehead` and `lem:collapse` use: both apply it to subgroups of `K`.) 
      chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p.toNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor.toNonScalarChiefFactor {p : Q2Presentation.Induction.FramedPair}
  (self : Q2Presentation.Induction.FirstNonScalarChiefFactor p) : Q2Presentation.Induction.NonScalarChiefFactor p)
  (lamModule.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K) :
    Module.DualModule.Dual.{u_4, u_5} (R : Type u_4) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] : Type (max u_5 u_4)The left dual space of an R-module M is the R-module of linear maps `M → R`.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2)
      (Q2Presentation.Induction.towerRQ2Presentation.Induction.towerR {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) : TypeThe additive `R = Phi(K)` layer. 
        chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor))
  (hinv∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam :
    ∀
      (cQ2Presentation.Induction.towerC K :
        Q2Presentation.Induction.towerCQ2Presentation.Induction.towerC {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) : TypeThe lower target `C = Y/K` (`eq:targettower`). 
          KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor),
      lamModule.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K) ∘ₗLinearMap.comp.{u_2, u_3, u_4, u_9, u_10, u_11} {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9}
  {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂]
  [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) :
  M₁ →ₛₗ[σ₁₃] M₃Composition of two linear maps is a linear map 
          ↑((Q2Presentation.Induction.towerActRQ2Presentation.Induction.towerActR {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) :
  Q2Presentation.Induction.towerC K →*
    Q2Presentation.Induction.towerR chief K ≃ₗ[ZMod 2] Q2Presentation.Induction.towerR chief KThe conjugation action of `C = Y/K` on `R = Phi(K)`. 
                chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
              cQ2Presentation.Induction.towerC K) =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`.
        lamModule.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K))
  (USubmodule (ZMod 2) (Induction3BShear.Vq chief K lam hinv) :
    SubmoduleSubmodule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type vA submodule of a module is one which is closed under vector operations.
This is a sufficient condition for the subset of vectors in the submodule
to themselves form a module.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2)
      (Induction3BShear.VqInduction3BShear.Vq {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K))
  (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) :
  TypeThe head `V̄ = M̄/T̄`.  chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor lamModule.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)
        hinv∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam))
  (hstab∀ (c : Q2Presentation.Induction.towerC K), ∀ v ∈ U, (Induction3BShear.actVq chief K lam hinv c) v ∈ U :
    ∀
      (cQ2Presentation.Induction.towerC K :
        Q2Presentation.Induction.towerCQ2Presentation.Induction.towerC {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) : TypeThe lower target `C = Y/K` (`eq:targettower`). 
          KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor),
      ∀ vInduction3BShear.Vq chief K lam hinv ∈ USubmodule (ZMod 2) (Induction3BShear.Vq chief K lam hinv),
        (Induction3BShear.actVqInduction3BShear.actVq {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K))
  (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam)
  (c : Q2Presentation.Induction.towerC K) :
  Induction3BShear.Vq chief K lam hinv ≃ₗ[ZMod 2] Induction3BShear.Vq chief K lam hinvThe head action.  chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor
              lamModule.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K) hinv∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam cQ2Presentation.Induction.towerC K)
            vInduction3BShear.Vq chief K lam hinv ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`.
          USubmodule (ZMod 2) (Induction3BShear.Vq chief K lam hinv)) :
  USubmodule (ZMod 2) (Induction3BShear.Vq chief K lam hinv) =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`. ⊥Bot.bot.{u_1} {α : Type u_1} [self : Bot α] : αThe bot (`⊥`, `\bot`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊥` in identifiers is `bot`. ∨Or (a b : Prop) : Prop`Or a b`, or `a ∨ b`, is the disjunction of propositions. There are two
constructors for `Or`, called `Or.inl : a → a ∨ b` and `Or.inr : b → a ∨ b`,
and you can use `match` or `cases` to destruct an `Or` assumption into the
two cases.


Conventions for notations in identifiers:

 * The recommended spelling of `∨` in identifiers is `or`.

 * The recommended spelling of `\/` in identifiers is `or` (prefer `∨` over `\/`). USubmodule (ZMod 2) (Induction3BShear.Vq chief K lam hinv) =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`.

theorem Q2Presentation.Induction.head_nontrivial
  {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|`. }
  {chiefQ2Presentation.Induction.NonScalarChiefFactor p :
    Q2Presentation.Induction.NonScalarChiefFactorQ2Presentation.Induction.NonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA concrete non-scalar chief factor in the marked wild kernel `L_Y`.

This is the Lean form of the Section 7 entry point: choose `S triangleleft P <= L_Y`
with `P/S` the first non-scalar simple factor.  Here the existing project predicate
`ChiefFactorInLY` supplies the chief-factor condition, and `not ChiefFactorTrivial`
records non-scalarity. 
      pQ2Presentation.Induction.FramedPair}
  (KQ2Presentation.Induction.KernelMinimal chief :
    Q2Presentation.Induction.KernelMinimalQ2Presentation.Induction.KernelMinimal {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : TypeThe manuscript's kernel choice (l.3623): `K ◁ Y`, `K ≤ P`, `KS = P`, and `K` is
**⊆-minimal** with these properties — stated as: any `Y`-normal `K' ≤ K` still joining
with `S` to `P` equals `K`.  (This, not leastness among all candidates, is what
`lem:simplehead` and `lem:collapse` use: both apply it to subgroups of `K`.) 
      chiefQ2Presentation.Induction.NonScalarChiefFactor p) :
  NontrivialNontrivial.{u_3} (α : Type u_3) : PropPredicate typeclass for expressing that a type is not reduced to a single element. In rings,
this is equivalent to `0 ≠ 1`. In vector spaces, this is equivalent to positive dimension. 
    (HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.
Q2Presentation.Induction.towerMQ2Presentation.Induction.towerM {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) : TypeThe additive elementary module layer `M = K/Φ(K)` (`lem:simplehead`).  KQ2Presentation.Induction.KernelMinimal chief ⧸HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.

      Q2Presentation.Induction.towerTQ2Presentation.Induction.towerT {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) :
  Submodule (ZMod 2) (Q2Presentation.Induction.towerM K)The manuscript's radical layer `T = (K ∩ S)/R ◁ M` (l.3628), as a
`ZMod 2`-submodule of the additive module `M`.  KQ2Presentation.Induction.KernelMinimal chief)HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.

theorem Q2Presentation.Induction.headInv_eq_zero
  {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|`. }
  (chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p :
    Q2Presentation.Induction.FirstNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA non-scalar chief factor of `L_Y` that is **first**: every chief factor strictly
below it (i.e. with upper term contained in `lower`) is scalar.  This is the manuscript's
choice `S ◁ P` at l.3616–3623 ("all chief factors below `S` are scalar and `V` is the
first non-scalar simple factor"), which `lem:collapse` requires for the coprime step
`[S, Ñ] = 1`. 
      pQ2Presentation.Induction.FramedPair)
  (KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor :
    Q2Presentation.Induction.KernelMinimalQ2Presentation.Induction.KernelMinimal {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : TypeThe manuscript's kernel choice (l.3623): `K ◁ Y`, `K ≤ P`, `KS = P`, and `K` is
**⊆-minimal** with these properties — stated as: any `Y`-normal `K' ≤ K` still joining
with `S` to `P` equals `K`.  (This, not leastness among all candidates, is what
`lem:simplehead` and `lem:collapse` use: both apply it to subgroups of `K`.) 
      chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p.toNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor.toNonScalarChiefFactor {p : Q2Presentation.Induction.FramedPair}
  (self : Q2Presentation.Induction.FirstNonScalarChiefFactor p) : Q2Presentation.Induction.NonScalarChiefFactor p)
  (vQ2Presentation.Induction.towerM K ⧸ Q2Presentation.Induction.towerT K :
    Q2Presentation.Induction.towerMQ2Presentation.Induction.towerM {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) : TypeThe additive elementary module layer `M = K/Φ(K)` (`lem:simplehead`).  KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor ⧸HasQuotient.Quotient.{u, v} (A : outParam (Type u)) {B : Type v} [self : HasQuotient A B] : B → Type (max u v)`HasQuotient.Quotient A b` (denoted as `A ⧸ b`) is the quotient of the type `A` by `b`.

This differs from `HasQuotient.quotient'` in that the `A` argument is explicit,
which is necessary to make Lean show the notation in the goal state.

      Q2Presentation.Induction.towerTQ2Presentation.Induction.towerT {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) :
  Submodule (ZMod 2) (Q2Presentation.Induction.towerM K)The manuscript's radical layer `T = (K ∩ S)/R ◁ M` (l.3628), as a
`ZMod 2`-submodule of the additive module `M`.  KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (hv∀ (c : Q2Presentation.Induction.towerC K), (Q2Presentation.Induction.headActE chief K c) v = v :
    ∀
      (cQ2Presentation.Induction.towerC K :
        Q2Presentation.Induction.towerCQ2Presentation.Induction.towerC {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) : TypeThe lower target `C = Y/K` (`eq:targettower`). 
          KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor),
      (Q2Presentation.Induction.headActEQ2Presentation.Induction.headActE {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (c : Q2Presentation.Induction.towerC K) :
  Q2Presentation.Induction.towerM K ⧸ Q2Presentation.Induction.towerT K →ₗ[ZMod 2]
    Q2Presentation.Induction.towerM K ⧸ Q2Presentation.Induction.towerT KThe descended `C`-action on the head `V = M/T` (`towerActM` mod the
stable radical layer, via `Submodule.mapQ`). 
            chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor cQ2Presentation.Induction.towerC K)
          vQ2Presentation.Induction.towerM K ⧸ Q2Presentation.Induction.towerT K =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`.
        vQ2Presentation.Induction.towerM K ⧸ Q2Presentation.Induction.towerT K) :
  vQ2Presentation.Induction.towerM K ⧸ Q2Presentation.Induction.towerT K =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`. 0

theorem Q2Presentation.Induction.minimalBlock_kernelConcreteRoute24Data_from_finerPackets
  {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|`. }
  (chiefQ2Presentation.Induction.NonScalarChiefFactor p :
    Q2Presentation.Induction.NonScalarChiefFactorQ2Presentation.Induction.NonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA concrete non-scalar chief factor in the marked wild kernel `L_Y`.

This is the Lean form of the Section 7 entry point: choose `S triangleleft P <= L_Y`
with `P/S` the first non-scalar simple factor.  Here the existing project predicate
`ChiefFactorInLY` supplies the chief-factor condition, and `not ChiefFactorTrivial`
records non-scalarity. 
      pQ2Presentation.Induction.FramedPair) :
  NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.

    (Q2Presentation.Induction.MinimalBlockKernelConcreteRoute24DataQ2Presentation.Induction.MinimalBlockKernelConcreteRoute24Data {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : Type 1Route24 coherent Section 7 kernel/head packet.

Compared with Route23, the fourth field records the actual invariant packet on
the selected raw tower. The Route12 semantic head/invariant packet is then
derived theorem-level by `headInvariantOfInvariantActual`.

      chiefQ2Presentation.Induction.NonScalarChiefFactor p)

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute44.frattiniData_from_route44Collapse
  {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|`. }
  {chiefQ2Presentation.Induction.NonScalarChiefFactor p :
    Q2Presentation.Induction.NonScalarChiefFactorQ2Presentation.Induction.NonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA concrete non-scalar chief factor in the marked wild kernel `L_Y`.

This is the Lean form of the Section 7 entry point: choose `S triangleleft P <= L_Y`
with `P/S` the first non-scalar simple factor.  Here the existing project predicate
`ChiefFactorInLY` supplies the chief-factor condition, and `not ChiefFactorTrivial`
records non-scalarity. 
      pQ2Presentation.Induction.FramedPair}
  (KQ2Presentation.Induction.MinimalBlockKernelLeastOverChiefData chief :
    Q2Presentation.Induction.MinimalBlockKernelLeastOverChiefDataQ2Presentation.Induction.MinimalBlockKernelLeastOverChiefData {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : TypeNarrow kernel-choice packet: a least candidate over the selected chief factor.

The current downstream semantic packet asks for this leastness as
`Ksub <= K'` for every other candidate `K'`.  That is stronger than mere
finite-poset minimality, so it is kept as the finite-group choice content rather
than hidden behind a false finite-minimization proof. 
      chiefQ2Presentation.Induction.NonScalarChiefFactor p) :
  NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.

    (Q2Presentation.Induction.MinimalBlockKernelModuleConcreteFrattiniDataQ2Presentation.Induction.MinimalBlockKernelModuleConcreteFrattiniData {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p}
  (K : Q2Presentation.Induction.MinimalBlockKernelLeastOverChiefData chief) : PropManuscript `lem:collapse` for the literal Frattini subgroup of the chosen
least kernel `K`.

Compared with `MinimalBlockFrattiniCollapseData`, this keeps the actual collapse
facts that were present in the aggregate packet: centrality in `K`, `K^4 = 1`,
and exponent two on `Phi(K)`. 
      KQ2Presentation.Induction.MinimalBlockKernelLeastOverChiefData chief)

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute45.frattiniData_from_route45Split
  {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|`. }
  {chiefQ2Presentation.Induction.NonScalarChiefFactor p :
    Q2Presentation.Induction.NonScalarChiefFactorQ2Presentation.Induction.NonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA concrete non-scalar chief factor in the marked wild kernel `L_Y`.

This is the Lean form of the Section 7 entry point: choose `S triangleleft P <= L_Y`
with `P/S` the first non-scalar simple factor.  Here the existing project predicate
`ChiefFactorInLY` supplies the chief-factor condition, and `not ChiefFactorTrivial`
records non-scalarity. 
      pQ2Presentation.Induction.FramedPair}
  (KQ2Presentation.Induction.MinimalBlockKernelLeastOverChiefData chief :
    Q2Presentation.Induction.MinimalBlockKernelLeastOverChiefDataQ2Presentation.Induction.MinimalBlockKernelLeastOverChiefData {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : TypeNarrow kernel-choice packet: a least candidate over the selected chief factor.

The current downstream semantic packet asks for this leastness as
`Ksub <= K'` for every other candidate `K'`.  That is stronger than mere
finite-poset minimality, so it is kept as the finite-group choice content rather
than hidden behind a false finite-minimization proof. 
      chiefQ2Presentation.Induction.NonScalarChiefFactor p) :
  NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.

    (Q2Presentation.Induction.MinimalBlockKernelModuleConcreteFrattiniDataQ2Presentation.Induction.MinimalBlockKernelModuleConcreteFrattiniData {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p}
  (K : Q2Presentation.Induction.MinimalBlockKernelLeastOverChiefData chief) : PropManuscript `lem:collapse` for the literal Frattini subgroup of the chosen
least kernel `K`.

Compared with `MinimalBlockFrattiniCollapseData`, this keeps the actual collapse
facts that were present in the aggregate packet: centrality in `K`, `K^4 = 1`,
and exponent two on `Phi(K)`. 
      KQ2Presentation.Induction.MinimalBlockKernelLeastOverChiefData chief)

theorem Q2Presentation.Induction.MinimalBlockKernelRoute106FrattiniClosers.frattiniData_from_route106Coherent
  {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|`. }
  {chiefQ2Presentation.Induction.NonScalarChiefFactor p :
    Q2Presentation.Induction.NonScalarChiefFactorQ2Presentation.Induction.NonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA concrete non-scalar chief factor in the marked wild kernel `L_Y`.

This is the Lean form of the Section 7 entry point: choose `S triangleleft P <= L_Y`
with `P/S` the first non-scalar simple factor.  Here the existing project predicate
`ChiefFactorInLY` supplies the chief-factor condition, and `not ChiefFactorTrivial`
records non-scalarity. 
      pQ2Presentation.Induction.FramedPair}
  (KQ2Presentation.Induction.MinimalBlockKernelLeastOverChiefData chief :
    Q2Presentation.Induction.MinimalBlockKernelLeastOverChiefDataQ2Presentation.Induction.MinimalBlockKernelLeastOverChiefData {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : TypeNarrow kernel-choice packet: a least candidate over the selected chief factor.

The current downstream semantic packet asks for this leastness as
`Ksub <= K'` for every other candidate `K'`.  That is stronger than mere
finite-poset minimality, so it is kept as the finite-group choice content rather
than hidden behind a false finite-minimization proof. 
      chiefQ2Presentation.Induction.NonScalarChiefFactor p) :
  NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.

    (Q2Presentation.Induction.MinimalBlockKernelModuleConcreteFrattiniDataQ2Presentation.Induction.MinimalBlockKernelModuleConcreteFrattiniData {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p}
  (K : Q2Presentation.Induction.MinimalBlockKernelLeastOverChiefData chief) : PropManuscript `lem:collapse` for the literal Frattini subgroup of the chosen
least kernel `K`.

Compared with `MinimalBlockFrattiniCollapseData`, this keeps the actual collapse
facts that were present in the aggregate packet: centrality in `K`, `K^4 = 1`,
and exponent two on `Phi(K)`. 
      KQ2Presentation.Induction.MinimalBlockKernelLeastOverChiefData chief)

theorem Q2Presentation.Induction.MinimalBlockKernelRoute90Closers.frattiniCentralizerCollapseSectionData_from_route90
  {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|`. }
  {chiefQ2Presentation.Induction.NonScalarChiefFactor p :
    Q2Presentation.Induction.NonScalarChiefFactorQ2Presentation.Induction.NonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA concrete non-scalar chief factor in the marked wild kernel `L_Y`.

This is the Lean form of the Section 7 entry point: choose `S triangleleft P <= L_Y`
with `P/S` the first non-scalar simple factor.  Here the existing project predicate
`ChiefFactorInLY` supplies the chief-factor condition, and `not ChiefFactorTrivial`
records non-scalarity. 
      pQ2Presentation.Induction.FramedPair}
  (KQ2Presentation.Induction.MinimalBlockKernelLeastOverChiefData chief :
    Q2Presentation.Induction.MinimalBlockKernelLeastOverChiefDataQ2Presentation.Induction.MinimalBlockKernelLeastOverChiefData {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : TypeNarrow kernel-choice packet: a least candidate over the selected chief factor.

The current downstream semantic packet asks for this leastness as
`Ksub <= K'` for every other candidate `K'`.  That is stronger than mere
finite-poset minimality, so it is kept as the finite-group choice content rather
than hidden behind a false finite-minimization proof. 
      chiefQ2Presentation.Induction.NonScalarChiefFactor p) :
  NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.

    (Q2Presentation.Induction.MinimalBlockKernelRoute85Closers.FrattiniCentralizerCollapseSectionDataQ2Presentation.Induction.MinimalBlockKernelRoute85Closers.FrattiniCentralizerCollapseSectionData
  {p : Q2Presentation.Induction.FramedPair} {chief : Q2Presentation.Induction.NonScalarChiefFactor p}
  (K : Q2Presentation.Induction.MinimalBlockKernelLeastOverChiefData chief) : TypeRoute85 manuscript-shaped Frattini--centralizer collapse packet.

The fields are the selected pieces needed by the existing Route78/Route63
conversion API, but they are owned by one selected `K`, following
`lem:collapse` rather than the Route81 atomization.

      KQ2Presentation.Induction.MinimalBlockKernelLeastOverChiefData chief)

theorem Q2Presentation.Induction.kernelFrattini_le_lower
  {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|`. }
  {chiefQ2Presentation.Induction.NonScalarChiefFactor p :
    Q2Presentation.Induction.NonScalarChiefFactorQ2Presentation.Induction.NonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA concrete non-scalar chief factor in the marked wild kernel `L_Y`.

This is the Lean form of the Section 7 entry point: choose `S triangleleft P <= L_Y`
with `P/S` the first non-scalar simple factor.  Here the existing project predicate
`ChiefFactorInLY` supplies the chief-factor condition, and `not ChiefFactorTrivial`
records non-scalarity. 
      pQ2Presentation.Induction.FramedPair}
  (KQ2Presentation.Induction.KernelMinimal chief :
    Q2Presentation.Induction.KernelMinimalQ2Presentation.Induction.KernelMinimal {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : TypeThe manuscript's kernel choice (l.3623): `K ◁ Y`, `K ≤ P`, `KS = P`, and `K` is
**⊆-minimal** with these properties — stated as: any `Y`-normal `K' ≤ K` still joining
with `S` to `P` equals `K`.  (This, not leastness among all candidates, is what
`lem:simplehead` and `lem:collapse` use: both apply it to subgroups of `K`.) 
      chiefQ2Presentation.Induction.NonScalarChiefFactor p) :
  Q2Presentation.Induction.kernelFrattiniQ2Presentation.Induction.kernelFrattini {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) :
  Subgroup p.fst.YThe literal Frattini subgroup `R = Φ(K)` of the kernel, as a subgroup of `Y`
(the manuscript's `R`, l.3626). 
      KQ2Presentation.Induction.KernelMinimal chief ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`).
    chiefQ2Presentation.Induction.NonScalarChiefFactor p.lowerQ2Presentation.Induction.NonScalarChiefFactor.lower {p : Q2Presentation.Induction.FramedPair}
  (self : Q2Presentation.Induction.NonScalarChiefFactor p) : Subgroup p.fst.Y

theorem Q2Presentation.Induction.kernel_commutator_frattini_eq_bot
  {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|`. }
  (chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p :
    Q2Presentation.Induction.FirstNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor (p : Q2Presentation.Induction.FramedPair) : TypeA non-scalar chief factor of `L_Y` that is **first**: every chief factor strictly
below it (i.e. with upper term contained in `lower`) is scalar.  This is the manuscript's
choice `S ◁ P` at l.3616–3623 ("all chief factors below `S` are scalar and `V` is the
first non-scalar simple factor"), which `lem:collapse` requires for the coprime step
`[S, Ñ] = 1`. 
      pQ2Presentation.Induction.FramedPair)
  (KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor :
    Q2Presentation.Induction.KernelMinimalQ2Presentation.Induction.KernelMinimal {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.NonScalarChiefFactor p) : TypeThe manuscript's kernel choice (l.3623): `K ◁ Y`, `K ≤ P`, `KS = P`, and `K` is
**⊆-minimal** with these properties — stated as: any `Y`-normal `K' ≤ K` still joining
with `S` to `P` equals `K`.  (This, not leastness among all candidates, is what
`lem:simplehead` and `lem:collapse` use: both apply it to subgroups of `K`.) 
      chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p.toNonScalarChiefFactorQ2Presentation.Induction.FirstNonScalarChiefFactor.toNonScalarChiefFactor {p : Q2Presentation.Induction.FramedPair}
  (self : Q2Presentation.Induction.FirstNonScalarChiefFactor p) : Q2Presentation.Induction.NonScalarChiefFactor p) :
  ⁅Bracket.bracket.{u_1, u_2} {L : Type u_1} {M : Type u_2} [self : Bracket L M] : L → M → M`⁅x, y⁆` is the result of a bracket operation on elements `x` and `y`.
It is supported by the `Bracket` typeclass. KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor.KsubQ2Presentation.Induction.KernelMinimal.Ksub {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (self : Q2Presentation.Induction.KernelMinimal chief) :
  Subgroup p.fst.Y,Bracket.bracket.{u_1, u_2} {L : Type u_1} {M : Type u_2} [self : Bracket L M] : L → M → M`⁅x, y⁆` is the result of a bracket operation on elements `x` and `y`.
It is supported by the `Bracket` typeclass. 
      Q2Presentation.Induction.kernelFrattiniQ2Presentation.Induction.kernelFrattini {p : Q2Presentation.Induction.FramedPair}
  {chief : Q2Presentation.Induction.NonScalarChiefFactor p} (K : Q2Presentation.Induction.KernelMinimal chief) :
  Subgroup p.fst.YThe literal Frattini subgroup `R = Φ(K)` of the kernel, as a subgroup of `Y`
(the manuscript's `R`, l.3626). 
        KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor⁆Bracket.bracket.{u_1, u_2} {L : Type u_1} {M : Type u_2} [self : Bracket L M] : L → M → M`⁅x, y⁆` is the result of a bracket operation on elements `x` and `y`.
It is supported by the `Bracket` typeclass.  =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`.
    ⊥Bot.bot.{u_1} {α : Type u_1} [self : Bot α] : αThe bot (`⊥`, `\bot`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊥` in identifiers is `bot`.