theorem Q2Presentation.Induction.centralCover_candidateRLiftSemanticData
  {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|`. }
  (BQ2Presentation.Induction.MinimalBlock p :
    Q2Presentation.Induction.MinimalBlockQ2Presentation.Induction.MinimalBlock (p : Q2Presentation.Induction.FramedPair) : Type 1**The §7 minimal non-scalar block.**  Source-uniform module-level data of the
manuscript tower (`eq:targettower`), with the deep group/representation inputs of
`lem:simplehead`/`lem:collapse`/`prop:simpleheaddet` isolated as documented fields. 
      pQ2Presentation.Induction.FramedPair)
  (TQ2Presentation.Induction.CentralCoverElementaryQuotientTowerData B :
    Q2Presentation.Induction.CentralCoverElementaryQuotientTowerDataQ2Presentation.Induction.CentralCoverElementaryQuotientTowerData {p : Q2Presentation.Induction.FramedPair}
  (B : Q2Presentation.Induction.MinimalBlock p) : Type 1A realized elementary quotient tower for `eq:targettower`.

This is the missing target-side finite group datum behind the lower term in
`eq:Mstage`: the middle quotient `B = Y/R`, the lower quotient `C = Y/K`, and the
map `B -> C`.  The cardinal equations record the two quotient steps in a form
that proves strict decrease.

The current `MinimalBlock` supplies the abstract modules, but not this realized
quotient tower. 
      BQ2Presentation.Induction.MinimalBlock 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.CentralCoverCandidateRLiftSemanticDataQ2Presentation.Induction.CentralCoverCandidateRLiftSemanticData {p : Q2Presentation.Induction.FramedPair}
  (B : Q2Presentation.Induction.MinimalBlock p)
  (T : Q2Presentation.Induction.CentralCoverElementaryQuotientTowerData B) : Type 1Semantic candidate-side final `R`-lift packet.

The exact-image partition used by the recursion is not merely an abstract
cardinality equivalence.  In the manuscript it comes from the central
`R = Phi(K)` cover over the realized quotient tower
`Y -> B = Y/R -> C = Y/K`, the obstruction map of `lem:covertransform`, the
affine lift equation of `lem:affinelifting`, and the Frattini-surjectivity
argument in `prop:finalfourier`.

The packet is now split into the four manuscript-facing pieces above: exact-image
base quotient, obstruction-index-to-base map, affine fibre torsor, and Frattini
exact-image surjectivity. 
      BQ2Presentation.Induction.MinimalBlock p TQ2Presentation.Induction.CentralCoverElementaryQuotientTowerData B)

theorem Q2Presentation.Induction.cover_Z1_card_gq2
  {YtQ2Presentation.BoundaryFramedTarget :
    Q2Presentation.BoundaryFramedTargetQ2Presentation.BoundaryFramedTarget : Type 1A **boundary-framed marked target** `𝒴 = (Y, L_Y, π_Y, θ_Y)` (manuscript
Definition 4.1, `def:framed`): a finite group `Y` with a normal finite `2`-subgroup
`L_Y`, a surjection `π_Y : Y ↠ H` onto a finite *tame* quotient with kernel exactly
`L_Y`, and an *elementary decoration* `θ_Y : Y → Multiplicative E` into the
multiplicative image of a finite `𝔽₂`-vector space `E`.  The pair
`q_Y = (π_Y, θ_Y)` fixes both the tame quotient `Y / L_Y ≅ H` and the decoration. }
  [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 YtQ2Presentation.BoundaryFramedTarget.YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. ]
  (EQ2Presentation.Lifting.ElementaryKernel Yt :
    Q2Presentation.Lifting.ElementaryKernelQ2Presentation.Lifting.ElementaryKernel (Yt : Q2Presentation.BoundaryFramedTarget) : TypeA normal subgroup of a framed target that is killed by the decoration,
contained in the wild kernel, **abelian**, and of **exponent 2** — the shape
of the chief kernels the cochain keeps quantify over. 
      YtQ2Presentation.BoundaryFramedTarget)
  (FQ2Presentation.BoundaryFrame Yt : Q2Presentation.BoundaryFrameQ2Presentation.BoundaryFrame (Yt : Q2Presentation.BoundaryFramedTarget) : TypeA **boundary frame** on a boundary-framed target `𝒴` (manuscript `eq:beta`):
the fixed compatible data `α : 𝕋_tame ↠ H`, `ψ : Π → Multiplicative E`, and the
induced `β : ∂_bd → H × Multiplicative E`.  Surjectivity of `α` records that `H`
really is a tame quotient (manuscript: "Fix a finite tame quotient `H`, an
epimorphism `α : 𝕋_A ↠ H`").  YtQ2Presentation.BoundaryFramedTarget)
  (hcardNat.card (Q2Presentation.Lifting.NAdd E) = 2 :
    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.Lifting.NAddQ2Presentation.Lifting.NAdd {Yt : Q2Presentation.BoundaryFramedTarget}
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) : TypeThe additive `F₂`-carrier of an elementary kernel.  EQ2Presentation.Lifting.ElementaryKernel Yt) =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`.
      2)
  (gQ2Presentation.boundaryFramedSurj Q2Presentation.boundaryPackage_GQ2
  (Q2Presentation.TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯)
  (Q2Presentation.TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F) :
    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_GQ2Q2Presentation.boundaryPackage_GQ2 : Q2Presentation.BoundaryPackage Q2Presentation.GQ2Profinite**The local boundary package** `boundaryPackage_GQ2 : BoundaryPackage G_{ℚ₂}`
(manuscript Prop 3.14 `prop:compatiblemarking` for `Γ = G_{ℚ₂}`; plan Turn 4 §6),
the `G_{ℚ₂}`-side instance of the uniform Stage-C boundary datum.

* `tameMap`/`tame_surj`/`tame_nu` — the local tame quotient `G_{ℚ₂} ↠ T_A` with
  unramified marking `ν_loc`, from the axiom `gq2_tame_quotient` (Prop 3.2 + the
  local half of Prop `compatiblemarking`);
* `pro2Map`/`pro2_surj`/`pro2_nu` — the local maximal pro-`2` quotient
  `G_{ℚ₂} ↠ Π` with the *same* unramified marking `ν_loc`, proved from the fully
  marked Labute comparison `labute_GQ2_maxPro2_marked` (`pro2Map_loc`,
  `pro2Map_loc_surjective`, `pro2Map_loc_nu`);
* `nu := ν_loc` — the common unramified character 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). 
        YtQ2Presentation.BoundaryFramedTarget EQ2Presentation.Lifting.ElementaryKernel Yt.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). 
        YtQ2Presentation.BoundaryFramedTarget EQ2Presentation.Lifting.ElementaryKernel Yt.NQ2Presentation.Lifting.ElementaryKernel.N {Yt : Q2Presentation.BoundaryFramedTarget}
  (self : Q2Presentation.Lifting.ElementaryKernel Yt) : Subgroup Yt.Y ⋯ ⋯ FQ2Presentation.BoundaryFrame Yt))
  (f₀Q2Presentation.TorsorProgram.liftHom Yt E.N ⋯ ⋯ Q2Presentation.boundaryPackage_GQ2 F g :
    Q2Presentation.TorsorProgram.liftHomQ2Presentation.TorsorProgram.liftHom (Yt : Q2Presentation.BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal]
  (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : Q2Presentation.BoundaryPackage Γ)
  (F : Q2Presentation.BoundaryFrame Yt)
  (g :
    Q2Presentation.boundaryFramedSurj B (Q2Presentation.TorsorProgram.quotientFramedTarget Yt N hNLY hNθ)
      (Q2Presentation.TorsorProgram.quotientFrame Yt N hNLY hNθ F)) :
  Type**All framed lifts** of a child-framed surjection (surjectivity NOT imposed;
the Frattini argument recovers it per use-site). 
      YtQ2Presentation.BoundaryFramedTarget EQ2Presentation.Lifting.ElementaryKernel Yt.NQ2Presentation.Lifting.ElementaryKernel.N {Yt : Q2Presentation.BoundaryFramedTarget}
  (self : Q2Presentation.Lifting.ElementaryKernel Yt) : Subgroup Yt.Y ⋯ ⋯
      Q2Presentation.boundaryPackage_GQ2Q2Presentation.boundaryPackage_GQ2 : Q2Presentation.BoundaryPackage Q2Presentation.GQ2Profinite**The local boundary package** `boundaryPackage_GQ2 : BoundaryPackage G_{ℚ₂}`
(manuscript Prop 3.14 `prop:compatiblemarking` for `Γ = G_{ℚ₂}`; plan Turn 4 §6),
the `G_{ℚ₂}`-side instance of the uniform Stage-C boundary datum.

* `tameMap`/`tame_surj`/`tame_nu` — the local tame quotient `G_{ℚ₂} ↠ T_A` with
  unramified marking `ν_loc`, from the axiom `gq2_tame_quotient` (Prop 3.2 + the
  local half of Prop `compatiblemarking`);
* `pro2Map`/`pro2_surj`/`pro2_nu` — the local maximal pro-`2` quotient
  `G_{ℚ₂} ↠ Π` with the *same* unramified marking `ν_loc`, proved from the fully
  marked Labute comparison `labute_GQ2_maxPro2_marked` (`pro2Map_loc`,
  `pro2Map_loc_surjective`, `pro2Map_loc_nu`);
* `nu := ν_loc` — the common unramified character through which both factor.  FQ2Presentation.BoundaryFrame Yt
      gQ2Presentation.boundaryFramedSurj Q2Presentation.boundaryPackage_GQ2
  (Q2Presentation.TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯)
  (Q2Presentation.TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) :
  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.TorsorProgram.Z1Q2Presentation.TorsorProgram.Z1 (Yt : Q2Presentation.BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal]
  (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : Q2Presentation.BoundaryPackage Γ)
  (F : Q2Presentation.BoundaryFrame Yt)
  (g :
    Q2Presentation.boundaryFramedSurj B (Q2Presentation.TorsorProgram.quotientFramedTarget Yt N hNLY hNθ)
      (Q2Presentation.TorsorProgram.quotientFrame Yt N hNLY hNθ F))
  (f₀ : Q2Presentation.TorsorProgram.liftHom Yt N hNLY hNθ B F g) : Type**The twisted cocycle set** relative to a base lift.  YtQ2Presentation.BoundaryFramedTarget
        EQ2Presentation.Lifting.ElementaryKernel Yt.NQ2Presentation.Lifting.ElementaryKernel.N {Yt : Q2Presentation.BoundaryFramedTarget}
  (self : Q2Presentation.Lifting.ElementaryKernel Yt) : Subgroup Yt.Y ⋯ ⋯
        Q2Presentation.boundaryPackage_GQ2Q2Presentation.boundaryPackage_GQ2 : Q2Presentation.BoundaryPackage Q2Presentation.GQ2Profinite**The local boundary package** `boundaryPackage_GQ2 : BoundaryPackage G_{ℚ₂}`
(manuscript Prop 3.14 `prop:compatiblemarking` for `Γ = G_{ℚ₂}`; plan Turn 4 §6),
the `G_{ℚ₂}`-side instance of the uniform Stage-C boundary datum.

* `tameMap`/`tame_surj`/`tame_nu` — the local tame quotient `G_{ℚ₂} ↠ T_A` with
  unramified marking `ν_loc`, from the axiom `gq2_tame_quotient` (Prop 3.2 + the
  local half of Prop `compatiblemarking`);
* `pro2Map`/`pro2_surj`/`pro2_nu` — the local maximal pro-`2` quotient
  `G_{ℚ₂} ↠ Π` with the *same* unramified marking `ν_loc`, proved from the fully
  marked Labute comparison `labute_GQ2_maxPro2_marked` (`pro2Map_loc`,
  `pro2Map_loc_surjective`, `pro2Map_loc_nu`);
* `nu := ν_loc` — the common unramified character through which both factor. 
        FQ2Presentation.BoundaryFrame Yt gQ2Presentation.boundaryFramedSurj Q2Presentation.boundaryPackage_GQ2
  (Q2Presentation.TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯)
  (Q2Presentation.TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F) f₀Q2Presentation.TorsorProgram.liftHom Yt E.N ⋯ ⋯ Q2Presentation.boundaryPackage_GQ2 F g) =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`.
    8

theorem Q2Presentation.Lifting.cover_Z1_card_gammaA
  {YtQ2Presentation.BoundaryFramedTarget :
    Q2Presentation.BoundaryFramedTargetQ2Presentation.BoundaryFramedTarget : Type 1A **boundary-framed marked target** `𝒴 = (Y, L_Y, π_Y, θ_Y)` (manuscript
Definition 4.1, `def:framed`): a finite group `Y` with a normal finite `2`-subgroup
`L_Y`, a surjection `π_Y : Y ↠ H` onto a finite *tame* quotient with kernel exactly
`L_Y`, and an *elementary decoration* `θ_Y : Y → Multiplicative E` into the
multiplicative image of a finite `𝔽₂`-vector space `E`.  The pair
`q_Y = (π_Y, θ_Y)` fixes both the tame quotient `Y / L_Y ≅ H` and the decoration. }
  [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 YtQ2Presentation.BoundaryFramedTarget.YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. ]
  (EQ2Presentation.Lifting.ElementaryKernel Yt :
    Q2Presentation.Lifting.ElementaryKernelQ2Presentation.Lifting.ElementaryKernel (Yt : Q2Presentation.BoundaryFramedTarget) : TypeA normal subgroup of a framed target that is killed by the decoration,
contained in the wild kernel, **abelian**, and of **exponent 2** — the shape
of the chief kernels the cochain keeps quantify over. 
      YtQ2Presentation.BoundaryFramedTarget)
  (hcardNat.card (Q2Presentation.Lifting.NAdd E) = 2 :
    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.Lifting.NAddQ2Presentation.Lifting.NAdd {Yt : Q2Presentation.BoundaryFramedTarget}
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) : TypeThe additive `F₂`-carrier of an elementary kernel.  EQ2Presentation.Lifting.ElementaryKernel Yt) =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`.
      2)
  (FQ2Presentation.BoundaryFrame Yt : Q2Presentation.BoundaryFrameQ2Presentation.BoundaryFrame (Yt : Q2Presentation.BoundaryFramedTarget) : TypeA **boundary frame** on a boundary-framed target `𝒴` (manuscript `eq:beta`):
the fixed compatible data `α : 𝕋_tame ↠ H`, `ψ : Π → Multiplicative E`, and the
induced `β : ∂_bd → H × Multiplicative E`.  Surjectivity of `α` records that `H`
really is a tame quotient (manuscript: "Fix a finite tame quotient `H`, an
epimorphism `α : 𝕋_A ↠ H`").  YtQ2Presentation.BoundaryFramedTarget)
  (gQ2Presentation.boundaryFramedSurj Q2Presentation.boundaryPackage_GammaA
  (Q2Presentation.TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯)
  (Q2Presentation.TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F) :
    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). 
        YtQ2Presentation.BoundaryFramedTarget EQ2Presentation.Lifting.ElementaryKernel Yt.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). 
        YtQ2Presentation.BoundaryFramedTarget EQ2Presentation.Lifting.ElementaryKernel Yt.NQ2Presentation.Lifting.ElementaryKernel.N {Yt : Q2Presentation.BoundaryFramedTarget}
  (self : Q2Presentation.Lifting.ElementaryKernel Yt) : Subgroup Yt.Y ⋯ ⋯ FQ2Presentation.BoundaryFrame Yt))
  (f₀Q2Presentation.TorsorProgram.liftHom Yt E.N ⋯ ⋯ Q2Presentation.boundaryPackage_GammaA F g :
    Q2Presentation.TorsorProgram.liftHomQ2Presentation.TorsorProgram.liftHom (Yt : Q2Presentation.BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal]
  (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : Q2Presentation.BoundaryPackage Γ)
  (F : Q2Presentation.BoundaryFrame Yt)
  (g :
    Q2Presentation.boundaryFramedSurj B (Q2Presentation.TorsorProgram.quotientFramedTarget Yt N hNLY hNθ)
      (Q2Presentation.TorsorProgram.quotientFrame Yt N hNLY hNθ F)) :
  Type**All framed lifts** of a child-framed surjection (surjectivity NOT imposed;
the Frattini argument recovers it per use-site). 
      YtQ2Presentation.BoundaryFramedTarget EQ2Presentation.Lifting.ElementaryKernel Yt.NQ2Presentation.Lifting.ElementaryKernel.N {Yt : Q2Presentation.BoundaryFramedTarget}
  (self : Q2Presentation.Lifting.ElementaryKernel Yt) : Subgroup Yt.Y ⋯ ⋯
      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. 
      FQ2Presentation.BoundaryFrame Yt gQ2Presentation.boundaryFramedSurj Q2Presentation.boundaryPackage_GammaA
  (Q2Presentation.TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯)
  (Q2Presentation.TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) :
  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.TorsorProgram.Z1Q2Presentation.TorsorProgram.Z1 (Yt : Q2Presentation.BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal]
  (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : Q2Presentation.BoundaryPackage Γ)
  (F : Q2Presentation.BoundaryFrame Yt)
  (g :
    Q2Presentation.boundaryFramedSurj B (Q2Presentation.TorsorProgram.quotientFramedTarget Yt N hNLY hNθ)
      (Q2Presentation.TorsorProgram.quotientFrame Yt N hNLY hNθ F))
  (f₀ : Q2Presentation.TorsorProgram.liftHom Yt N hNLY hNθ B F g) : Type**The twisted cocycle set** relative to a base lift.  YtQ2Presentation.BoundaryFramedTarget
        EQ2Presentation.Lifting.ElementaryKernel Yt.NQ2Presentation.Lifting.ElementaryKernel.N {Yt : Q2Presentation.BoundaryFramedTarget}
  (self : Q2Presentation.Lifting.ElementaryKernel Yt) : Subgroup Yt.Y ⋯ ⋯
        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. 
        FQ2Presentation.BoundaryFrame Yt gQ2Presentation.boundaryFramedSurj Q2Presentation.boundaryPackage_GammaA
  (Q2Presentation.TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯)
  (Q2Presentation.TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F) f₀Q2Presentation.TorsorProgram.liftHom Yt E.N ⋯ ⋯ Q2Presentation.boundaryPackage_GammaA F g) =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`.
    8

theorem Q2Presentation.Lifting.scalarCover_Z1_card
  {YtQ2Presentation.BoundaryFramedTarget :
    Q2Presentation.BoundaryFramedTargetQ2Presentation.BoundaryFramedTarget : Type 1A **boundary-framed marked target** `𝒴 = (Y, L_Y, π_Y, θ_Y)` (manuscript
Definition 4.1, `def:framed`): a finite group `Y` with a normal finite `2`-subgroup
`L_Y`, a surjection `π_Y : Y ↠ H` onto a finite *tame* quotient with kernel exactly
`L_Y`, and an *elementary decoration* `θ_Y : Y → Multiplicative E` into the
multiplicative image of a finite `𝔽₂`-vector space `E`.  The pair
`q_Y = (π_Y, θ_Y)` fixes both the tame quotient `Y / L_Y ≅ H` and the decoration. }
  [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 YtQ2Presentation.BoundaryFramedTarget.YQ2Presentation.BoundaryFramedTarget.Y (self : Q2Presentation.BoundaryFramedTarget) : TypeThe finite target group `Y`. ]
  (EQ2Presentation.Lifting.ElementaryKernel Yt :
    Q2Presentation.Lifting.ElementaryKernelQ2Presentation.Lifting.ElementaryKernel (Yt : Q2Presentation.BoundaryFramedTarget) : TypeA normal subgroup of a framed target that is killed by the decoration,
contained in the wild kernel, **abelian**, and of **exponent 2** — the shape
of the chief kernels the cochain keeps quantify over. 
      YtQ2Presentation.BoundaryFramedTarget)
  (FQ2Presentation.BoundaryFrame Yt : Q2Presentation.BoundaryFrameQ2Presentation.BoundaryFrame (Yt : Q2Presentation.BoundaryFramedTarget) : TypeA **boundary frame** on a boundary-framed target `𝒴` (manuscript `eq:beta`):
the fixed compatible data `α : 𝕋_tame ↠ H`, `ψ : Π → Multiplicative E`, and the
induced `β : ∂_bd → H × Multiplicative E`.  Surjectivity of `α` records that `H`
really is a tame quotient (manuscript: "Fix a finite tame quotient `H`, an
epimorphism `α : 𝕋_A ↠ H`").  YtQ2Presentation.BoundaryFramedTarget)
  (gQ2Presentation.boundaryFramedSurj Q2Presentation.boundaryPackage_GammaA
  (Q2Presentation.TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯)
  (Q2Presentation.TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F) :
    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). 
        YtQ2Presentation.BoundaryFramedTarget EQ2Presentation.Lifting.ElementaryKernel Yt.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). 
        YtQ2Presentation.BoundaryFramedTarget EQ2Presentation.Lifting.ElementaryKernel Yt.NQ2Presentation.Lifting.ElementaryKernel.N {Yt : Q2Presentation.BoundaryFramedTarget}
  (self : Q2Presentation.Lifting.ElementaryKernel Yt) : Subgroup Yt.Y ⋯ ⋯ FQ2Presentation.BoundaryFrame Yt))
  (lamModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd E) :
    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.  EQ2Presentation.Lifting.ElementaryKernel Yt))
  (hinvlam ∈ Q2Presentation.Lifting.conjInvDuals E :
    lamModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd E) ∈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`.
      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). 
        EQ2Presentation.Lifting.ElementaryKernel Yt)
  (hnelam ≠ 0 : lamModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd E) ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. 0)
  (f₀Q2Presentation.Lifting.scalarCoverLiftHom E lam hinv Q2Presentation.boundaryPackage_GammaA F g :
    Q2Presentation.Lifting.scalarCoverLiftHomQ2Presentation.Lifting.scalarCoverLiftHom {Yt : Q2Presentation.BoundaryFramedTarget} [Finite Yt.Y]
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd E))
  (hinv : lam ∈ Q2Presentation.Lifting.conjInvDuals E) {Γ : ProfiniteGrp.{0}} (B : Q2Presentation.BoundaryPackage Γ)
  (F : Q2Presentation.BoundaryFrame Yt)
  (g :
    Q2Presentation.boundaryFramedSurj B (Q2Presentation.TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯)
      (Q2Presentation.TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) :
  Type**Cover lifts of `g`** (`lem:obstructionseparation` l.4219–4223):
framed homs `Γ ⟶ B_λ` over `g` — surjectivity NOT imposed (the
manuscript's compatible lifts: `λ_*o` measures weak liftability; images
are stratified by `eq:recursionR2`/`R3` later). 
      EQ2Presentation.Lifting.ElementaryKernel Yt lamModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd E) hinvlam ∈ Q2Presentation.Lifting.conjInvDuals 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. 
      FQ2Presentation.BoundaryFrame Yt gQ2Presentation.boundaryFramedSurj Q2Presentation.boundaryPackage_GammaA
  (Q2Presentation.TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯)
  (Q2Presentation.TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) :
  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.TorsorProgram.Z1Q2Presentation.TorsorProgram.Z1 (Yt : Q2Presentation.BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal]
  (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : Q2Presentation.BoundaryPackage Γ)
  (F : Q2Presentation.BoundaryFrame Yt)
  (g :
    Q2Presentation.boundaryFramedSurj B (Q2Presentation.TorsorProgram.quotientFramedTarget Yt N hNLY hNθ)
      (Q2Presentation.TorsorProgram.quotientFrame Yt N hNLY hNθ F))
  (f₀ : Q2Presentation.TorsorProgram.liftHom Yt N hNLY hNθ B F g) : Type**The twisted cocycle set** relative to a base lift. 
        (Q2Presentation.Lifting.scalarCoverTargetQ2Presentation.Lifting.scalarCoverTarget {Yt : Q2Presentation.BoundaryFramedTarget} [Finite Yt.Y]
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd E))
  (hinv : lam ∈ Q2Presentation.Lifting.conjInvDuals E) : Q2Presentation.BoundaryFramedTarget**The scalar pushout target** `B_λ = Y/ker λ` as a framed target
