theorem Q2Presentation.Induction.headIm_odd_of_unramified
  {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)
  (h1Q2Presentation.Induction.headTau chief K = 1 : Q2Presentation.Induction.headTauQ2Presentation.Induction.headTau {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) : Q2Presentation.Induction.HeadIm chief K**`τ̃` — THE canonical ramification operator of the block** (design
§4.2/§4.5: `headTau = 1` exactly captures the unramified discharge
below; when P8-S2a lands, `blockTameRamFlag` is to be DEFINED as the
Bool-spelling of `headTau ≠ 1`, so the F-ram gate and the sign-lane
flag are the same object).  chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

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

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


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 1) :
  OddOdd.{u_2} {α : Type u_2} [Semiring α] (a : α) : PropAn element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`.  (Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number.
If `α` is infinite, `Nat.card α = 0`.  (Q2Presentation.Induction.HeadImQ2Presentation.Induction.HeadIm {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) : Type**The faithful head-action image** (the carrier of the averaging;
the manuscript's `H_V`-quotient of `lem:basedetclass`).  chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor))

theorem Q2Presentation.Induction.baseModelExists_of_unramified
  {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) (h1Q2Presentation.Induction.headTau chief K = 1 : Q2Presentation.Induction.headTauQ2Presentation.Induction.headTau {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) : Q2Presentation.Induction.HeadIm chief K**`τ̃` — THE canonical ramification operator of the block** (design
§4.2/§4.5: `headTau = 1` exactly captures the unramified discharge
below; when P8-S2a lands, `blockTameRamFlag` is to be DEFINED as the
Bool-spelling of `headTau ≠ 1`, so the F-ram gate and the sign-lane
flag are the same object).  chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

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

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


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 1) :
  Q2Presentation.Induction.BaseModelExistsQ2Presentation.Induction.BaseModelExists {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)) (hne : lam ≠ 0) : Prop**KEEP-SHAPED INPUT (named `Prop`, consumed as a hypothesis):
the base equivariant determinant class exists at the R4b head.**

Provenance (manuscript): `lem:basedetclass` l.2286–2360 — the normalized
base class `κ_q⁰ ∈ Z²(V⋊H,𝔽₂)` with fibre square map `q`, built on an
`H`-split regular pair via the three orbit-polynomial factor sets
(`eq:squareorbitfactor`, `eq:freeorbitfactor`, `eq:kappahalforbit`);
its normalized-section action data are exactly the `m_c` of
`lem:extraspecialconnecting`.  The proof consumes the tame module
structure (projectivity via `lem:faithfulprojective` in the ramified
case, Maschke in the odd unramified case) — genuinely arithmetic input
about `V`, NOT finite bookkeeping.

Dissolution program (owner: the P6 base-class lane, coordinated with
BLOCKR_P6_DESIGN §1.1 which records the `eq:basekappacochain`
normalization shape): (i) the split pair `V → 𝔽₂[H]^N → V` at the head
(`edgeHead`-carrier Maschke/projectivity); (ii) the three orbit factor
sets with their `m_c = 0` resp. half-orbit corrections; (iii) pullback
and the `eq:mquadratic`/`eq:mcoherent` laws.  Until it lands, both
`btChild_splits_of` and `zeroEdgeDescentData_nonempty_of` consume the
DATA (`BaseModelData`) as an explicit hypothesis.  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) hnelam ≠ 0

theorem Q2Presentation.Induction.baseModelExists_of_oddHeadAction
  {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)
  (hoddOdd (Nat.card (Q2Presentation.Induction.HeadIm chief K)) : OddOdd.{u_2} {α : Type u_2} [Semiring α] (a : α) : PropAn element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`.  (Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number.
If `α` is infinite, `Nat.card α = 0`.  (Q2Presentation.Induction.HeadImQ2Presentation.Induction.HeadIm {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) : Type**The faithful head-action image** (the carrier of the averaging;
the manuscript's `H_V`-quotient of `lem:basedetclass`).  chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor))) :
  Q2Presentation.Induction.BaseModelExistsQ2Presentation.Induction.BaseModelExists {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)) (hne : lam ≠ 0) : Prop**KEEP-SHAPED INPUT (named `Prop`, consumed as a hypothesis):
the base equivariant determinant class exists at the R4b head.**

Provenance (manuscript): `lem:basedetclass` l.2286–2360 — the normalized
base class `κ_q⁰ ∈ Z²(V⋊H,𝔽₂)` with fibre square map `q`, built on an
`H`-split regular pair via the three orbit-polynomial factor sets
(`eq:squareorbitfactor`, `eq:freeorbitfactor`, `eq:kappahalforbit`);
its normalized-section action data are exactly the `m_c` of
`lem:extraspecialconnecting`.  The proof consumes the tame module
structure (projectivity via `lem:faithfulprojective` in the ramified
case, Maschke in the odd unramified case) — genuinely arithmetic input
about `V`, NOT finite bookkeeping.

Dissolution program (owner: the P6 base-class lane, coordinated with
BLOCKR_P6_DESIGN §1.1 which records the `eq:basekappacochain`
normalization shape): (i) the split pair `V → 𝔽₂[H]^N → V` at the head
(`edgeHead`-carrier Maschke/projectivity); (ii) the three orbit factor
sets with their `m_c = 0` resp. half-orbit corrections; (iii) pullback
and the `eq:mquadratic`/`eq:mcoherent` laws.  Until it lands, both
`btChild_splits_of` and `zeroEdgeDescentData_nonempty_of` consume the
DATA (`BaseModelData`) as an explicit hypothesis.  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) hnelam ≠ 0

theorem Q2Presentation.Induction.splitsBtChild_of_zeroEdge_of_oddHeadAction
  {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)
  (hZQ2Presentation.Induction.ZeroEdge chief K lam hinv : Q2Presentation.Induction.ZeroEdgeQ2Presentation.Induction.ZeroEdge {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)) : Prop**The zero-edge predicate** (`lem:radicaledge`'s `[ε̄] = 0` branch,
cocycle-free): some edge complement is normal in the whole cover.  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))
  (hoddOdd (Nat.card (Q2Presentation.Induction.HeadIm chief K)) : OddOdd.{u_2} {α : Type u_2} [Semiring α] (a : α) : PropAn element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`.  (Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number.
If `α` is infinite, `Nat.card α = 0`.  (Q2Presentation.Induction.HeadImQ2Presentation.Induction.HeadIm {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) : Type**The faithful head-action image** (the carrier of the averaging;
the manuscript's `H_V`-quotient of `lem:basedetclass`).  chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor))) :
  Q2Presentation.Induction.SplitsBtChildQ2Presentation.Induction.SplitsBtChild {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) : Prop**`B/T'` splits as `V⋊C`** (the conclusion of `lem:transgression` at
the child, complement form — the exact shape of the `Csec/hdisj/hsup`
slots of `ZeroEdgeDescentData`, design §4.7).  chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor

theorem Q2Presentation.Induction.baseModelExists_iff_splits
  {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)
  (hZQ2Presentation.Induction.ZeroEdge chief K lam hinv : Q2Presentation.Induction.ZeroEdgeQ2Presentation.Induction.ZeroEdge {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)) : Prop**The zero-edge predicate** (`lem:radicaledge`'s `[ε̄] = 0` branch,
cocycle-free): some edge complement is normal in the whole cover.  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.Induction.BaseModelExistsQ2Presentation.Induction.BaseModelExists {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)) (hne : lam ≠ 0) : Prop**KEEP-SHAPED INPUT (named `Prop`, consumed as a hypothesis):
the base equivariant determinant class exists at the R4b head.**

Provenance (manuscript): `lem:basedetclass` l.2286–2360 — the normalized
base class `κ_q⁰ ∈ Z²(V⋊H,𝔽₂)` with fibre square map `q`, built on an
`H`-split regular pair via the three orbit-polynomial factor sets
(`eq:squareorbitfactor`, `eq:freeorbitfactor`, `eq:kappahalforbit`);
its normalized-section action data are exactly the `m_c` of
`lem:extraspecialconnecting`.  The proof consumes the tame module
structure (projectivity via `lem:faithfulprojective` in the ramified
case, Maschke in the odd unramified case) — genuinely arithmetic input
about `V`, NOT finite bookkeeping.

