The orientation cubic root and orientation-value arithmetic (Roe note §3.3)

Formalises the arithmetic content of ⟦prop:orientation⟧ (Proposition 3.3 of the verification note paper/roe-presentation-verification.tex), which computes the canonical Demushkin orientation χ_R of D_R on generators via Labute's descent characterisation. This file verifies the outputs of that computation — the cubic root and the unit-group facts — not the crossed-derivation derivation of the descent equations (eqs. (charrelation)/(Cx)/(Cs)/(Cy), the note's Labute step).

The note's display eq. (orientationvalues) records the generator values (S, X, Y) = (χ_R s, χ_R x, χ_R y):

Y = -X²,      X³ + 2X² + 1 = 0,      S = -X³ / (X² + X + 1),

with Z³ + 2Z² + 1 having a unique root in ℤ₂ˣ, and

X ≡ 5 (mod 16),      S ≡ 13 (mod 16),      im χ_R = {±1} × (1 + 4ℤ₂).

Main definitions

• rootX : ℤ_[2] — the unique 2-adic root X of f(Z) = Z³ + 2Z² + 1, obtained from mathlib's hensels_lemma at the approximate root 1 (‖f 1‖ = ‖4‖ < 1 = ‖f′ 1‖² = ‖7‖²);
• Sval : ℤ_[2] — S = -X³ · (X²+X+1)⁻¹, defined through the unit X²+X+1;
• Yval : ℤ_[2] — Y = -X².

Main results

• rootX_isRoot / rootX_unique — X is a root and the only root of f in ℤ₂ (mod-2 analysis: f ≡ (Z+1)(Z²+Z+1) and Z²+Z+1 has no root in 𝔽₂, so every root is ≡ 1 mod 2, hence inside the Hensel ball ‖· − 1‖ < ‖7‖ = 1 where the root is unique);
• rootX_toZModPow_four : toZModPow 4 rootX = 5 and Sval_toZModPow_four = 13 — eq. (orientationvalues)'s mod-16 congruences (decide over ZMod 16; the cubic has the unique residue 5 mod 16 and Sval is pinned by Sval_mul_denom);
• norm_rootX_sub_one : ‖rootX − 1‖ = 1/4 and norm_Sval_sub_one : ‖Sval − 1‖ = 1/4 — the v₂ = 2 facts (the "X, S topologically generate 1 + 4ℤ₂" input to the descent-depth f = 2 of ⟦cor:abstractD0⟧); packaged as the exact-level forms rootX_sub_one_eq/Sval_sub_one_eq (· − 1 = 4·unit) that a downstream zpowZtwo_injective-style argument (GQ2/ZtwoPowering.lean) consumes directly;
• denom_isUnit, rootX_isUnit, isUnit_sq_sub_self_sub_one_of_odd — the unit facts used to define Sval and to exclude the Y = +X² branch downstream.

Cross-checked against the R2 spike's independent 2-adic computation (docs/orchestration/roe-r2-spike.md): X ≡ 5 (16), S ≡ 13 (16), v₂(X−1)=v₂(S−1)=2, and the deeper X ≡ 21 (mod 32) recorded here as the rootX_toZModPow_five stress test.

All std-3 (2-adic hensels_lemma + finite decide over ZMod (2ⁿ)).

Sanity checks feeding the Hensel invocation

theorem GQ2.Roe.f_one_eq_four : 1 ^ 3 + 2 * 1 ^ 2 + 1 = 4

f(1) = 1 + 2 + 1 = 4, the numerator of the Hensel gap ‖f 1‖ = ‖4‖.

Small 2-adic helpers

The cubic root X