(same `H`, `E`, frame; `eq:targettower` refined by l.4219–4223). 
          EQ2Presentation.Lifting.ElementaryKernel Yt lamModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd E) hinvlam ∈ Q2Presentation.Lifting.conjInvDuals E)
        (Q2Presentation.Lifting.scalarRelKernelQ2Presentation.Lifting.scalarRelKernel {Yt : Q2Presentation.BoundaryFramedTarget} [Finite Yt.Y]
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd E))
  (hinv : lam ∈ Q2Presentation.Lifting.conjInvDuals E) :
  Q2Presentation.Lifting.ElementaryKernel (Q2Presentation.Lifting.scalarCoverTarget E lam hinv)**The relative kernel** `R/ker λ ≤ B_λ` — the deck kernel of the
central double cover, as an elementary kernel of the cover target.  It
is `Subgroup.map`-spelled so Noether III applies on the nose. 
            EQ2Presentation.Lifting.ElementaryKernel Yt lamModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd E) hinvlam ∈ Q2Presentation.Lifting.conjInvDuals E).NQ2Presentation.Lifting.ElementaryKernel.N {Yt : Q2Presentation.BoundaryFramedTarget}
  (self : Q2Presentation.Lifting.ElementaryKernel Yt) : Subgroup Yt.Y
        ⋯ ⋯
        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.Lifting.scalarCoverFrameQ2Presentation.Lifting.scalarCoverFrame {Yt : Q2Presentation.BoundaryFramedTarget} [Finite Yt.Y]
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd E))
  (hinv : lam ∈ Q2Presentation.Lifting.conjInvDuals E) (F : Q2Presentation.BoundaryFrame Yt) :
  Q2Presentation.BoundaryFrame (Q2Presentation.Lifting.scalarCoverTarget E lam hinv)The frame transports verbatim to the scalar pushout target. 
          EQ2Presentation.Lifting.ElementaryKernel Yt lamModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd E) hinvlam ∈ Q2Presentation.Lifting.conjInvDuals E FQ2Presentation.BoundaryFrame Yt)
        (Q2Presentation.Lifting.scalarCoverChildQ2Presentation.Lifting.scalarCoverChild {Yt : Q2Presentation.BoundaryFramedTarget} [Finite Yt.Y]
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd E))
  (hinv : lam ∈ Q2Presentation.Lifting.conjInvDuals E) {Γ : ProfiniteGrp.{0}} (B : Q2Presentation.BoundaryPackage Γ)
  (F : Q2Presentation.BoundaryFrame Yt)
  (g :
    Q2Presentation.boundaryFramedSurj B (Q2Presentation.TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯)
      (Q2Presentation.TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) :
  Q2Presentation.boundaryFramedSurj B
    (Q2Presentation.TorsorProgram.quotientFramedTarget (Q2Presentation.Lifting.scalarCoverTarget E lam hinv)
      (Q2Presentation.Lifting.scalarRelKernel E lam hinv).N ⋯ ⋯)
    (Q2Presentation.TorsorProgram.quotientFrame (Q2Presentation.Lifting.scalarCoverTarget E lam hinv)
      (Q2Presentation.Lifting.scalarRelKernel E lam hinv).N ⋯ ⋯ (Q2Presentation.Lifting.scalarCoverFrame E lam hinv F))**The child seen below the cover**: transport a child-framed
surjection across the collapse `(B_λ)/(R/ker λ) ≃* Y/R`. 
          EQ2Presentation.Lifting.ElementaryKernel Yt lamModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd E) hinvlam ∈ Q2Presentation.Lifting.conjInvDuals 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. 
          FQ2Presentation.BoundaryFrame Yt gQ2Presentation.boundaryFramedSurj Q2Presentation.boundaryPackage_GammaA
  (Q2Presentation.TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯)
  (Q2Presentation.TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F))
        f₀Q2Presentation.Lifting.scalarCoverLiftHom E lam hinv Q2Presentation.boundaryPackage_GammaA F g) =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`.
    8

theorem Q2Presentation.Induction.liftPartitionCardinality_of_liftPartition
  {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|`. }
  (BQ2Presentation.Induction.MinimalBlock p :
    Q2Presentation.Induction.MinimalBlockQ2Presentation.Induction.MinimalBlock (p : Q2Presentation.Induction.FramedPair) : Type 1**The §7 minimal non-scalar block.**  Source-uniform module-level data of the
manuscript tower (`eq:targettower`), with the deep group/representation inputs of
`lem:simplehead`/`lem:collapse`/`prop:simpleheaddet` isolated as documented fields. 
      pQ2Presentation.Induction.FramedPair)
  (SType : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. )
  (OQ2Presentation.Induction.CentralCoverSourceObstructionData B S :
    Q2Presentation.Induction.CentralCoverSourceObstructionDataQ2Presentation.Induction.CentralCoverSourceObstructionData {p : Q2Presentation.Induction.FramedPair}
  (B : Q2Presentation.Induction.MinimalBlock p) (S : Type) : Type 1Source-specific exact-image obstruction index and obstruction map.

Manuscript anchors: `def:Xgamma`, `lem:obstructionseparation`, and the
`o_R : X_Gamma(B) -> O_R` input to `prop:finalfourier`. 
      BQ2Presentation.Induction.MinimalBlock p SType)
  (ZQ2Presentation.Induction.CentralCoverSourceCocycleData B :
    Q2Presentation.Induction.CentralCoverSourceCocycleDataQ2Presentation.Induction.CentralCoverSourceCocycleData {p : Q2Presentation.Induction.FramedPair}
  (B : Q2Presentation.Induction.MinimalBlock p) : Type 1Source-specific `Z^1_Gamma(R)` group with the common size `z_R`.

Manuscript anchors: `lem:affinelifting`, `eq:mumultiplicity`, and the
source-interface lift-multiplicity comparison. 
      BQ2Presentation.Induction.MinimalBlock p)
  (FQ2Presentation.Induction.CentralCoverSourceLiftFibers B S O Z :
    Q2Presentation.Induction.CentralCoverSourceLiftFibersQ2Presentation.Induction.CentralCoverSourceLiftFibers {p : Q2Presentation.Induction.FramedPair}
  (B : Q2Presentation.Induction.MinimalBlock p) (S : Type)
  (O : Q2Presentation.Induction.CentralCoverSourceObstructionData B S)
  (Z : Q2Presentation.Induction.CentralCoverSourceCocycleData B) : Type 1Lift fibres over unobstructed points, before partitioning the global
boundary-framed surjection set.

Manuscript anchor: `lem:affinelifting`. 
      BQ2Presentation.Induction.MinimalBlock p SType OQ2Presentation.Induction.CentralCoverSourceObstructionData B S ZQ2Presentation.Induction.CentralCoverSourceCocycleData B)
  (PQ2Presentation.Induction.CentralCoverSourceLiftPartition B S O Z F :
    Q2Presentation.Induction.CentralCoverSourceLiftPartitionQ2Presentation.Induction.CentralCoverSourceLiftPartition {p : Q2Presentation.Induction.FramedPair}
  (B : Q2Presentation.Induction.MinimalBlock p) (S : Type)
  (O : Q2Presentation.Induction.CentralCoverSourceObstructionData B S)
  (Z : Q2Presentation.Induction.CentralCoverSourceCocycleData B)
  (F : Q2Presentation.Induction.CentralCoverSourceLiftFibers B S O Z) : TypeExact-image partition of the global surjection set by the unobstructed lift
fibres.

Manuscript anchors: `lem:covertransform` and `prop:finalfourier`, including
Frattini surjectivity of the final `R`-lifts. 
      BQ2Presentation.Induction.MinimalBlock p SType OQ2Presentation.Induction.CentralCoverSourceObstructionData B S ZQ2Presentation.Induction.CentralCoverSourceCocycleData B FQ2Presentation.Induction.CentralCoverSourceLiftFibers B S O Z) :
  Q2Presentation.Induction.CentralCoverSourceLiftPartitionCardinalityQ2Presentation.Induction.CentralCoverSourceLiftPartitionCardinality {p : Q2Presentation.Induction.FramedPair}
  (B : Q2Presentation.Induction.MinimalBlock p) (S : Type)
  (O : Q2Presentation.Induction.CentralCoverSourceObstructionData B S)
  (Z : Q2Presentation.Induction.CentralCoverSourceCocycleData B)
  (F : Q2Presentation.Induction.CentralCoverSourceLiftFibers B S O Z) : PropCardinal form of the exact-image lift partition.  This is the remaining
