Appendix A/B: computational cross-checks of the ω₂-marking

The paper's Appendices A–B are an explicit, finite computational verification that is independent of the proof (Remark 1.3): the auxiliary words and the relator are evaluated in finite groups, with the profinite idempotent ω₂ ∈ ℤ̂ replaced by an ordinary integer representative modulo the group's exponent (App. B: ω₂ ≡ 40491355905 (mod 85667662080)).

This file makes that finite calculus rigorous and machine-checkable:

• powOmega2_eq_one_of_odd, powOmega2_eq_self_of_orderOf_two_pow — how ω₂ acts elementwise (≡ 0 on the odd part, ≡ 1 on the 2-part); the App. A word-ledger building blocks.
• markOmega2 — the App. B computable ω₂-power x ↦ x ^ 40491355905, proved equal to powOmega2 on any group whose element orders divide 85667662080.
• concrete admissible markings verified by decide (see AppendixB examples below).

How ω₂ acts elementwise (App. A ledger, Lemma 5.1)

theorem GQ2.powOmega2_eq_one_of_odd {G : Type u_1} [Group G] {x : G} (h : Odd (orderOf x)) : powOmega2 x = 1

ω₂ ≡ 0 on the odd part. If x has odd order, then x ^ ω₂ = 1.

theorem GQ2.powOmega2_eq_self_of_orderOf_two_pow {G : Type u_1} [Group G] {x : G} {k : ℕ} (h : orderOf x = 2 ^ k) : powOmega2 x = x

ω₂ ≡ 1 on the 2-part. If x has order a power of 2, then x ^ ω₂ = x.

The Appendix-B computable ω₂-power

def GQ2.markOmega2 {G : Type u_1} [Group G] (x : G) : G

App. B representative of ω₂. The computable ω₂-power on finite groups: x ↦ x^ω₂ with ω₂ replaced by its Appendix-B integer serialization 40491355905 (valid whenever the exponent divides M = 85667662080). Unlike powOmega2 (which is noncomputable via orderOf), this is a plain group power and so evaluates by decide/#eval.

Equations

• GQ2.markOmega2 x = x ^ 40491355905

theorem GQ2.markOmega2_eq_powOmega2 {G : Type u_1} [Group G] {x : G} (h : orderOf x ∣ 85667662080) : markOmega2 x = powOmega2 x

markOmega2 agrees with the genuine powOmega2 on any element whose order divides the Appendix-B modulus M = 85667662080 (in particular on any group of exponent dividing M). This is powOmega2_pow_eq together with the verified omega2Exp 85667662080 = 40491355905.

Concrete verified admissible markings

theorem GQ2.Marking.wildRel_of_trivial_wild {G : Type u_2} [Group G] (t : Marking G) (hx0 : t.x₀ = 1) (hx1 : t.x₁ = 1) (hτ : powOmega2 t.τ = 1) : t.WildRel

If both wild generators are trivial and τ has trivial ω₂-power (e.g. τ of odd order, by powOmega2_eq_one_of_odd), then every auxiliary word collapses to 1 and the wild relation holds automatically. This is the tame-frame case of the relator evaluation.

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

• Lemma 5.1 = ⟦lem-finiteexponent⟧
• Remark 1.3 = ⟦rem-computation⟧