The marked matching engine: ν-compatible correction of the B-Lab isomorphism (ticket R15)

Machinery for the fill of markedPro2_R (GQ2/Roe/MarkedPro2.lean, note §3.3 ⟦prop:markedpro2⟧). Given the abstract B-Lab isomorphism f : D_R ≅ D₀, the marked statement needs a corrected isomorphism matching the unramified markings; per the note's proof this requires (a) functoriality of the canonical (Labute) orientation across f, and (b) the (u, b)-correction of prop_3_8_classification/prop_3_8_lift. This file provides both and packages the result as the keystone exists_matching_iso.

(a) Orientation functoriality: isLabuteOrientation_comp_iso

χ₀ ∘ f is a Labute orientation of D_R, for every continuous isomorphism f : D_R ≅ D₀ — the "canonical orientations are functorial" step of the note's proof. The descent characterization (IsLabuteOrientationDatum) asks that the WordLift ℤ₂(χ) ⋊ ℤ₂ˣ-lift of the relator die for arbitrary derivation generator-values, so the proof must realize arbitrary values (Ds, Dx, Dy) at the transported generators f⁻¹-side. Route:

1. D₀-side master derivations masterH c (c ∈ ℤ₂³): continuous homs D₀ → ℤ₂(χ₀) ⋊ ℤ₂ˣ with base χ₀ and derivation generator-values c — Labute's descent for D₀, i.e. the computation 2·0 + 4·Ds + (η⁻¹ − 1)·Ds = 4Ds − 4Ds = 0 on the relator A²S⁴[S,Y] at the orientation values (−1, 1, η), fed to the universal property d0LiftHom. (The lift group carries the product topology; the pro-2 instance is the ℤ₂-by-ℤ₂ˣ extension argument isProP_two_wordLift.)
2. The evaluation matrix M : Matrix (Fin 3) (Fin 3) ℤ₂, M i j = value of the j-th basis master at the i-th transported generator f (s/x/y). M is invertible: mod 2 the masters become genuine (untwisted) 𝔽₂-characters, and a continuous hom into a finite discrete group is determined on the topological generators f (s), f (x), f (y) (mem_closure_image_gens), so the mod-2 rows span 𝔽₂³; Nakayama-style, det M ∈ ℤ₂ˣ.
3. Solve M c = (Ds, Dx, Dy), contract the three basis masters by c (masterContract, a hom by the crossed-derivation product rule), pull back along f, and evaluate on dr_relation via map_drWord.

(b) The ν-correction: exists_matching_iso

With χ₀ ∘ f = χ_R (by (a) + isLabuteOrientation_ext), the Ȳ₀-coordinate τ₂ of f(x) in D₀^{ab} is a 2-adic unit: squaring kills the torsion character, leaving X² = (η²)^{τ₂} with X ≡ 5 (mod 16) (rootX_toZModPow_four) while an even exponent would force X² ≡ 1 (mod 16). The mod-2 row analysis (same engine as (2)) makes the (S̄₀, Ȳ₀)-coordinate matrix of (f(s), f(x)) invertible, so the linear system u·σᵢ + b·τᵢ = ν_R(gen i) has a solution with u ∈ ℤ₂ˣ; prop_3_8_lift lifts (u, b) to an automorphism Ψ of D₀, and F := Ψ ∘ f matches the markings: ζ ∘ ν_{D_R} = sHom ∘ abMk ∘ F (sHom = the S̄₀-coordinate = the D₀-side unramified functional, cf. GQ2/LocalMarked.lean).

Everything here is axiom-free modulo the June-side inputs it cites (B3c/B8 via chiD0/prop_3_8_lift) and the R13b Demushkin fills cited by MarkedPro2.lean (landed 2026-07-25, sorry-free); no BLabHypothesis occurs — the abstract isomorphism is a hypothesis of the keystone.

The lift group ℤ₂ ⋊ ℤ₂ˣ as a profinite 2-group