candidate finite bookkeeping statement: the actual maps and the disjoint union
of unobstructed lift fibres have the same finite cardinality. 
    BQ2Presentation.Induction.MinimalBlock p SType OQ2Presentation.Induction.CentralCoverSourceObstructionData B S ZQ2Presentation.Induction.CentralCoverSourceCocycleData B FQ2Presentation.Induction.CentralCoverSourceLiftFibers B S O Z

theorem Q2Presentation.Induction.sec7_scalarCoverPartition_gammaA
  {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.Lifting.NAdd (Q2Presentation.Induction.xrKernel 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.xrKernelQ2Presentation.Induction.xrKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) :
  Q2Presentation.Lifting.ElementaryKernel p.fst**The Frattini layer `R = Φ(K)` as an elementary kernel**
(`lem:collapse`): normal, inside `L_Y`, `θ`-dead, elementary abelian. 
          chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)))
  (hinvlam ∈ Q2Presentation.Lifting.conjInvDuals (Q2Presentation.Induction.xrKernel chief K) :
    lamModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.xrKernel chief 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`.
      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.xrKernelQ2Presentation.Induction.xrKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) :
  Q2Presentation.Lifting.ElementaryKernel p.fst**The Frattini layer `R = Φ(K)` as an elementary kernel**
(`lem:collapse`): normal, inside `L_Y`, `θ`-dead, elementary abelian. 
          chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor))
  (hnelam ≠ 0 : lamModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.xrKernel chief K)) ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. 0) :
  8 *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
      Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number.
If `α` is infinite, `Nat.card α = 0`. 
        {Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`. gQ2Presentation.boundaryFramedSurj Q2Presentation.boundaryPackage_GammaA
  (Q2Presentation.Induction.XRZero.xrChild chief K).fst (Q2Presentation.Induction.XRZero.xrChild chief K).snd //Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`.
          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.Lifting.scalarCoverLiftHomQ2Presentation.Lifting.scalarCoverLiftHom {Yt : Q2Presentation.BoundaryFramedTarget} [Finite Yt.Y]
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd E))
  (hinv : lam ∈ Q2Presentation.Lifting.conjInvDuals E) {Γ : ProfiniteGrp.{0}} (B : Q2Presentation.BoundaryPackage Γ)
  (F : Q2Presentation.BoundaryFrame Yt)
  (g :
    Q2Presentation.boundaryFramedSurj B (Q2Presentation.TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯)
      (Q2Presentation.TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) :
  Type**Cover lifts of `g`** (`lem:obstructionseparation` l.4219–4223):
framed homs `Γ ⟶ B_λ` over `g` — surjectivity NOT imposed (the
manuscript's compatible lifts: `λ_*o` measures weak liftability; images
are stratified by `eq:recursionR2`/`R3` later). 
              (Q2Presentation.Induction.xrKernelQ2Presentation.Induction.xrKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) :
  Q2Presentation.Lifting.ElementaryKernel p.fst**The Frattini layer `R = Φ(K)` as an elementary kernel**
(`lem:collapse`): normal, inside `L_Y`, `θ`-dead, elementary abelian. 
                chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
              lamModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.xrKernel chief K)) hinvlam ∈ Q2Presentation.Lifting.conjInvDuals (Q2Presentation.Induction.xrKernel chief K)
              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. 
              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.
 gQ2Presentation.boundaryFramedSurj Q2Presentation.boundaryPackage_GammaA
  (Q2Presentation.Induction.XRZero.xrChild chief K).fst (Q2Presentation.Induction.XRZero.xrChild chief K).snd) }Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`. =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`.
    ∑ JQ2Presentation.Induction.scalarCoverStrata chief K lam hinv,
      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.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.Induction.scalarCoverStratumPairQ2Presentation.Induction.scalarCoverStratumPair {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (lam : Module.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.xrKernel chief K)))
  (hinv : lam ∈ Q2Presentation.Lifting.conjInvDuals (Q2Presentation.Induction.xrKernel chief K))
  (J : Q2Presentation.Induction.scalarCoverStrata chief K lam hinv) : Q2Presentation.Induction.FramedPair**The stratum framed pair** `(J̃, J̃ ∩ L̃, π̃|_J̃, θ̃|_J̃; same frame)` —
