Char-2 scalar helpers (private, decide-grounded)

CocycleCover.lean's zmod2_add_self is private there; the file-local mirrors below keep every char-2 rearrangement a closed 𝔽₂ computation.

The solvability indicator (∃ continuous c, δc = F)

def Q2Presentation.Induction.CochainSolvable (Γ : ProfiniteGrp.{0}) (F : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2) : Prop

Cochain solvability (design §4-N2): the 2-cochain equation of F on the profinite source Γ has a continuous (= locally constant, Γ profinite and 𝔽₂ discrete) solution — ∃ c : Γ → 𝔽₂ continuous with c (γγ') = c γ + c γ' + F γ γ'. This is the SOLVABILITY INDICATOR of the normalized-cochain house style: no cohomology carrier is ever formed, and F need not be a cocycle for the Prop to be well-formed (the calculus below restricts to cocycles exactly where the mathematics does).

Equations

• Q2Presentation.Induction.CochainSolvable Γ F = ∃ (c : ↑Γ.toProfinite.toTop → ZMod 2), IsLocallyConstant c ∧ ∀ (γ γ' : ↑Γ.toProfinite.toTop), c (γ * γ') = c γ + c γ' + F γ γ'

theorem Q2Presentation.Induction.cochainEq_apply_one {Γ : ProfiniteGrp.{0}} {F : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2} {c : ↑Γ.toProfinite.toTop → ZMod 2} (heq : ∀ (γ γ' : ↑Γ.toProfinite.toTop), c (γ * γ') = c γ + c γ' + F γ γ') (hF : F 1 1 = 0) : c 1 = 0

Any solution of an equation with normalized diagonal value is itself normalized: c 1 = 0 (evaluate at (1,1), char 2).

theorem Q2Presentation.Induction.cochainSolvable_zero {Γ : ProfiniteGrp.{0}} : CochainSolvable Γ 0

The zero equation is solvable (witness c = 0).

theorem Q2Presentation.Induction.cochainSolvable_add {Γ : ProfiniteGrp.{0}} {F₁ F₂ : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2} (h₁ : CochainSolvable Γ F₁) (h₂ : CochainSolvable Γ F₂) : CochainSolvable Γ (F₁ + F₂)

The free half of additivity: solvable + solvable ⟹ solvable, by the sum of the witnesses (no cocycle law, no token needed).

theorem Q2Presentation.Induction.cochainSolvable_add_cancel_left {Γ : ProfiniteGrp.{0}} {F₁ F₂ : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2} (h₁ : CochainSolvable Γ F₁) (h : CochainSolvable Γ (F₁ + F₂)) : CochainSolvable Γ F₂

Char-2 cancellation: a solvable summand can be cancelled from a solvable sum (F₂ = F₁ + (F₁ + F₂) over 𝔽₂).

theorem Q2Presentation.Induction.not_cochainSolvable_add_left {Γ : ProfiniteGrp.{0}} {F₁ F₂ : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2} (h₁ : CochainSolvable Γ F₁) (h₂ : ¬CochainSolvable Γ F₂) : ¬CochainSolvable Γ (F₁ + F₂)

Solvable + unsolvable ⟹ unsolvable (left form).

theorem Q2Presentation.Induction.not_cochainSolvable_add_right {Γ : ProfiniteGrp.{0}} {F₁ F₂ : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2} (h₁ : ¬CochainSolvable Γ F₁) (h₂ : CochainSolvable Γ F₂) : ¬CochainSolvable Γ (F₁ + F₂)

Unsolvable + solvable ⟹ unsolvable (right form).

Explicit coboundary shifts

def Q2Presentation.Induction.cochainCoboundary (Γ : ProfiniteGrp.{0}) (u : ↑Γ.toProfinite.toTop → ZMod 2) : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2

The explicit coboundary δu of a 1-cochain u (char-2 inhomogeneous differential, trivial action): δu (γ, γ') = u γ + u γ' + u (γγ'). N7's completed-square defects and eq:Qkappadifference corrections enter the calculus through this def.

Equations

• Q2Presentation.Induction.cochainCoboundary Γ u γ γ' = u γ + u γ' + u (γ * γ')

@[simp]

theorem Q2Presentation.Induction.cochainCoboundary_apply {Γ : ProfiniteGrp.{0}} (u : ↑Γ.toProfinite.toTop → ZMod 2) (γ γ' : ↑Γ.toProfinite.toTop) : cochainCoboundary Γ u γ γ' = u γ + u γ' + u (γ * γ')

theorem Q2Presentation.Induction.cochainSolvable_coboundary {Γ : ProfiniteGrp.{0}} {u : ↑Γ.toProfinite.toTop → ZMod 2} (hu : IsLocallyConstant u) : CochainSolvable Γ (cochainCoboundary Γ u)

A continuous coboundary is solvable — the witness is u itself (char 2: u (γγ') = u γ + u γ' + δu (γ, γ') rearranges to a tautology).

theorem Q2Presentation.Induction.cochainSolvable_add_coboundary_iff {Γ : ProfiniteGrp.{0}} {F : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2} {u : ↑Γ.toProfinite.toTop → ZMod 2} (hu : IsLocallyConstant u) : CochainSolvable Γ (F + cochainCoboundary Γ u) ↔ CochainSolvable Γ F

Coboundary-shift invariance of solvability (design §4-N2 free half): shifting an equation by an explicit continuous coboundary does not change its solvability.

Normalized continuous 2-cocycles

The exact hypothesis package of the W7a cover carrier: CocycleExt's (hz1, hz2, hzc) plus local constancy of the two-variable cochain. The additivity token quantifies over THIS class only (over-strength guard).

structure Q2Presentation.Induction.IsNormalized2Cocycle (Γ : ProfiniteGrp.{0}) (F : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2) : Prop

Normalized continuous 𝔽₂-valued 2-cocycle on a profinite source: locally constant in the pair, normalized on both 1-slots, and satisfying the (trivial-action, char-2) 2-cocycle law — the (hz1, hz2, hzc) package of CocycleExt with the continuity that finite cover targets make automatic there but which is LOAD-BEARING at a profinite source.

• locallyConstant : IsLocallyConstant fun (p : ↑Γ.toProfinite.toTop × ↑Γ.toProfinite.toTop) => F p.1 p.2

  Joint local constancy (= continuity into discrete 𝔽₂).

• map_one_left (γ : ↑Γ.toProfinite.toTop) : F 1 γ = 0

  Left normalization F 1 γ = 0.

• map_one_right (γ : ↑Γ.toProfinite.toTop) : F γ 1 = 0

  Right normalization F γ 1 = 0.

• cocycle (a b c : ↑Γ.toProfinite.toTop) : F a b + F (a * b) c = F b c + F a (b * c)

  The 2-cocycle law F a b + F (ab) c = F b c + F a (bc).

theorem Q2Presentation.Induction.isNormalized2Cocycle_zero {Γ : ProfiniteGrp.{0}} : IsNormalized2Cocycle Γ 0

The zero cochain is a normalized continuous 2-cocycle.

theorem Q2Presentation.Induction.IsNormalized2Cocycle.add {Γ : ProfiniteGrp.{0}} {F₁ F₂ : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2} (h₁ : IsNormalized2Cocycle Γ F₁) (h₂ : IsNormalized2Cocycle Γ F₂) : IsNormalized2Cocycle Γ (F₁ + F₂)

Normalized continuous 2-cocycles are closed under sums (the carrier of the token's additivity statement).

theorem Q2Presentation.Induction.isNormalized2Cocycle_coboundary {Γ : ProfiniteGrp.{0}} {u : ↑Γ.toProfinite.toTop → ZMod 2} (hu : IsLocallyConstant u) (hu1 : u 1 = 0) : IsNormalized2Cocycle Γ (cochainCoboundary Γ u)

The explicit coboundary of a NORMALIZED continuous 1-cochain is a normalized continuous 2-cocycle (so coboundary shifts stay inside the token's carrier class).

The per-source additivity token and the ι-readings

def Q2Presentation.Induction.IotaToken (Γ : ProfiniteGrp.{0}) : Prop

The per-source ι-additivity token (design §4-N2; the h² ≤ 1 token): at the source Γ, any two UNSOLVABLE normalized continuous 2-cocycle equations have solvable sum. This is the cochain-level spelling of dim H²(Γ, 𝔽₂) ≤ 1 — stated with no cohomology carriers. Consumed as a hypothesis by the N7 engine instantiation; discharged per source by N3 (IotaToken GQ2Profinite, floor F-ι-loc: NSW (7.2.6) at the trivial module + (7.3.1)) and N4 (GammaA-bases, floor F-ι-cand: prop:chainmap l.1687 + lem:finitewordstokes). Together with the free half (cochainSolvable_add, not_cochainSolvable_add_left/right) it makes the case table of iotaRead on cocycle sums total.

Equations

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

def Q2Presentation.Induction.iotaRead (Γ : ProfiniteGrp.{0}) (F : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2) : ZMod 2

The ℤ/2-valued ι-reading of a 2-cochain equation: 0 if solvable, 1 if not — the per-source functional ι_Γ of the R4b design (S5's valuation), read as a bit. Everything downstream consumes this reading (or its ±1 sibling iotaSign), never raw case splits.

Equations

• Q2Presentation.Induction.iotaRead Γ F = if Q2Presentation.Induction.CochainSolvable Γ F then 0 else 1

def Q2Presentation.Induction.iotaSign (Γ : ProfiniteGrp.{0}) (F : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2) : ℤ

The ±1-indicator of solvability in ℤ: +1 if solvable, −1 if not — the summand shape of eq:recursionR5a's s_Γ(ζ) = Σ_ρ (±1) absorption (sGammaZ_eq downstream).

Equations

• Q2Presentation.Induction.iotaSign Γ F = if Q2Presentation.Induction.CochainSolvable Γ F then 1 else -1

theorem Q2Presentation.Induction.iotaRead_def (Γ : ProfiniteGrp.{0}) (F : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2) : iotaRead Γ F = if CochainSolvable Γ F then 0 else 1

Definitional form of iotaRead (the sGammaZ_def fix-class: cite this lemma, never re-haveI a decidability instance).

theorem Q2Presentation.Induction.iotaSign_def (Γ : ProfiniteGrp.{0}) (F : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2) : iotaSign Γ F = if CochainSolvable Γ F then 1 else -1

Definitional form of iotaSign.

theorem Q2Presentation.Induction.iotaRead_of_solvable {Γ : ProfiniteGrp.{0}} {F : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2} (h : CochainSolvable Γ F) : iotaRead Γ F = 0

theorem Q2Presentation.Induction.iotaRead_of_not_solvable {Γ : ProfiniteGrp.{0}} {F : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2} (h : ¬CochainSolvable Γ F) : iotaRead Γ F = 1

theorem Q2Presentation.Induction.iotaSign_of_solvable {Γ : ProfiniteGrp.{0}} {F : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2} (h : CochainSolvable Γ F) : iotaSign Γ F = 1

theorem Q2Presentation.Induction.iotaSign_of_not_solvable {Γ : ProfiniteGrp.{0}} {F : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2} (h : ¬CochainSolvable Γ F) : iotaSign Γ F = -1

theorem Q2Presentation.Induction.iotaRead_eq_zero_iff {Γ : ProfiniteGrp.{0}} {F : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2} : iotaRead Γ F = 0 ↔ CochainSolvable Γ F

The bit reads 0 exactly on solvable equations.

theorem Q2Presentation.Induction.iotaRead_eq_one_iff {Γ : ProfiniteGrp.{0}} {F : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2} : iotaRead Γ F = 1 ↔ ¬CochainSolvable Γ F

The bit reads 1 exactly on unsolvable equations.

theorem Q2Presentation.Induction.iotaSign_eq_one_iff {Γ : ProfiniteGrp.{0}} {F : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2} : iotaSign Γ F = 1 ↔ CochainSolvable Γ F

The indicator reads +1 exactly on solvable equations.

theorem Q2Presentation.Induction.iotaSign_eq_neg_one_iff {Γ : ProfiniteGrp.{0}} {F : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2} : iotaSign Γ F = -1 ↔ ¬CochainSolvable Γ F

The indicator reads −1 exactly on unsolvable equations.

theorem Q2Presentation.Induction.iotaSign_eq_one_sub_two_mul {Γ : ProfiniteGrp.{0}} {F : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2} : iotaSign Γ F = 1 - 2 * ↑(iotaRead Γ F).val

The ±1-indicator through the bit: iotaSign = 1 − 2·iotaRead in ℤ (the 2n − e absorption bridge for N9).

@[simp]

theorem Q2Presentation.Induction.iotaRead_zero {Γ : ProfiniteGrp.{0}} : iotaRead Γ 0 = 0

theorem Q2Presentation.Induction.iotaRead_coboundary {Γ : ProfiniteGrp.{0}} {u : ↑Γ.toProfinite.toTop → ZMod 2} (hu : IsLocallyConstant u) : iotaRead Γ (cochainCoboundary Γ u) = 0

A continuous coboundary reads 0.

theorem Q2Presentation.Induction.iotaRead_add_coboundary {Γ : ProfiniteGrp.{0}} {F : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2} {u : ↑Γ.toProfinite.toTop → ZMod 2} (hu : IsLocallyConstant u) : iotaRead Γ (F + cochainCoboundary Γ u) = iotaRead Γ F

iotaRead is invariant under explicit continuous coboundary shifts.

theorem Q2Presentation.Induction.iotaRead_add {Γ : ProfiniteGrp.{0}} (hT : IotaToken Γ) {F₁ F₂ : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2} (h₁ : IsNormalized2Cocycle Γ F₁) (h₂ : IsNormalized2Cocycle Γ F₂) : iotaRead Γ (F₁ + F₂) = iotaRead Γ F₁ + iotaRead Γ F₂

Additivity of the ι-reading on cocycle sums, given the token (design §4-N2: "the ℤ/2-valued iotaRead is well-defined and additive"). Three quadrants are the free half; the (¬,¬)-quadrant is exactly IotaToken.

theorem Q2Presentation.Induction.iotaSign_add {Γ : ProfiniteGrp.{0}} (hT : IotaToken Γ) {F₁ F₂ : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2} (h₁ : IsNormalized2Cocycle Γ F₁) (h₂ : IsNormalized2Cocycle Γ F₂) : iotaSign Γ (F₁ + F₂) = iotaSign Γ F₁ * iotaSign Γ F₂

Multiplicativity of the ±1-indicator on cocycle sums, given the token (design §4-N2: "the ±1-indicator is multiplicative on cocycle sums").

The ζ-cover reading lemma

Generic in the W7a datum (Yt, ζ) and the source package, exactly the variable discipline of Lifting/CocycleCover.lean; phaseCount (PhaseCoverTransform.lean:81) instantiates Yt := (cChild chief K).1, F := (cChild chief K).2, so the reading below aligns with its Nonempty-predicate EXACTLY (N9 hook).

def Q2Presentation.Induction.pullCochain (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B Yt F) : ↑Γ.toProfinite.toTop → ↑Γ.toProfinite.toTop → ZMod 2

The pulled-back 2-cochain g*ζ of a boundary-framed surjection g : Γ ↠ Y — the source-side equation whose solvability the ζ-cover lift indicator reads (lem:phasecover l.4377–4379).

Equations

• Q2Presentation.Induction.pullCochain Yt zeta B F g γ γ' = zeta ((ProfiniteGrp.Hom.hom (↑g).hom) γ) ((ProfiniteGrp.Hom.hom (↑g).hom) γ')

@[simp]

theorem Q2Presentation.Induction.pullCochain_apply (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B Yt F) (γ γ' : ↑Γ.toProfinite.toTop) : pullCochain Yt zeta B F g γ γ' = zeta ((ProfiniteGrp.Hom.hom (↑g).hom) γ) ((ProfiniteGrp.Hom.hom (↑g).hom) γ')

theorem Q2Presentation.Induction.pullCochain_isNormalized2Cocycle (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B Yt F) : IsNormalized2Cocycle Γ (pullCochain Yt zeta B F g)

The pullback of a normalized 2-cocycle along a boundary-framed surjection is a normalized continuous 2-cocycle — so g*ζ lies in the carrier class of IotaToken (continuity from g's, since Y is finite discrete).

theorem Q2Presentation.Induction.cocycleCoverLiftHom_iff_cochainSolvable (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B Yt F) : Nonempty (Lifting.cocycleCoverLiftHom Yt zeta hz1 hz2 hzc B F g) ↔ CochainSolvable Γ (pullCochain Yt zeta B F g)

The ζ-cover READING lemma (design §4-N2): the weak framed-lift set through the normalized-cocycle central double cover is nonempty iff the pulled-back 2-cochain equation is continuously solvable — the scalar-component split of the GREEN raw-hom unfolding cocycleCoverLiftHom_iff_exists (W7a), (y, s)-law (y,s)·(y',s') = (yy', s + s' + ζ(y,y')). The cover frame clause is transparent because the cover framing is the pulled-back one.

theorem Q2Presentation.Induction.iotaRead_pullCochain_eq_zero_iff (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B Yt F) : iotaRead Γ (pullCochain Yt zeta B F g) = 0 ↔ Nonempty (Lifting.cocycleCoverLiftHom Yt zeta hz1 hz2 hzc B F g)

The bit-alignment of the reading with phaseCount's predicate: the ι-reading of g*ζ is 0 iff g admits a weak framed ζ-cover lift (N9 consumes this per χ at ζ := Delta Z χ).

theorem Q2Presentation.Induction.iotaSign_pullCochain_eq_one_iff (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B Yt F) : iotaSign Γ (pullCochain Yt zeta B F g) = 1 ↔ Nonempty (Lifting.cocycleCoverLiftHom Yt zeta hz1 hz2 hzc B F g)

The ±1-alignment of the reading with phaseCount's predicate.