theorem GQ2.Roe.hensel_data : ∃ (z : ℤ_[2]), z ^ 3 + 2 * z ^ 2 + 1 = 0 ∧ ‖z - 1‖ < 1 ∧ ∀ (z' : ℤ_[2]), z' ^ 3 + 2 * z' ^ 2 + 1 = 0 → ‖z' - 1‖ < 1 → z' = z

Hensel data for f(Z) = Z³ + 2Z² + 1. Mathlib's hensels_lemma at the approximate root 1: ‖f 1‖ = ‖4‖ < 1 = ‖7‖² = ‖f′ 1‖² (with f′(1) = 7 a unit). Bundles the root, its Hensel-ball membership ‖z − 1‖ < 1, and ball-uniqueness.

noncomputable def GQ2.Roe.rootX : ℤ_[2]

The unique 2-adic root X = χ_R(x) of Z³ + 2Z² + 1, eq. (orientationvalues).

Equations

• GQ2.Roe.rootX = GQ2.Roe.hensel_data.choose

theorem GQ2.Roe.rootX_isRoot : rootX ^ 3 + 2 * rootX ^ 2 + 1 = 0

X³ + 2X² + 1 = 0 — the middle equation of eq. (orientationvalues).

theorem GQ2.Roe.rootX_dist : ‖rootX - 1‖ < 1

X lies in the Hensel ball ‖X − 1‖ < 1, i.e. X ≡ 1 mod 2.

theorem GQ2.Roe.rootX_unique {z : ℤ_[2]} (hz : z ^ 3 + 2 * z ^ 2 + 1 = 0) : z = rootX

Uniqueness of the root. Any 2-adic root of f equals X. A root z satisfies z³ ≡ 1 mod 2 (as 2z² ≡ 0), so z ≡ 1 mod 2 (the only cube root of 1 in 𝔽₂); hence z lies in the Hensel ball ‖z − 1‖ < ‖7‖ = 1 where the root is unique.

The mod-16 congruence of X and derived units

theorem GQ2.Roe.rootX_toZModPow_four : (PadicInt.toZModPow 4) rootX = 5

toZModPow 4 X = 5 — eq. (orientationvalues)'s X ≡ 5 (mod 16). The cubic r³ + 2r² + 1 = 0 has the unique solution r = 5 in ZMod 16 (decide).

theorem GQ2.Roe.rootX_toZModPow_one : (PadicInt.toZModPow 1) rootX = 1

X ≡ 1 mod 2 in ZMod 2 form (residue of the unit X).

theorem GQ2.Roe.rootX_isUnit : IsUnit rootX

X is a 2-adic unit (residue 1 mod 2).

theorem GQ2.Roe.denom_isUnit : IsUnit (rootX ^ 2 + rootX + 1)

The denominator X² + X + 1 of S is a unit (residue 1 + 1 + 1 = 1 mod 2); the "the denominator is a unit" clause following eq. (SfromX).

theorem GQ2.Roe.isUnit_sq_sub_self_sub_one_of_odd : IsUnit (rootX ^ 2 - rootX - 1)

X² − X − 1 is a unit (residue 1 mod 2); the "second factor is odd" step that kills the Y = +X² branch in the ⟦prop:orientation⟧ proof.

The value S = -X³/(X²+X+1)

noncomputable def GQ2.Roe.Sval : ℤ_[2]

S = χ_R(s) = -X³ · (X²+X+1)⁻¹, eq. (orientationvalues)/(SfromX). Defined through the unit denom_isUnit (division by a unit, no field structure needed).

Equations

• GQ2.Roe.Sval = -GQ2.Roe.rootX ^ 3 * ↑GQ2.Roe.denom_isUnit.unit⁻¹

theorem GQ2.Roe.Sval_mul_denom : Sval * (rootX ^ 2 + rootX + 1) = -rootX ^ 3

Equation form of S (preferred by downstream tickets): S · (X²+X+1) = -X³.

theorem GQ2.Roe.Sval_toZModPow_four : (PadicInt.toZModPow 4) Sval = 13

toZModPow 4 S = 13 — eq. (orientationvalues)'s S ≡ 13 (mod 16). From Sval_mul_denom reduced mod 16: S · 15 = 3, and 15 is its own inverse in ZMod 16.

The value Y = -X²

noncomputable def GQ2.Roe.Yval : ℤ_[2]

Y = χ_R(y) = -X², the first equation of eq. (orientationvalues).

Equations

• GQ2.Roe.Yval = -GQ2.Roe.rootX ^ 2

theorem GQ2.Roe.Yval_eq : Yval = -rootX ^ 2

Definitional unfolding of Y.

theorem GQ2.Roe.Yval_toZModPow_four : (PadicInt.toZModPow 4) Yval = 7

toZModPow 4 Y = 7 (Y ≡ -25 ≡ 7 mod 16).

theorem GQ2.Roe.Yval_ne_sq : Yval ≠ rootX ^ 2

Y ≠ X²: the excluded Y = +X² branch is genuinely different from Y = -X² (2X² ≠ 0 as X is a unit).

Exact-level (v₂ = 2) facts

theorem GQ2.Roe.rootX_sub_one_eq : ∃ (a : ℤ_[2]ˣ), rootX - 1 = 4 * ↑a

Exact-level form of X: X − 1 = 4·(unit). Consumed directly by a downstream zpowZtwo_injective_of_exact_level-style argument (cf. GQ2/ZtwoPowering.lean).

theorem GQ2.Roe.norm_rootX_sub_one : ‖rootX - 1‖ = 1 / 4

v₂(X − 1) = 2, i.e. ‖X − 1‖ = 1/4: X ≡ 5 (16) so X − 1 = 4·unit. The paper's "X topologically generates 1 + 4ℤ₂" input.

theorem GQ2.Roe.Sval_sub_one_eq : ∃ (a : ℤ_[2]ˣ), Sval - 1 = 4 * ↑a

Exact-level form of S: S − 1 = 4·(unit).

theorem GQ2.Roe.norm_Sval_sub_one : ‖Sval - 1‖ = 1 / 4

v₂(S − 1) = 2, i.e. ‖S − 1‖ = 1/4: S ≡ 13 (16) so S − 1 = 4·unit.

Stress test: the deeper mod-32 congruence

theorem GQ2.Roe.rootX_toZModPow_five : (PadicInt.toZModPow 5) rootX = 21

Stress test (docs/orchestration/roe-r2-spike.md §2, prec-2²²⁰ table): X ≡ 21 (mod 32). Verified by the same decide-over-ZMod 32 route directly from rootX_isRoot; 21 ≡ 5 (mod 16) cross-checks rootX_toZModPow_four and catches Newton-step sign slips.

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

• Proposition 3.3 = ⟦prop:orientation⟧
  • eq. (orientationvalues) Y = -X², X³+2X²+1 = 0, S = -X³/(X²+X+1) = Yval_eq, rootX_isRoot, Sval_mul_denom
  • X ≡ 5 (16), S ≡ 13 (16) = rootX_toZModPow_four, Sval_toZModPow_four
  • v₂(X−1) = v₂(S−1) = 2 = norm_rootX_sub_one, norm_Sval_sub_one
• Corollary 3.4 = ⟦cor:abstractD0⟧ (secondary orientation depth f = 2, consumes the above)