an ordinary exact-image object in the same global boundary-framed category
(same `H`, same `E`, `p.2`'s frame verbatim), ready for the engine's children
lists.  Its measure is `|J̃ ∩ L̃|`, `lem:strictdecrease`'s quantity. 
              chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor lamModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.xrKernel chief K)) hinvlam ∈ Q2Presentation.Lifting.conjInvDuals (Q2Presentation.Induction.xrKernel chief K) JQ2Presentation.Induction.scalarCoverStrata chief K lam hinv).fstSigma.fst.{u, v} {α : Type u} {β : α → Type v} (self : Sigma β) : αThe first component of a dependent pair.

          (Q2Presentation.Induction.scalarCoverStratumPairQ2Presentation.Induction.scalarCoverStratumPair {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (lam : Module.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.xrKernel chief K)))
  (hinv : lam ∈ Q2Presentation.Lifting.conjInvDuals (Q2Presentation.Induction.xrKernel chief K))
  (J : Q2Presentation.Induction.scalarCoverStrata chief K lam hinv) : Q2Presentation.Induction.FramedPair**The stratum framed pair** `(J̃, J̃ ∩ L̃, π̃|_J̃, θ̃|_J̃; same frame)` —
an ordinary exact-image object in the same global boundary-framed category
(same `H`, same `E`, `p.2`'s frame verbatim), ready for the engine's children
lists.  Its measure is `|J̃ ∩ L̃|`, `lem:strictdecrease`'s quantity. 
              chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor lamModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.xrKernel chief K)) hinvlam ∈ Q2Presentation.Lifting.conjInvDuals (Q2Presentation.Induction.xrKernel chief K) JQ2Presentation.Induction.scalarCoverStrata chief K lam hinv).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.
)