FoxH.WordLift ℤ_[2] ℤ_[2]ˣ (GQ2/FoxHeisenberg/Basic.lean) is the crossed-derivation lift group of GQ2/Roe/CrossedDerivation.lean. There it is used purely algebraically; to run D₀'s universal property into it we equip it (locally — the finite word-cochain theory GQ2/WordCohBridge.lean uses the discrete topology on its finite instances, so these instances stay file-local) with the product topology of ℤ₂ × ℤ₂ˣ, under which it is a profinite 2-group: an extension of the pro-2 ℤ₂ˣ by the pro-2 ℤ₂.

@[implicit_reducible]

noncomputable def GQ2.instTopWordLift : TopologicalSpace (FoxH.WordLift ℤ_[2] ℤ_[2]ˣ)

Equations

• GQ2.instTopWordLift = TopologicalSpace.induced (⇑GQ2.FoxH.WordLift.equivProd) inferInstance

theorem GQ2.instTopGroupWordLift : IsTopologicalGroup (FoxH.WordLift ℤ_[2] ℤ_[2]ˣ)

theorem GQ2.instCompactSpaceWordLiftPadicIntOfNatNatUnits : CompactSpace (FoxH.WordLift ℤ_[2] ℤ_[2]ˣ)

theorem GQ2.instT2SpaceWordLiftPadicIntOfNatNatUnits : T2Space (FoxH.WordLift ℤ_[2] ℤ_[2]ˣ)

theorem GQ2.instTotallyDisconnectedSpaceWordLiftPadicIntOfNatNatUnits : TotallyDisconnectedSpace (FoxH.WordLift ℤ_[2] ℤ_[2]ˣ)

theorem GQ2.isProP_two_wordLift : IsProP 2 (FoxH.WordLift ℤ_[2] ℤ_[2]ˣ)

The lift group is pro-2 — the extension argument: in a finite quotient, the image of the offset kernel is a 2-group (isPGroup_map_of_isProP), and the quotient by it is a finite discrete quotient of ℤ₂ˣ, hence a 2-group (isProP_two_unitsPadicInt); finite extensions of 2-groups by 2-groups are 2-groups (Nat.card multiplicativity).

Small local copies of private June-side value facts

unitNegThree_val, topAbCongr_abMk and (later) the sHom/yHom generator values are private in their home files (GQ2/PropOneOneAssembly.lean, GQ2/SectionThree.lean); their proofs are one-liners over public definitions, so we re-derive them here rather than widen the June API. The d0LiftHom generator values were in the same situation when this file was written and were copied here too; they have since been de-privatized as SectionThree.d0LiftHom_A/_S/_Y (L6 cleanup) and the local copies deleted, so this file now uses the public June lemmas directly.

The master crossed derivations

The group-level canonical orientation of D₀