Dissolution program (owner: the P6 base-class lane, coordinated with
BLOCKR_P6_DESIGN §1.1 which records the `eq:basekappacochain`
normalization shape): (i) the split pair `V → 𝔽₂[H]^N → V` at the head
(`edgeHead`-carrier Maschke/projectivity); (ii) the three orbit factor
sets with their `m_c = 0` resp. half-orbit corrections; (iii) pullback
and the `eq:mquadratic`/`eq:mcoherent` laws.  Until it lands, both
`btChild_splits_of` and `zeroEdgeDescentData_nonempty_of` consume the
DATA (`BaseModelData`) as an explicit hypothesis.  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) hnelam ≠ 0 ↔Iff (a b : Prop) : PropIf and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
is equivalent to the corresponding expression with `b` instead.


Conventions for notations in identifiers:

 * The recommended spelling of `↔` in identifiers is `iff`.

 * The recommended spelling of `<->` in identifiers is `iff` (prefer `↔` over `<->`).
    Q2Presentation.Induction.SplitsBtChildQ2Presentation.Induction.SplitsBtChild {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) : Prop**`B/T'` splits as `V⋊C`** (the conclusion of `lem:transgression` at
the child, complement form — the exact shape of the `Csec/hdisj/hsup`
slots of `ZeroEdgeDescentData`, design §4.7).  chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor

theorem Q2Presentation.Induction.btChild_splits
  {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)
  (hreadQ2Presentation.Induction.TransgressionReading chief K lam hinv hne :
    Q2Presentation.Induction.TransgressionReadingQ2Presentation.Induction.TransgressionReading {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)) (hne : lam ≠ 0) : Prop**Named deferred-construction `Prop`** (hypothesis slot; see the
`TransgressionDescentData` docstring for the two-part provenance: the
manuscript source is `lem:transgression`'s section/reading choices at the
descended cover of `lem:radicaledge` step 7, and the dissolution is the
mechanical U1–U3 reading construction — finite bookkeeping, no keeps).  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) hnelam ≠ 0)
  (hbaseQ2Presentation.Induction.BaseModelExists chief K lam hinv hne :
    Q2Presentation.Induction.BaseModelExistsQ2Presentation.Induction.BaseModelExists {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)) (hne : lam ≠ 0) : Prop**KEEP-SHAPED INPUT (named `Prop`, consumed as a hypothesis):
the base equivariant determinant class exists at the R4b head.**

Provenance (manuscript): `lem:basedetclass` l.2286–2360 — the normalized
base class `κ_q⁰ ∈ Z²(V⋊H,𝔽₂)` with fibre square map `q`, built on an
`H`-split regular pair via the three orbit-polynomial factor sets
(`eq:squareorbitfactor`, `eq:freeorbitfactor`, `eq:kappahalforbit`);
its normalized-section action data are exactly the `m_c` of
`lem:extraspecialconnecting`.  The proof consumes the tame module
structure (projectivity via `lem:faithfulprojective` in the ramified
case, Maschke in the odd unramified case) — genuinely arithmetic input
about `V`, NOT finite bookkeeping.

Dissolution program (owner: the P6 base-class lane, coordinated with
BLOCKR_P6_DESIGN §1.1 which records the `eq:basekappacochain`
normalization shape): (i) the split pair `V → 𝔽₂[H]^N → V` at the head
(`edgeHead`-carrier Maschke/projectivity); (ii) the three orbit factor
sets with their `m_c = 0` resp. half-orbit corrections; (iii) pullback
and the `eq:mquadratic`/`eq:mcoherent` laws.  Until it lands, both
`btChild_splits_of` and `zeroEdgeDescentData_nonempty_of` consume the
DATA (`BaseModelData`) as an explicit hypothesis.  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) hnelam ≠ 0) :
  Q2Presentation.Induction.SplitsBtChildQ2Presentation.Induction.SplitsBtChild {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) : Prop**`B/T'` splits as `V⋊C`** (the conclusion of `lem:transgression` at
the child, complement form — the exact shape of the `Csec/hdisj/hsup`
slots of `ZeroEdgeDescentData`, design §4.7).  chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor

theorem Q2Presentation.Induction.zeroEdgePinnedExistence
  {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)
  (hZQ2Presentation.Induction.ZeroEdge chief K lam hinv : Q2Presentation.Induction.ZeroEdgeQ2Presentation.Induction.ZeroEdge {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)) : Prop**The zero-edge predicate** (`lem:radicaledge`'s `[ε̄] = 0` branch,
cocycle-free): some edge complement is normal in the whole cover.  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))
  (hbaseQ2Presentation.Induction.BaseModelExists chief K lam hinv hne :
    Q2Presentation.Induction.BaseModelExistsQ2Presentation.Induction.BaseModelExists {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)) (hne : lam ≠ 0) : Prop**KEEP-SHAPED INPUT (named `Prop`, consumed as a hypothesis):
the base equivariant determinant class exists at the R4b head.**

Provenance (manuscript): `lem:basedetclass` l.2286–2360 — the normalized
base class `κ_q⁰ ∈ Z²(V⋊H,𝔽₂)` with fibre square map `q`, built on an
`H`-split regular pair via the three orbit-polynomial factor sets
(`eq:squareorbitfactor`, `eq:freeorbitfactor`, `eq:kappahalforbit`);
its normalized-section action data are exactly the `m_c` of
`lem:extraspecialconnecting`.  The proof consumes the tame module
structure (projectivity via `lem:faithfulprojective` in the ramified
case, Maschke in the odd unramified case) — genuinely arithmetic input
about `V`, NOT finite bookkeeping.

Dissolution program (owner: the P6 base-class lane, coordinated with
BLOCKR_P6_DESIGN §1.1 which records the `eq:basekappacochain`
normalization shape): (i) the split pair `V → 𝔽₂[H]^N → V` at the head
(`edgeHead`-carrier Maschke/projectivity); (ii) the three orbit factor
sets with their `m_c = 0` resp. half-orbit corrections; (iii) pullback
and the `eq:mquadratic`/`eq:mcoherent` laws.  Until it lands, both
`btChild_splits_of` and `zeroEdgeDescentData_nonempty_of` consume the
DATA (`BaseModelData`) as an explicit hypothesis.  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) hnelam ≠ 0) :
  ∃ ZQ2Presentation.Induction.ZeroEdgeDescentData chief K lam hinv,
    Q2Presentation.Induction.ZeroEdgeDescentDataPinnedQ2Presentation.Induction.ZeroEdgeDescentDataPinned {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))
  (Z : Q2Presentation.Induction.ZeroEdgeDescentData chief K lam hinv) : Prop**The pinning `Prop`** — the exact hypothesis slot the future
coordinated zero-edge keep must carry alongside the bundle `Z` until the
reading-data construction lands (the §13 note's discipline: conditioning
lives on the future keep, never in the count `Prop`s).  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)
      ZQ2Presentation.Induction.ZeroEdgeDescentData chief K lam hinv