theorem Q2Presentation.Induction.sec7_scalarCoverPartition_gq2
  {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.Lifting.NAdd (Q2Presentation.Induction.xrKernel 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.xrKernelQ2Presentation.Induction.xrKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) :
  Q2Presentation.Lifting.ElementaryKernel p.fst**The Frattini layer `R = Φ(K)` as an elementary kernel**
(`lem:collapse`): normal, inside `L_Y`, `θ`-dead, elementary abelian. 
          chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)))
  (hinvlam ∈ Q2Presentation.Lifting.conjInvDuals (Q2Presentation.Induction.xrKernel chief K) :
    lamModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.xrKernel chief 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`.
      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.xrKernelQ2Presentation.Induction.xrKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) :
  Q2Presentation.Lifting.ElementaryKernel p.fst**The Frattini layer `R = Φ(K)` as an elementary kernel**
(`lem:collapse`): normal, inside `L_Y`, `θ`-dead, elementary abelian. 
          chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor))
  (hnelam ≠ 0 : lamModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.xrKernel chief K)) ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. 0) :
  8 *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
      Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number.
If `α` is infinite, `Nat.card α = 0`. 
        {Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`. gQ2Presentation.boundaryFramedSurj Q2Presentation.boundaryPackage_GQ2
  (Q2Presentation.Induction.XRZero.xrChild chief K).fst (Q2Presentation.Induction.XRZero.xrChild chief K).snd //Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`.
          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.Lifting.scalarCoverLiftHomQ2Presentation.Lifting.scalarCoverLiftHom {Yt : Q2Presentation.BoundaryFramedTarget} [Finite Yt.Y]
  (E : Q2Presentation.Lifting.ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd E))
  (hinv : lam ∈ Q2Presentation.Lifting.conjInvDuals E) {Γ : ProfiniteGrp.{0}} (B : Q2Presentation.BoundaryPackage Γ)
  (F : Q2Presentation.BoundaryFrame Yt)
  (g :
    Q2Presentation.boundaryFramedSurj B (Q2Presentation.TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯)
      (Q2Presentation.TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) :
  Type**Cover lifts of `g`** (`lem:obstructionseparation` l.4219–4223):
framed homs `Γ ⟶ B_λ` over `g` — surjectivity NOT imposed (the
manuscript's compatible lifts: `λ_*o` measures weak liftability; images
are stratified by `eq:recursionR2`/`R3` later). 
              (Q2Presentation.Induction.xrKernelQ2Presentation.Induction.xrKernel {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) :
  Q2Presentation.Lifting.ElementaryKernel p.fst**The Frattini layer `R = Φ(K)` as an elementary kernel**
(`lem:collapse`): normal, inside `L_Y`, `θ`-dead, elementary abelian. 
                chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
              lamModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.xrKernel chief K)) hinvlam ∈ Q2Presentation.Lifting.conjInvDuals (Q2Presentation.Induction.xrKernel chief K)
              Q2Presentation.boundaryPackage_GQ2Q2Presentation.boundaryPackage_GQ2 : Q2Presentation.BoundaryPackage Q2Presentation.GQ2Profinite**The local boundary package** `boundaryPackage_GQ2 : BoundaryPackage G_{ℚ₂}`
