ℤ₂-powering on pro-2 groups

This file defines x ^ u for a 2-adic exponent u ∈ ℤ₂ and x in any pro-2 group, with the laws consumed by the proofs in §3.

Contents

(i) The projection ℤ̂ ↠ ℤ₂ and the seam isomorphism.

• zhatProjTwo : ℤ̂ → Multiplicative ℤ₂ — defined as γ ↦ (ofAdd 1) ^ᶻ γ, i.e. as a ẑ-power (the profinite-exponentiation API), so continuity/hom-ness/ofInt-anchors come from the existing API.
• zhatProjTwo_surjective, ker_zhatProjTwo : ker = proPKernel 2 ℤ̂.
• ztwoEquivPadic : maxProPQuotient 2 ℤ̂ ≃ₜ* Multiplicative ℤ₂, pinned by maxProPMk (ofInt 1) ↦ ofAdd 1. Since Ztwo := maxProPQuotient 2 Zhat (GQ2/BoundaryFrame.lean, definitionally), this is the ι of SectionThree.prop_3_10_local_marked and the identification Prop. 3.2's nuTwo-surjectivity can compose with.

(ii) ℤ₂-powering on pro-2 groups.

• zpowZtwo (hP : IsProP 2 P) (x : P) (u : ℤ_[2]) : P, bundled as zpowZtwoHom hP x : Multiplicative ℤ₂ →ₜ* P; built from zpowHatHom through (i) via the universal property maxProPHomEquiv.
• Anchors: zpowZtwo_intCast (= x ^ n on integer exponents), exponent additivity (it is a hom), the composition law zpowZtwo_zpowZtwo : (x^u)^v = x^{uv}, naturality map_zpowZtwo, and the uniqueness principle zpowZtwoHom_unique (a continuous hom ℤ₂ → P is determined by its value at 1 — the tool for identifying constructed maps with powerings).
• Bijectivity: zpowZtwo_bijective (x ↦ x^u bijective for u ∈ ℤ₂ˣ, inverse x ↦ x^{u⁻¹}) and pow_bijective_of_odd (odd integer powers; the Lemmas 3.6–3.8 proof's "cube roots", inverse x ↦ x^{m⁻¹}).

(iii) The η-facts (shared the Lemmas 3.4–3.5 proof lemma_3_5_injective / the Lemmas 3.6–3.8 proof prop_3_8_classification prerequisite).

• isProP_two_unitsPadicInt : IsProP 2 ℤ₂ˣ — so η ^ u makes sense for η ∈ ℤ₂ˣ, u ∈ ℤ₂.
• zpowZtwo_injective_of_norm — η-injectivity: if ‖η − 1‖ = 2⁻² (i.e. v₂(η−1) = 2; the paper's η = (−3)⁻¹, cf. norm_inv_neg_three_sub_one) then u ↦ η ^ u is injective. This is the consumable form of the paper's "η topologically generates 1 + 4ℤ₂" (Lemma 3.5's injectivity row and Prop. 3.8's Ȳ-coordinate forcing use exactly injectivity).

(iv) Pro-2 Frattini/Burnside criterion. The complementary statement "surjective on G/Φ(G) implies surjective" is proved in GQ2/FrattiniCriterion.lean in index-p detection form.

Conventions

Multiplicative throughout: exponents live in Multiplicative ℤ_[2] (group law = addition of exponents), matching Zhat's convention; zpowZtwo takes the additive u : ℤ_[2] and wraps it. 2-specific facts use p = 2 instances (Fact (Nat.Prime 2) is found automatically).

The density/extension workhorse

ℤ ⊆ ℤ₂ (indeed ℕ ⊆ ℤ₂) is dense, so a continuous monoid hom out of Multiplicative ℤ₂ into a Hausdorff monoid is determined by its value at ofAdd 1. This single lemma powers all the algebraic laws of zpowZtwo below.

theorem GQ2.multPadicIntHom_ext {M : Type u_1} [Monoid M] [TopologicalSpace M] [T2Space M] {f g : Multiplicative ℤ_[2] →* M} (hf : Continuous ⇑f) (hg : Continuous ⇑g) (h : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) : f = g

Two continuous monoid homs Multiplicative ℤ₂ →* M (M Hausdorff) agreeing at ofAdd 1 are equal. (Via DenseRange.addChar_eq_of_eval_one_eq and AddChar ℤ₂ M ≃ (Multiplicative ℤ₂ →* M).)

ℤ₂-powering of an element of 2-power order

The elementary building block: if g ^ 2^k = 1 then u ↦ g ^ (u mod 2^k) is a continuous monoid hom Multiplicative ℤ₂ →* Q. Used for the kernel computation of zhatProjTwo (where Q is a finite quotient of ℤ̂), and reusable for any finite 2-group target.

noncomputable def GQ2.powZModTwoHom {Q : Type u_1} [Group Q] (g : Q) (k : ℕ) (hg : g ^ 2 ^ k = 1) : Multiplicative ℤ_[2] →* Q

u ↦ g ^ (u mod 2^k) for an element g with g ^ 2^k = 1.

Equations

• GQ2.powZModTwoHom g k hg = { toFun := fun (u : Multiplicative ℤ_[2]) => g ^ ((PadicInt.toZModPow k) (Multiplicative.toAdd u)).val, map_one' := ⋯, map_mul' := ⋯ }

theorem GQ2.isOpen_fiber_toZModPow (k : ℕ) (c : ZMod (2 ^ k)) : IsOpen (⇑(PadicInt.toZModPow k) ⁻¹' {c})

The fibres of toZModPow k : ℤ₂ → ℤ/2^k are open (cosets of the ball span {2^k}).

theorem GQ2.isOpen_preimage_toZModPow (k : ℕ) (T : Set (ZMod (2 ^ k))) : IsOpen (⇑(PadicInt.toZModPow k) ⁻¹' T)

Every toZModPow-preimage is open (union of open fibres): toZModPow k is locally constant.

theorem GQ2.continuous_powZModTwoHom {Q : Type u_1} [Group Q] [TopologicalSpace Q] (g : Q) (k : ℕ) (hg : g ^ 2 ^ k = 1) : Continuous ⇑(powZModTwoHom g k hg)

powZModTwoHom is continuous: it factors through the locally constant toZModPow k.

The canonical projection ℤ̂ ↠ ℤ₂ (part (i))

zhatProjTwo := γ ↦ (ofAdd 1) ^ᶻ γ — the ẑ-power of 1 ∈ ℤ₂ (the profinite-exponentiation API machinery), which on integer exponents is just n ↦ n : ℤ → ℤ₂.

noncomputable def GQ2.Zhat.ofIntHom : Multiplicative ℤ →* ↑Zhat.toProfinite.toTop

The dense embedding ℤ → ℤ̂, bundled (multiplicative convention, as everywhere in GQ2/Zhat.lean).

Equations

• GQ2.Zhat.ofIntHom = { toFun := fun (n : Multiplicative ℤ) => GQ2.Zhat.ofInt (Multiplicative.toAdd n), map_one' := GQ2.Zhat.ofInt_zero, map_mul' := GQ2.Zhat.ofIntHom._proof_1 }

theorem GQ2.Zhat.ofInt_one_zpow (n : ℤ) : ofInt 1 ^ n = ofInt n

ofInt turns integer powers of ofInt 1 into ofInt of the integer.

noncomputable def GQ2.zhatProjTwo : ↑Zhat.toProfinite.toTop →ₜ* Multiplicative ℤ_[2]

The canonical projection ℤ̂ → ℤ₂ (multiplicatively: onto Multiplicative ℤ₂), as the ẑ-power morphism of ofAdd 1: γ ↦ (ofAdd 1) ^ᶻ γ. On ℤ ⊆ ℤ̂ it is the inclusion ℤ ⊆ ℤ₂ (zhatProjTwo_ofInt); it realizes ℤ₂ as the maximal pro-2 quotient of ℤ̂ (ker_zhatProjTwo, ztwoEquivPadic).

Equations

• GQ2.zhatProjTwo = ProfiniteGrp.Hom.hom (GQ2.zpowHatHom (Multiplicative.ofAdd 1))

theorem GQ2.zhatProjTwo_surjective : Function.Surjective ⇑zhatProjTwo

zhatProjTwo is surjective (closed range ⊇ the dense ℕ ⊆ ℤ₂).

theorem GQ2.ker_zhatProjTwo_le : zhatProjTwo.ker ≤ proPKernel 2 ↑Zhat.toProfinite.toTop

The kernel of zhatProjTwo is contained in the pro-2 kernel: any element of ℤ̂ killed by the projection to ℤ₂ dies in every finite 2-group quotient. Proof idea: for an open normal U with 2-group quotient, the quotient map q : ℤ̂ → ℤ̂/U and the composite of zhatProjTwo with "ℤ₂-powering of q(ofInt 1)" (powZModTwoHom) are continuous maps agreeing on the dense ℤ ⊆ ℤ̂, hence equal (funext_ofInt); the second visibly kills ker zhatProjTwo.

theorem GQ2.ker_zhatProjTwo : zhatProjTwo.ker = proPKernel 2 ↑Zhat.toProfinite.toTop

ker zhatProjTwo = proPKernel 2 ℤ̂: the projection to ℤ₂ realizes exactly the maximal pro-2 quotient of ℤ̂ (the missing direction is proPKernel_le_ker for the pro-2 target ℤ₂, GQ2/PropOneOne.lean).

The seam isomorphism maxPro2(ℤ̂) ≅ ℤ₂ (part (i), packaged)

Ztwo := maxProPQuotient 2 Zhat in GQ2/BoundaryFrame.lean (definitionally), so ztwoEquivPadic is the ι : Ztwo ≃ₜ* Multiplicative ℤ₂ of SectionThree.prop_3_10_local_marked, pinned by ztwoOne ↦ ofAdd 1 (ztwoEquivPadic_ofInt_one).

noncomputable def GQ2.ztwoDescend : ↑(maxProPQuotient 2 ↑Zhat.toProfinite.toTop).toProfinite.toTop →ₜ* Multiplicative ℤ_[2]

The descent of zhatProjTwo to the maximal pro-2 quotient.

Equations

• GQ2.ztwoDescend = GQ2.quotientLift (GQ2.proPKernel 2 ↑GQ2.Zhat.toProfinite.toTop) GQ2.zhatProjTwo GQ2.ztwoDescend._proof_2

noncomputable def GQ2.ztwoEquivPadic : ↑(maxProPQuotient 2 ↑Zhat.toProfinite.toTop).toProfinite.toTop ≃ₜ* Multiplicative ℤ_[2]

maxPro2(ℤ̂) ≅ ℤ₂ — the peripheral-action interface "nice-to-have", and the ι-seam of prop_3_10_local_marked/Prop. 3.2's nuTwo (as Ztwo = maxProPQuotient 2 Zhat definitionally).

Equations

• GQ2.ztwoEquivPadic = GQ2.continuousMulEquivOfBijective GQ2.ztwoDescend GQ2.ztwoDescend_bijective✝

@[simp]

theorem GQ2.ztwoEquivPadic_ofInt_one : ztwoEquivPadic ((maxProPMk 2 ↑Zhat.toProfinite.toTop) (Zhat.ofInt 1)) = Multiplicative.ofAdd 1

The generator pin: ztwoOne = maxProPMk (ofInt 1) ↦ ofAdd 1 (the normalization prop_3_10_local_marked requires of ι).

ℤ₂-powering on pro-2 groups (part (ii))

For x in a pro-2 profinite group P, the ẑ-power morphism zpowHatHom x : ℤ̂ ⟶ P (the profinite-exponentiation API) kills proPKernel 2 ℤ̂ (universal property, since P is pro-2), so through ker zhatProjTwo = proPKernel 2 ℤ̂ (part (i)) it factors through ℤ₂: this is zpowZtwoHom. Everything else follows from the extension-by-density workhorse multPadicIntHom_ext.

theorem GQ2.maxProPHomEquiv_symm_apply_maxProPMk {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hP : IsProP p P) (F : G →ₜ* P) (γ : G) : ((maxProPHomEquiv hP).symm F) ((maxProPMk p G) γ) = F γ

Evaluation of the maxProPHomEquiv-descended hom on classes: the descent of F at maxProPMk γ is F γ. (The .symm of the universal property is quotientLift.)

noncomputable def GQ2.zpowZtwoHom {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] (hP : IsProP 2 P) (x : P) : Multiplicative ℤ_[2] →ₜ* P

The ℤ₂-power morphism of x in a pro-2 group P: the unique continuous extension of n ↦ xⁿ to exponents in ℤ₂, as a continuous hom Multiplicative ℤ₂ →ₜ* P. Built by factoring zpowHatHom x : ℤ̂ ⟶ P through zhatProjTwo via the universal property of the maximal pro-2 quotient and the part-(i) isomorphism.

Equations

• GQ2.zpowZtwoHom hP x = ((GQ2.maxProPHomEquiv hP).symm (ProfiniteGrp.Hom.hom (GQ2.zpowHatHom x))).comp ↑GQ2.ztwoEquivPadic.symm

noncomputable def GQ2.zpowZtwo {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] (hP : IsProP 2 P) (x : P) (u : ℤ_[2]) : P

x ^ u for a 2-adic exponent u ∈ ℤ₂ (x in a pro-2 group; additive exponent convention: zpowZtwo hP x (u + v) = zpowZtwo hP x u * zpowZtwo hP x v).

Equations

• GQ2.zpowZtwo hP x u = (GQ2.zpowZtwoHom hP x) (Multiplicative.ofAdd u)

theorem GQ2.continuous_zpowZtwo {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] (hP : IsProP 2 P) (x : P) : Continuous (zpowZtwo hP x)

theorem GQ2.zpowZtwoHom_ofAdd_one {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] (hP : IsProP 2 P) (x : P) : (zpowZtwoHom hP x) (Multiplicative.ofAdd 1) = x

The generator pin: x ^ (1 : ℤ₂) = x.

@[simp]

theorem GQ2.zpowZtwo_one_exp {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] (hP : IsProP 2 P) (x : P) : zpowZtwo hP x 1 = x

@[simp]

theorem GQ2.zpowZtwo_intCast {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] (hP : IsProP 2 P) (x : P) (n : ℤ) : zpowZtwo hP x ↑n = x ^ n

ℤ₂-powers extend ordinary integer powers.

@[simp]

theorem GQ2.zpowZtwo_natCast {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] (hP : IsProP 2 P) (x : P) (n : ℕ) : zpowZtwo hP x ↑n = x ^ n

theorem GQ2.zpowZtwo_add {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] (hP : IsProP 2 P) (x : P) (u v : ℤ_[2]) : zpowZtwo hP x (u + v) = zpowZtwo hP x u * zpowZtwo hP x v

Exponent additivity (the hom law, in zpowZtwo clothing).

theorem GQ2.zpowZtwoHom_unique {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] (hP : IsProP 2 P) {φ : Multiplicative ℤ_[2] →* P} (hφ : Continuous ⇑φ) (u : ℤ_[2]) : φ (Multiplicative.ofAdd u) = zpowZtwo hP (φ (Multiplicative.ofAdd 1)) u

Uniqueness/identification principle: any continuous hom φ : ℤ₂ → P is the ℤ₂-powering of its value at 1. (The tool for recognizing constructed maps as powerings — e.g. the Lemmas 3.6–3.8 proof's Θ_b legs.)

theorem GQ2.zpowZtwo_zpowZtwo {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] (hP : IsProP 2 P) (x : P) (u v : ℤ_[2]) : zpowZtwo hP (zpowZtwo hP x u) v = zpowZtwo hP x (u * v)

Composition law: (x ^ u) ^ v = x ^ (u * v).

@[simp]

theorem GQ2.zpowZtwo_one_base {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] (hP : IsProP 2 P) (u : ℤ_[2]) : zpowZtwo hP 1 u = 1

Powering the identity: 1 ^ u = 1.

theorem GQ2.zpowZtwo_bijective {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] (hP : IsProP 2 P) (u : ℤ_[2]ˣ) : Function.Bijective fun (x : P) => zpowZtwo hP x ↑u

Unit-power bijectivity: for u ∈ ℤ₂ˣ, x ↦ x ^ u is a bijection of P, with inverse x ↦ x ^ u⁻¹.

theorem GQ2.isUnit_intCast_of_odd {m : ℤ} (hm : Odd m) : IsUnit ↑m

Odd integers are units of ℤ₂.

theorem GQ2.map_zpowZtwo {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q] [CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q] (hP : IsProP 2 P) (hQ : IsProP 2 Q) (f : P →ₜ* Q) (x : P) (u : ℤ_[2]) : f (zpowZtwo hP x u) = zpowZtwo hQ (f x) u

Naturality: continuous homs of pro-2 groups commute with ℤ₂-powers.

theorem GQ2.zpowHat_eq_zpowZtwo {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] (hP : IsProP 2 P) (x : P) (γ : ↑Zhat.toProfinite.toTop) : zpowHat x γ = zpowZtwo hP x (Multiplicative.toAdd (zhatProjTwo γ))

Bridge to ẑ-powers: on a pro-2 group, x ^ᶻ γ computes the ℤ₂-power at the projection of γ — the profinite exponents of the profinite-exponentiation API (e.g. ω₂) factor through ℤ₂ here.

ℤ₂ˣ is pro-2, and the η-injectivity (part (iii))

This is a shared prerequisite for the Lemmas 3.4–3.8 proofs. Level-tracking is done algebraically (divisibility by 2^k, with unit witnesses for exact levels) — p = 2 is what makes ℤ₂ˣ pro-2: every unit is ≡ 1 (mod 2), and squaring gains exactly one level. Real norms appear only once, bridging to the open-ball description of a neighbourhood in ℤ₂ˣ.

theorem GQ2.not_isUnit_two : ¬IsUnit 2

2 is not a unit of ℤ₂.

theorem GQ2.isUnit_one_add_two_mul (x : ℤ_[2]) : IsUnit (1 + 2 * x)

1 + 2x is a unit of ℤ₂ (its residue mod 2 is 1).

theorem GQ2.two_dvd_val_sub_one (u : ℤ_[2]ˣ) : 2 ∣ ↑u - 1

Every 2-adic unit is ≡ 1 (mod 2) (p = 2: the residue field has one nonzero class).

theorem GQ2.two_pow_succ_dvd_pow_two_pow_sub_one (u : ℤ_[2]ˣ) (k : ℕ) : 2 ^ (k + 1) ∣ ↑(u ^ 2 ^ k) - 1

Level gain under 2-power powers: 2^{k+1} ∣ u^{2^k} − 1 for every u ∈ ℤ₂ˣ (squaring 1 + 2^m a gains exactly one level: (1+2^m a)² = 1 + 2^{m+1}(a + 2^{m-1}a²)).

theorem GQ2.exists_unit_pow_two_pow_sub_one (η a : ℤ_[2]ˣ) (hη : ↑η - 1 = 4 * ↑a) (k : ℕ) : ∃ (b : ℤ_[2]ˣ), ↑(η ^ 2 ^ k) - 1 = 2 ^ (k + 2) * ↑b

Exact-level version (unit-witnessed): if η − 1 = 4a with a ∈ ℤ₂ˣ (i.e. v₂(η−1) = 2 exactly), then η^{2^k} − 1 = 2^{k+2}·(unit) — the level grows by exactly one per squaring, so no 2-power power of η is 1.

theorem GQ2.dist_one_le_of_two_pow_dvd {x : ℤ_[2]} {n : ℕ} (h : 2 ^ n ∣ x - 1) : dist x 1 ≤ ↑2 ^ (-↑n)

The divisibility-to-metric bridge: 2^n ∣ x − 1 means x is within 2^{-n} of 1.

theorem GQ2.isProP_two_unitsPadicInt : IsProP 2 ℤ_[2]ˣ

ℤ₂ˣ is a pro-2 group: every finite continuous quotient of the 2-adic units is a 2-group. (Uniform annihilation: any open U ∋ 1 contains all units within 2^{-(K+1)} of 1 — in both the value and the inverse coordinate of the Units topology — and u^{2^K} ≡ 1 (mod 2^{K+1}) for every unit u.)

The profinite-group instances on ℤ₂ˣ

Mathlib provides IsTopologicalGroup αˣ ([ContinuousMul α]), CompactSpace αˣ ([T1Space α] [ContinuousMul α] [CompactSpace α]), and T2Space αˣ; total disconnectedness transfers along the embedProduct embedding. With these, zpowZtwo applies to ℤ₂ˣ.

instance GQ2.instTotallyDisconnectedSpaceMulOppositePadicIntOfNatNat_gQ2 : TotallyDisconnectedSpace ℤ_[2]ᵐᵒᵖ

instance GQ2.instTotallyDisconnectedSpaceUnitsPadicIntOfNatNat_gQ2 : TotallyDisconnectedSpace ℤ_[2]ˣ

The η-injectivity

theorem GQ2.zpowZtwo_injective_of_exact_level (η a : ℤ_[2]ˣ) (hη : ↑η - 1 = 4 * ↑a) : Function.Injective (zpowZtwo isProP_two_unitsPadicInt η)

η-injectivity: if η − 1 = 4a with a ∈ ℤ₂ˣ (equivalently v₂(η − 1) = 2 — the paper's "η topologically generates 1 + 4ℤ₂", in the form Lemma 3.5's injectivity row and Prop. 3.8's Ȳ-coordinate forcing consume), then u ↦ η ^ u is injective on ℤ₂-exponents.

Proof: a nonzero exponent factors as c = w·2^m (w ∈ ℤ₂ˣ, m = v₂(c)); η^c = (η^{2^m})^w, so η^c = 1 forces η^{2^m} = 1 (unit powers are bijective), contradicting the exact level η^{2^m} − 1 = 2^{m+2}·(unit) ≠ 0.

theorem GQ2.neg_three_inv_exact_level (y : ℤ_[2]ˣ) (hy : ↑y = -3) : ↑y⁻¹ - 1 = 4 * ↑y⁻¹

The paper's η = (−3)⁻¹ has exact level 2: η − 1 = 4·η (witness a = η itself), since η − 1 = η(1 − (−3))·… = 4η.

theorem GQ2.zpowZtwo_injective_neg_three_inv (y : ℤ_[2]ˣ) (hy : ↑y = -3) : Function.Injective (zpowZtwo isProP_two_unitsPadicInt y⁻¹)

The form consumed by the Lemmas 3.4–3.8 proofs: u ↦ ((−3)⁻¹) ^ u is injective (η = y⁻¹ for the class y = −3 of Lemma 3.5 / Prop. 3.8).

Paper-tag ledger (auto-generated by paperforge; do not edit)

• Lemma 3.5 = ⟦lem-markedinitialform⟧
• Prop 3.8 = ⟦prop-orientationlift⟧ (= proposition 3.9 in current tex)