theorem Q2Presentation.Induction.zeroEdgePinnedExistence_of_oddHeadAction
  {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)
  (hZQ2Presentation.Induction.ZeroEdge chief K lam hinv : Q2Presentation.Induction.ZeroEdgeQ2Presentation.Induction.ZeroEdge {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)) : Prop**The zero-edge predicate** (`lem:radicaledge`'s `[ε̄] = 0` branch,
cocycle-free): some edge complement is normal in the whole cover.  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))
  (hoddOdd (Nat.card (Q2Presentation.Induction.HeadIm chief K)) : OddOdd.{u_2} {α : Type u_2} [Semiring α] (a : α) : PropAn element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`.  (Nat.cardNat.card.{u_3} (α : Type u_3) : ℕ`Nat.card α` is the cardinality of `α` as a natural number.
If `α` is infinite, `Nat.card α = 0`.  (Q2Presentation.Induction.HeadImQ2Presentation.Induction.HeadIm {p : Q2Presentation.Induction.FramedPair}
  (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p)
  (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) : Type**The faithful head-action image** (the carrier of the averaging;
the manuscript's `H_V`-quotient of `lem:basedetclass`).  chiefQ2Presentation.Induction.FirstNonScalarChiefFactor p KQ2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor))) :
  ∃ ZQ2Presentation.Induction.ZeroEdgeDescentData chief K lam hinv,
    Q2Presentation.Induction.ZeroEdgeDescentDataPinnedQ2Presentation.Induction.ZeroEdgeDescentDataPinned {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))
  (Z : Q2Presentation.Induction.ZeroEdgeDescentData chief K lam hinv) : Prop**The pinning `Prop`** — the exact hypothesis slot the future
coordinated zero-edge keep must carry alongside the bundle `Z` until the
reading-data construction lands (the §13 note's discipline: conditioning
lives on the future keep, never in the count `Prop`s).  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)
      ZQ2Presentation.Induction.ZeroEdgeDescentData chief K lam hinv

theorem Q2Presentation.Quadratic.Candidate.candidateForm_polar_eq.{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]
  (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) (U(Module.End (ZMod 2) V)ˣ : (Module.EndModule.End.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type vLinear endomorphisms of a module, with associated ring structure
`Module.End.semiring` and algebra structure `Module.End.algebra`.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) VType u_1)ˣUnits.{u} (α : Type u) [Monoid α] : Type uUnits of a `Monoid`, bundled version. Notation: `αˣ`.

An element of a `Monoid` is a unit if it has a two-sided inverse.
This version bundles the inverse element so that it can be computed.
For a predicate see `IsUnit`. )
  (hisom∀ (x y : V), (q.polar (↑U x)) (↑U y) = (q.polar x) y : ∀ (xV yV : VType u_1), (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  (↑U(Module.End (ZMod 2) V)ˣ xV)) (↑U(Module.End (ZMod 2) V)ˣ yV) =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`. (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  xV) yV)
  (cV c'V : VType u_1) :
  ((Q2Presentation.Quadratic.Candidate.candidateFormQ2Presentation.Quadratic.Candidate.candidateForm.{u_1} {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V]
  (q : Q2Presentation.Quadratic.QuadF2 V) (U : (Module.End (ZMod 2) V)ˣ)
  (hisom : ∀ (x y : V), (q.polar (↑U x)) (↑U y) = (q.polar x) y) : Q2Presentation.Quadratic.QuadF2 V**The candidate base determinant form** `Q_A^0` in the ramified normal form
(eq:QAcases): `form c = q(c) + b_q(c, U^{-1}c)`, with polar form the mixed-Hessian
operator `b_q(c, (1 + U + U^{-1}) c')` (eq:polaroperator).  qQ2Presentation.Quadratic.QuadF2 V U(Module.End (ZMod 2) V)ˣ hisom∀ (x y : V), (q.polar (↑U x)) (↑U y) = (q.polar x) y).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  cV)
      c'V =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`.
    (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  cV) ((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`.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`. ↑U(Module.End (ZMod 2) V)ˣ +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`. ↑U(Module.End (ZMod 2) V)ˣ⁻¹Inv.inv.{u} {α : Type u} [self : Inv α] : α → α`a⁻¹` computes the inverse of `a`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `⁻¹` in identifiers is `inv`.)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`. c'V)

theorem Q2Presentation.Quadratic.Candidate.candidateForm_nonsingular.{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]
  (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) (U(Module.End (ZMod 2) V)ˣ : (Module.EndModule.End.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type vLinear endomorphisms of a module, with associated ring structure
`Module.End.semiring` and algebra structure `Module.End.algebra`.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) VType u_1)ˣUnits.{u} (α : Type u) [Monoid α] : Type uUnits of a `Monoid`, bundled version. Notation: `αˣ`.

An element of a `Monoid` is a unit if it has a two-sided inverse.
This version bundles the inverse element so that it can be computed.
For a predicate see `IsUnit`. )
  (hisom∀ (x y : V), (q.polar (↑U x)) (↑U y) = (q.polar x) y : ∀ (xV yV : VType u_1), (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  (↑U(Module.End (ZMod 2) V)ˣ xV)) (↑U(Module.End (ZMod 2) V)ˣ yV) =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`. (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  xV) yV)
  (hqq.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). )
  (hMIsUnit (Q2Presentation.Quadratic.Candidate.pairOp U) : IsUnitIsUnit.{u_1} {M : Type u_1} [Monoid M] (a : M) : PropAn element `a : M` of a `Monoid` is a unit if it has a two-sided inverse.
The actual definition says that `a` is equal to some `u : Mˣ`, where
`Mˣ` is a bundled version of `IsUnit`.  (Q2Presentation.Quadratic.Candidate.pairOpQ2Presentation.Quadratic.Candidate.pairOp.{u_1} {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V]
  (U : (Module.End (ZMod 2) V)ˣ) : Module.End (ZMod 2) VThe **mixed-Hessian pairing operator** `M = 1 + U + U⁻¹` on `V` (`pairingOp`,
eq:pairingoperator).  U(Module.End (ZMod 2) V)ˣ)) :
  (Q2Presentation.Quadratic.Candidate.candidateFormQ2Presentation.Quadratic.Candidate.candidateForm.{u_1} {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V]
  (q : Q2Presentation.Quadratic.QuadF2 V) (U : (Module.End (ZMod 2) V)ˣ)
  (hisom : ∀ (x y : V), (q.polar (↑U x)) (↑U y) = (q.polar x) y) : Q2Presentation.Quadratic.QuadF2 V**The candidate base determinant form** `Q_A^0` in the ramified normal form
(eq:QAcases): `form c = q(c) + b_q(c, U^{-1}c)`, with polar form the mixed-Hessian
operator `b_q(c, (1 + U + U^{-1}) c')` (eq:polaroperator).  qQ2Presentation.Quadratic.QuadF2 V U(Module.End (ZMod 2) V)ˣ
      hisom∀ (x y : V), (q.polar (↑U x)) (↑U y) = (q.polar x) y).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). 

theorem Q2Presentation.Quadratic.CandidateArf.hyp_count_eq_plus :
  ↑(Q2Presentation.Quadratic.numZerosQ2Presentation.Quadratic.numZeros.{u_1} {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V]
  (q : Q2Presentation.Quadratic.QuadF2 V) : ℕThe number of zeros `# Q⁻¹(0)` of a quadratic form. 
        Q2Presentation.Quadratic.CandidateArf.hypQ2Presentation.Quadratic.CandidateArf.hyp : Q2Presentation.Quadratic.QuadF2 Q2Presentation.Quadratic.CandidateArf.WThe hyperbolic quadratic form `q(a,b) = a*b` on `(ZMod 2)²`. A genuinely nonsingular
`QuadF2` (its polar form is the standard symplectic form). ) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

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

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


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
    Q2Presentation.Quadratic.baseZeroCountQ2Presentation.Quadratic.baseZeroCount (ramified : Bool) (d : ℕ) : ℤThe **base determinant zero count** `2^{d-1} + ε·2^{d/2-1}` (eq:candidatezeros /
eq:localzeros).  trueBool.true : BoolThe Boolean value `true`, not to be confused with the proposition `True`. 
      (Module.finrankModule.finrank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : ℕThe rank of a module as a natural number.

For a finite-dimensional vector space `V` over a field `k`, `Module.finrank k V` is equal to
the dimension of `V` over `k`.

For a general module `M` over a ring `R`, `Module.finrank R M` is defined to be the supremum of the
cardinalities of the `R`-linearly independent subsets of `M`, if this supremum is finite. It is
defined by convention to be `0` if this supremum is infinite. See `Module.rank` for a
cardinal-valued version where infinite rank modules have rank an infinite cardinal.

Note that if `R` is not a field then there can exist modules `M` with `¬(Module.Finite R M)` but
`finrank R M ≠ 0`. For example `ℚ` has `finrank` equal to `1` over `ℤ`, because the nonempty
`ℤ`-linearly independent subsets of `ℚ` are precisely the nonzero singletons.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) Q2Presentation.Quadratic.CandidateArf.WQ2Presentation.Quadratic.CandidateArf.W : TypeCarrier of the explicit witness: the hyperbolic plane `(ZMod 2)²`. )

theorem Q2Presentation.Quadratic.CandidateArf.hyp_correct_existential :
  ∃ ramBool,
    ↑(Q2Presentation.Quadratic.numZerosQ2Presentation.Quadratic.numZeros.{u_1} {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V]
  (q : Q2Presentation.Quadratic.QuadF2 V) : ℕThe number of zeros `# Q⁻¹(0)` of a quadratic form. 
          Q2Presentation.Quadratic.CandidateArf.hypQ2Presentation.Quadratic.CandidateArf.hyp : Q2Presentation.Quadratic.QuadF2 Q2Presentation.Quadratic.CandidateArf.WThe hyperbolic quadratic form `q(a,b) = a*b` on `(ZMod 2)²`. A genuinely nonsingular
`QuadF2` (its polar form is the standard symplectic form). ) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

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

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


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
      Q2Presentation.Quadratic.baseZeroCountQ2Presentation.Quadratic.baseZeroCount (ramified : Bool) (d : ℕ) : ℤThe **base determinant zero count** `2^{d-1} + ε·2^{d/2-1}` (eq:candidatezeros /
eq:localzeros).  ramBool
        (Module.finrankModule.finrank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : ℕThe rank of a module as a natural number.

For a finite-dimensional vector space `V` over a field `k`, `Module.finrank k V` is equal to
the dimension of `V` over `k`.

For a general module `M` over a ring `R`, `Module.finrank R M` is defined to be the supremum of the
cardinalities of the `R`-linearly independent subsets of `M`, if this supremum is finite. It is
defined by convention to be `0` if this supremum is infinite. See `Module.rank` for a
cardinal-valued version where infinite rank modules have rank an infinite cardinal.

Note that if `R` is not a field then there can exist modules `M` with `¬(Module.Finite R M)` but
`finrank R M ≠ 0`. For example `ℚ` has `finrank` equal to `1` over `ℤ`, because the nonempty
`ℤ`-linearly independent subsets of `ℚ` are precisely the nonzero singletons.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2)
          Q2Presentation.Quadratic.CandidateArf.WQ2Presentation.Quadratic.CandidateArf.W : TypeCarrier of the explicit witness: the hyperbolic plane `(ZMod 2)²`. )