(manuscript Prop 3.14 `prop:compatiblemarking` for `Γ = G_{ℚ₂}`; plan Turn 4 §6),
the `G_{ℚ₂}`-side instance of the uniform Stage-C boundary datum.

* `tameMap`/`tame_surj`/`tame_nu` — the local tame quotient `G_{ℚ₂} ↠ T_A` with
  unramified marking `ν_loc`, from the axiom `gq2_tame_quotient` (Prop 3.2 + the
  local half of Prop `compatiblemarking`);
* `pro2Map`/`pro2_surj`/`pro2_nu` — the local maximal pro-`2` quotient
  `G_{ℚ₂} ↠ Π` with the *same* unramified marking `ν_loc`, proved from the fully
  marked Labute comparison `labute_GQ2_maxPro2_marked` (`pro2Map_loc`,
  `pro2Map_loc_surjective`, `pro2Map_loc_nu`);
* `nu := ν_loc` — the common unramified character through which both factor. 
              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.
 gQ2Presentation.boundaryFramedSurj Q2Presentation.boundaryPackage_GQ2
  (Q2Presentation.Induction.XRZero.xrChild chief K).fst (Q2Presentation.Induction.XRZero.xrChild chief K).snd) }Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`. =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`.
    ∑ JQ2Presentation.Induction.scalarCoverStrata chief K lam hinv,
      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.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_GQ2Q2Presentation.boundaryPackage_GQ2 : Q2Presentation.BoundaryPackage Q2Presentation.GQ2Profinite**The local boundary package** `boundaryPackage_GQ2 : BoundaryPackage G_{ℚ₂}`
(manuscript Prop 3.14 `prop:compatiblemarking` for `Γ = G_{ℚ₂}`; plan Turn 4 §6),
the `G_{ℚ₂}`-side instance of the uniform Stage-C boundary datum.

* `tameMap`/`tame_surj`/`tame_nu` — the local tame quotient `G_{ℚ₂} ↠ T_A` with
  unramified marking `ν_loc`, from the axiom `gq2_tame_quotient` (Prop 3.2 + the
  local half of Prop `compatiblemarking`);
* `pro2Map`/`pro2_surj`/`pro2_nu` — the local maximal pro-`2` quotient
  `G_{ℚ₂} ↠ Π` with the *same* unramified marking `ν_loc`, proved from the fully
  marked Labute comparison `labute_GQ2_maxPro2_marked` (`pro2Map_loc`,
  `pro2Map_loc_surjective`, `pro2Map_loc_nu`);
* `nu := ν_loc` — the common unramified character through which both factor. 
          (Q2Presentation.Induction.scalarCoverStratumPairQ2Presentation.Induction.scalarCoverStratumPair {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (lam : Module.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.xrKernel chief K)))
  (hinv : lam ∈ Q2Presentation.Lifting.conjInvDuals (Q2Presentation.Induction.xrKernel chief K))
  (J : Q2Presentation.Induction.scalarCoverStrata chief K lam hinv) : Q2Presentation.Induction.FramedPair**The stratum framed pair** `(J̃, J̃ ∩ L̃, π̃|_J̃, θ̃|_J̃; same frame)` —