noncomputable def GQ2.chiD0G [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : ↑D0.toProfinite.toTop →ₜ* ℤ_[2]ˣ

The canonical orientation of D₀ at the group level: χ₀ = chiD0 ∘ abMk (generator values (−1, 1, (−3)⁻¹), from the B3c bundle).

Equations

• GQ2.chiD0G = GQ2.chiD0.comp { toMonoidHom := GQ2.SectionThree.abMk, continuous_toFun := GQ2.chiD0G._proof_1 }

The mod-2 reduction of the masters and the generation engine

@[implicit_reducible]

def GQ2.instTopZModTwo : TopologicalSpace (ZMod (2 ^ 1))

Equations

• GQ2.instTopZModTwo = ⊥

theorem GQ2.instDiscreteTopologyZModHPowNatOfNat_gQ2 : DiscreteTopology (ZMod (2 ^ 1))

The evaluation matrix and its invertibility

Orientation functoriality

theorem GQ2.isLabuteOrientation_comp_iso [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (f : ↑DR.toProfinite.toTop ≃ₜ* ↑D0.toProfinite.toTop) : IsLabuteOrientation (chiD0G.comp f.toMonoidHom)

Canonical orientations are functorial across the B-Lab isomorphism (note §3.3, step "canonical orientations are functorial"): for every continuous isomorphism f : D_R ≅ D₀, the pullback χ₀ ∘ f of the canonical orientation of D₀ is a Labute orientation of D_R — every prescribed derivation triple (Ds, Dx, Dy) is realized by contracting the D₀-side master derivations against a solution of the (invertible) evaluation-matrix system and pulling back along f, and then drWord dies on dr_relation by naturality (map_drWord).

Local copies of the sHom/yHom generator values (private in GQ2/SectionThree.lean)

The identification χ₀ ∘ f = χ_R and the Ȳ₀-coordinate parity

τ₂ is odd: the mod-16 argument

@[implicit_reducible]

def GQ2.instTopZModSixteen : TopologicalSpace (ZMod (2 ^ 4))

Equations

• GQ2.instTopZModSixteen = ⊥

theorem GQ2.instDiscreteTopologyZModHPowNatOfNat_gQ2_1 : DiscreteTopology (ZMod (2 ^ 4))

The (u, b)-correction data

The corrected isomorphism and the keystone

theorem GQ2.exists_matching_iso [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hex : Nonempty (↑DR.toProfinite.toTop ≃ₜ* ↑D0.toProfinite.toTop)) : ∃ (F : ↑DR.toProfinite.toTop ≃ₜ* ↑D0.toProfinite.toTop), SectionThree.sHom (SectionThree.abMk (F drS)) = Multiplicative.ofAdd 1 ∧ SectionThree.sHom (SectionThree.abMk (F drX)) = 1 ∧ SectionThree.sHom (SectionThree.abMk (F drY)) = 1

The matching isomorphism (⟦prop:markedpro2⟧ engine, note §3.3): from any abstract continuous isomorphism D_R ≅ D₀ (the B-Lab input) there is a marked one — a corrected F = Ψ_{u,b} ∘ f whose S̄₀-coordinate takes the unramified marking values (1, 0, 0) on the generators of D_R. (Stated on generator values; the consumer markedPro2_R runs the dr_topGen density argument against ν_{D_R}, which lives downstream.) Everything upstream (orientation functoriality, the τ₂-parity, the coordinate solve, prop_3_8_lift) is packaged here.

theorem GQ2.nuUrBar_symm_eq_sHom [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (R : LocalReciprocity) (e₁ : ↑(maxProPQuotient 2 AbsGalQ2).toProfinite.toTop ≃ₜ* ↑D0.toProfinite.toTop) (hA : ∀ (g : AbsGalQ2), (maxProPMk 2 AbsGalQ2) g = e₁.symm d0A → R.nu_ur (toAb g) = Multiplicative.ofAdd ↑(-2)) (hS : ∀ (g : AbsGalQ2), (maxProPMk 2 AbsGalQ2) g = e₁.symm d0S → R.nu_ur (toAb g) = Multiplicative.ofAdd ↑1) (hY : ∀ (g : AbsGalQ2), (maxProPMk 2 AbsGalQ2) g = e₁.symm d0Y → R.nu_ur (toAb g) = Multiplicative.ofAdd ↑0) (d : ↑D0.toProfinite.toTop) : (PropOneOne.nuUrBar R) (e₁.symm d) = SectionThree.sHom (SectionThree.abMk d)

The prop_1_1 unramified rows compute sHom — the D₀-side density bridge the markedPro2_R assembly consumes: if e₁ : G_{ℚ₂}(2) ≅ D₀ has the prop_1_1 unramified coordinates (−2, 1, 0) at (A, S₀, Y₀) (read through arbitrary lifts), then ν̄_ur ∘ e₁⁻¹ = sHom ∘ abMk everywhere (density over topGen_d0).

Stress lemmas (plan rule 9)

theorem GQ2.chiD0G_values [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : chiD0G d0A = -1 ∧ chiD0G d0S = 1 ∧ chiD0G d0Y = unitNegThree⁻¹

Stress test (group-level orientation values) ⟦eq:chi0⟧: χ₀(A, S₀, Y₀) = (−1, 1, (−3)⁻¹).

theorem GQ2.chiD0G_iso_drX [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (f : ↑DR.toProfinite.toTop ≃ₜ* ↑D0.toProfinite.toTop) : chiD0G (f drX) = Roe.chiR drX

Stress test (orientation functoriality, X-value): the pulled-back canonical orientation agrees with χ_R on the wild generator — χ₀(f(x)) = χ_R(x) = X, the Hensel root, for every continuous isomorphism f : D_R ≅ D₀.