theorem Q2Presentation.Quadratic.candidate_base_zeroCount_proven.{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]
  [Module.FiniteModule.Finite.{u_1, u_4} (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : PropA module over a semiring is `Module.Finite` if it is finitely generated as a module.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) VType u_1] [NontrivialNontrivial.{u_3} (α : Type u_3) : PropPredicate typeclass for expressing that a type is not reduced to a single element. In rings,
this is equivalent to `0 ≠ 1`. In vector spaces, this is equivalent to positive dimension.  VType u_1]
  (qAQ2Presentation.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) (hnsqA.Nonsingular : qAQ2Presentation.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). ) :
  ∃ ramBool,
    ↑(Q2Presentation.Quadratic.numZerosQ2Presentation.Quadratic.numZeros.{u_1} {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V]
  (q : Q2Presentation.Quadratic.QuadF2 V) : ℕThe number of zeros `# Q⁻¹(0)` of a quadratic form.  qAQ2Presentation.Quadratic.QuadF2 V) =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

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

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


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
      Q2Presentation.Quadratic.baseZeroCountQ2Presentation.Quadratic.baseZeroCount (ramified : Bool) (d : ℕ) : ℤThe **base determinant zero count** `2^{d-1} + ε·2^{d/2-1}` (eq:candidatezeros /
eq:localzeros).  ramBool
        (Module.finrankModule.finrank.{u_1, u_2} (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : ℕThe rank of a module as a natural number.

For a finite-dimensional vector space `V` over a field `k`, `Module.finrank k V` is equal to
the dimension of `V` over `k`.

For a general module `M` over a ring `R`, `Module.finrank R M` is defined to be the supremum of the
cardinalities of the `R`-linearly independent subsets of `M`, if this supremum is finite. It is
defined by convention to be `0` if this supremum is infinite. See `Module.rank` for a
cardinal-valued version where infinite rank modules have rank an infinite cardinal.

Note that if `R` is not a field then there can exist modules `M` with `¬(Module.Finite R M)` but
`finrank R M ≠ 0`. For example `ℚ` has `finrank` equal to `1` over `ℤ`, because the nonempty
`ℤ`-linearly independent subsets of `ℚ` are precisely the nonzero singletons.  (ZModZMod : ℕ → TypeThe integers modulo `n : ℕ`.  2) VType u_1)