an ordinary exact-image object in the same global boundary-framed category
(same `H`, same `E`, `p.2`'s frame verbatim), ready for the engine's children
lists.  Its measure is `|J̃ ∩ L̃|`, `lem:strictdecrease`'s quantity. 
              chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor lamModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.xrKernel chief K)) hinvlam ∈ Q2Presentation.Lifting.conjInvDuals (Q2Presentation.Induction.xrKernel chief K) JQ2Presentation.Induction.scalarCoverStrata chief K lam hinv).fstSigma.fst.{u, v} {α : Type u} {β : α → Type v} (self : Sigma β) : αThe first component of a dependent pair.

          (Q2Presentation.Induction.scalarCoverStratumPairQ2Presentation.Induction.scalarCoverStratumPair {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor)
  (lam : Module.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.xrKernel chief K)))
  (hinv : lam ∈ Q2Presentation.Lifting.conjInvDuals (Q2Presentation.Induction.xrKernel chief K))
  (J : Q2Presentation.Induction.scalarCoverStrata chief K lam hinv) : Q2Presentation.Induction.FramedPair**The stratum framed pair** `(J̃, J̃ ∩ L̃, π̃|_J̃, θ̃|_J̃; same frame)` —
an ordinary exact-image object in the same global boundary-framed category
(same `H`, same `E`, `p.2`'s frame verbatim), ready for the engine's children
lists.  Its measure is `|J̃ ∩ L̃|`, `lem:strictdecrease`'s quantity. 
              chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor lamModule.Dual (ZMod 2) (Q2Presentation.Lifting.NAdd (Q2Presentation.Induction.xrKernel chief K)) hinvlam ∈ Q2Presentation.Lifting.conjInvDuals (Q2Presentation.Induction.xrKernel chief K) JQ2Presentation.Induction.scalarCoverStrata chief K lam hinv).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.
)

theorem Q2Presentation.Induction.Fourier.fourier_inversion.{u_1,
    u_2}
  {WType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  WType u_1]
  [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) WType u_1] [FintypeFintype.{u_4} (α : Type u_4) : Type u_4`Fintype α` means that `α` is finite, i.e. there are only
finitely many distinct elements of type `α`. The evidence of this
is a finset `elems` (a list up to permutation without duplicates),
together with a proof that everything of type `α` is in the list.  WType u_1]
  [DecidableEqDecidableEq.{u} (α : Sort u) : Sort (max 1 u)Propositional equality is `Decidable` for all elements of a type.

In other words, an instance of `DecidableEq α` is a means of deciding the proposition `a = b` is
for all `a b : α`.
 WType u_1] {XType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [FintypeFintype.{u_4} (α : Type u_4) : Type u_4`Fintype α` means that `α` is finite, i.e. there are only
finitely many distinct elements of type `α`. The evidence of this
is a finset `elems` (a list up to permutation without duplicates),
together with a proof that everything of type `α` is in the list.  XType u_2] (oX → W : XType u_2 → WType u_1) :
  ↑(Fintype.cardFintype.card.{u_4} (α : Type u_4) [Fintype α] : ℕ`card α` is the number of elements in `α`, defined when `α` is a fintype. 
          (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) WType u_1)) *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
      ↑(Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number.
If `α` is infinite, `Nat.card α = 0`.  {Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`. xX //Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`. oX → W xX =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 }Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`.) =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) W,
      (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).2 *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
          ↑(Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number.
If `α` is infinite, `Nat.card α = 0`. 
              {Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`. xX //Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`. χModule.Dual (ZMod 2) W (oX → W xX) =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 }Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`.) -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).
        ↑(Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number.
If `α` is infinite, `Nat.card α = 0`.  XType u_2))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).

theorem Q2Presentation.Quadratic.one_add_signChar
  (aZMod 2 : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) :
  1 +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.
      Q2Presentation.Quadratic.Dickson.signCharQ2Presentation.Quadratic.Dickson.signChar (a : ZMod 2) : ℤThe sign character `χ(0) = 1`, `χ(1) = -1`. 
        aZMod 2 =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`.
    ifite.{u} {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
 aZMod 2 =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 thenite.{u} {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
 2 elseite.{u} {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
 0

theorem Q2Presentation.Quadratic.sum_signChar_dual.{u_1}
  {EType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  EType u_1]
  [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) EType u_1]
  [FintypeFintype.{u_4} (α : Type u_4) : Type u_4`Fintype α` means that `α` is finite, i.e. there are only
finitely many distinct elements of type `α`. The evidence of this
is a finset `elems` (a list up to permutation without duplicates),
together with a proof that everything of type `α` is in the list.  (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) EType u_1)]
  (vE : EType u_1) :
  ∑ χModule.Dual (ZMod 2) E,
      Q2Presentation.Quadratic.Dickson.signCharQ2Presentation.Quadratic.Dickson.signChar (a : ZMod 2) : ℤThe sign character `χ(0) = 1`, `χ(1) = -1`. 
        (χModule.Dual (ZMod 2) E vE) =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`.
    ifite.{u} {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
 vE =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 thenite.{u} {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.

      ↑(Fintype.cardFintype.card.{u_4} (α : Type u_4) [Fintype α] : ℕ`card α` is the number of elements in `α`, defined when `α` is a fintype. 
          (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) EType u_1))
    elseite.{u} {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
 0

theorem Q2Presentation.Quadratic.QuadF2.polar_bijective.{u_1}
  {VType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  VType u_1]
  [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) VType u_1] [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 VType u_1]
  (qQ2Presentation.Quadratic.QuadF2 V : Q2Presentation.Quadratic.QuadF2Q2Presentation.Quadratic.QuadF2.{u_2} (V : Type u_2) [AddCommGroup V] [Module (ZMod 2) V] : Type u_2A **quadratic form over `F₂`** with its bilinear polar (commutator) form.  VType u_1)
  (hnsq.Nonsingular : qQ2Presentation.Quadratic.QuadF2 V.NonsingularQ2Presentation.Quadratic.QuadF2.Nonsingular.{u_1} {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V]
  (q : Q2Presentation.Quadratic.QuadF2 V) : Prop**Nonsingularity** (the polar form is nondegenerate / perfect): the only vector
pairing to `0` with everything is `0`.  For a nonzero invariant form on a simple
self-dual `V` this is automatic (`lem:zeropolar`, l.3452). ) :
  Function.BijectiveFunction.Bijective.{u₁, u₂} {α : Sort u₁} {β : Sort u₂} (f : α → β) : PropA function is called bijective if it is both injective and surjective.  ⇑qQ2Presentation.Quadratic.QuadF2 V.polarQ2Presentation.Quadratic.QuadF2.polar.{u_2} {V : Type u_2} [AddCommGroup V] [Module (ZMod 2) V]
  (self : Q2Presentation.Quadratic.QuadF2 V) : V →ₗ[ZMod 2] V →ₗ[ZMod 2] ZMod 2the bilinear polar form `b_q`, i.e. the commutator pairing 

theorem Q2Presentation.Quadratic.constrainedGauss_count.{u_1,
    u_2}
  {WType u_1 : Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. } {EType u_2 : Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. }
  [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  WType u_1] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) WType u_1]
  [FintypeFintype.{u_4} (α : Type u_4) : Type u_4`Fintype α` means that `α` is finite, i.e. there are only
finitely many distinct elements of type `α`. The evidence of this
is a finset `elems` (a list up to permutation without duplicates),
together with a proof that everything of type `α` is in the list.  WType u_1] [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.  EType u_2]
  [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring.
It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`,
connected by a "scalar multiplication" operation `r • x : M`
(where `r : R` and `x : M`) with some natural associativity and
distributivity axioms similar to those on a ring.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) EType u_2] [FiniteFinite.{u_3} (α : Sort u_3) : PropA type is `Finite` if it is in bijective correspondence to some `Fin n`.

This is similar to `Fintype`, but `Finite` is a proposition rather than data.
A particular benefit to this is that `Finite` instances are definitionally equal to one another
(due to proof irrelevance) rather than being merely propositionally equal,
and, furthermore, `Finite` instances generally avoid the need for `Decidable` instances.
One other notable difference is that `Finite` allows there to be `Finite p` instances
for all `p : Prop`, which is not allowed by `Fintype` due to universe constraints.
An application of this is that `Finite (x ∈ s → β x)` follows from the general instance for pi
types, assuming `[∀ x, Finite (β x)]`.
Implementation note: this is a reason `Finite α` is not defined as `Nonempty (Fintype α)`.

Every `Fintype` instance provides a `Finite` instance via `Finite.of_fintype`.
Conversely, one can noncomputably create a `Fintype` instance from a `Finite` instance
via `Fintype.ofFinite`. In a proof one might write
```lean
  have := Fintype.ofFinite α
```
to obtain such an instance.

Do not write noncomputable `Fintype` instances; instead write `Finite` instances
and use this `Fintype.ofFinite` interface.
The `Fintype` instances should be relied upon to be computable for evaluation purposes.

Theorems should use `Finite` instead of `Fintype`, unless definitions in the theorem statement
require `Fintype`.
Definitions should prefer `Finite` as well, unless it is important that the definitions
are meant to be computable in the reduction or `#eval` sense.
 EType u_2]
  [FintypeFintype.{u_4} (α : Type u_4) : Type u_4`Fintype α` means that `α` is finite, i.e. there are only
finitely many distinct elements of type `α`. The evidence of this
is a finset `elems` (a list up to permutation without duplicates),
together with a proof that everything of type `α` is in the list.  (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) EType u_2)]
  (LW →ₗ[ZMod 2] E : WType u_1 →ₗ[LinearMap.{u_14, u_15, u_16, u_17} {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] (σ : R →+* S)
  (M : Type u_16) (M₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] :
  Type (max u_16 u_17)A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S`
is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
`f (c • x) = (σ c) • f x`. Elements of `LinearMap σ M M₂` (available under the notation
`M →ₛₗ[σ] M₂`) are bundled versions of such maps. For plain linear maps (i.e. for which
`σ = RingHom.id R`), the notation `M →ₗ[R] M₂` is available. An unbundled version of plain linear
maps is available with the predicate `IsLinearMap`, but it should be avoided most of the time. ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2]LinearMap.{u_14, u_15, u_16, u_17} {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] (σ : R →+* S)
  (M : Type u_16) (M₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] :
  Type (max u_16 u_17)A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ : R →+* S`
is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
`f (c • x) = (σ c) • f x`. Elements of `LinearMap σ M M₂` (available under the notation
`M →ₛₗ[σ] M₂`) are bundled versions of such maps. For plain linear maps (i.e. for which
`σ = RingHom.id R`), the notation `M →ₗ[R] M₂` is available. An unbundled version of plain linear
maps is available with the predicate `IsLinearMap`, but it should be avoided most of the time.  EType u_2)
  (hLFunction.Surjective ⇑L : Function.SurjectiveFunction.Surjective.{u_1, u_2} {α : Sort u_1} {β : Sort u_2} (f : α → β) : PropA function `f : α → β` is called surjective if every `b : β` is equal to `f a`
for some `a : α`.  ⇑LW →ₗ[ZMod 2] E)
  (QQ2Presentation.Quadratic.QuadF2 W : Q2Presentation.Quadratic.QuadF2Q2Presentation.Quadratic.QuadF2.{u_2} (V : Type u_2) [AddCommGroup V] [Module (ZMod 2) V] : Type u_2A **quadratic form over `F₂`** with its bilinear polar (commutator) form.  WType u_1)
  (lModule.Dual (ZMod 2) W : 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) WType u_1)
  (AModule.Dual (ZMod 2) E → W : 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) EType u_2 → WType u_1)
  (hA∀ (χ : Module.Dual (ZMod 2) E) (x : W), (Q.polar (A χ)) x = χ (L x) + l x :
    ∀ (χModule.Dual (ZMod 2) E : 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) EType u_2)
      (xW : WType u_1),
      (QQ2Presentation.Quadratic.QuadF2 W.polarQ2Presentation.Quadratic.QuadF2.polar.{u_2} {V : Type u_2} [AddCommGroup V] [Module (ZMod 2) V]
  (self : Q2Presentation.Quadratic.QuadF2 V) : V →ₗ[ZMod 2] V →ₗ[ZMod 2] ZMod 2the bilinear polar form `b_q`, i.e. the commutator pairing  (AModule.Dual (ZMod 2) E → W χModule.Dual (ZMod 2) E)) xW =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) E (LW →ₗ[ZMod 2] E xW) +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. lModule.Dual (ZMod 2) W xW)
  (κE : EType u_2) (εZMod 2 : ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) :
  2 *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`. ↑(Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number.
If `α` is infinite, `Nat.card α = 0`.  EType u_2) *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
      ↑(Q2Presentation.Quadratic.constrainedZerosQ2Presentation.Quadratic.constrainedZeros.{u_1, u_2} {W : Type u_1} {E : Type u_2} [AddCommGroup W] [Module (ZMod 2) W]
  [AddCommGroup E] [Module (ZMod 2) E] (L : W →ₗ[ZMod 2] E) (Q : Q2Presentation.Quadratic.QuadF2 W)
  (l : Module.Dual (ZMod 2) W) (κ : E) (ε : ZMod 2) : ℕ`N(κ, ε)` — the **constrained count** of `lem:constrainedgauss` (l.3879–3882),
with an affine (linear-term) refinement: `#{x : L x = κ ∧ Q(x) + ℓ(x) = ε}`.
At `ℓ = 0` this is the manuscript's `N(κ,ε)`; the affine form is what
`prop:zeroedge` consumes through `eq:Qkappadifference` (the actual pushout form
`Q_κ` is base-plus-linear, its constant part being absorbed into `ε`). 
          LW →ₗ[ZMod 2] E QQ2Presentation.Quadratic.QuadF2 W lModule.Dual (ZMod 2) W κE εZMod 2) =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`.
    ↑(Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number.
If `α` is infinite, `Nat.card α = 0`.  WType u_1) +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.
      Q2Presentation.Quadratic.Dickson.gaussSumQ2Presentation.Quadratic.Dickson.gaussSum.{u_1} {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] [Fintype V]
  (q : Q2Presentation.Quadratic.QuadF2 V) : ℤThe **Gauss sum** `D(q) = ∑_v χ(q v)`. 
          QQ2Presentation.Quadratic.QuadF2 W *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
        ∑ χModule.Dual (ZMod 2) E,
          Q2Presentation.Quadratic.Dickson.signCharQ2Presentation.Quadratic.Dickson.signChar (a : ZMod 2) : ℤThe sign character `χ(0) = 1`, `χ(1) = -1`. 
            (HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.χModule.Dual (ZMod 2) E κE +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. εZMod 2 +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. QQ2Presentation.Quadratic.QuadF2 W.formQ2Presentation.Quadratic.QuadF2.form.{u_2} {V : Type u_2} [AddCommGroup V] [Module (ZMod 2) V]
  (self : Q2Presentation.Quadratic.QuadF2 V) : V → ZMod 2the quadratic map `q : V → F₂`  (AModule.Dual (ZMod 2) E → W χModule.Dual (ZMod 2) E))HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`.