Skip to content

p16d2-plan.md

Latest commit

 

History

History
195 lines (166 loc) · 13.9 KB

p16d2-plan.md

File metadata and controls

195 lines (166 loc) · 13.9 KB
Raw

P-16d2 — R-stage obstruction module: reduction (landed) + construction route (escalation)

Ticket: P-16d2 (docs/p16-ticket-split.md, P-16d item 1 "sharpened residue"). Build the (W, o, e, hmB, hobs, hfib) datum that GQ2.SectionEight.stageR136_of consumes to prove the (136) display of Prop 8.9, for the concrete R-stage. Deps P-13f (prop_5_15, landed) + prop_5_16 (landed); Ax B6, B7. Owner Opus, 2026-07-05.

Status: abstract module FINISHED (std-3, sorry-free) — (136) reduced to two source residues

(2026-07-06) stageR136_ofRSepData is the finish line. Every abstractly-provable ingredient of the (W,o,e,hmB,hobs,hfib) datum is proven in GQ2/RStageObstructionBuild.lean; (136) now rests on exactly two irreducible concrete/source inputs (which the concrete 𝒴-frame, P-16d6, supplies from the arithmetic) plus hE2:

  • hsep_hom — the radical-obstruction separation: obs g = 0 ⟹ g has a homomorphism lift to Y. This is the (R^∨)^C-detection of H²(Γ,R) — a property of the concrete R + C-action, provably not derivable in the bare abstract frame (with a pair-injectivity field the assembly still hits an irreducible H¹-vanishing / C-invariance condition). homLift_of_split discharges the abstractly-provable half (splitting cochain ⟹ continuous hom lift); d6 supplies the splitting.
  • hZcount — the source Z¹-count #RCocycle = z_R (prop_5_16/prop_5_15 cl.2 + card_DR).

Proven abstract scaffolding: the obstruction map + hmB (steps 1–2), stageR136_ofRObstructionData (the assembler + easy hobs), the whole hfib fibre-torsor (fibreCocycleEquiv), hsep's Frattini/framing wrapper (liftB_fibre_nonempty_of_homLift), and homLift_of_split. d6 consumes stageR136_ofRSepData by constructing the concrete RObstructionData and discharging hsep_hom + hZcount.

(historical) Status: reduction landed std-3; datum-construction escalated

  • ✅ Reduction landed — GQ2/RStageObstruction.lean, stageR136_ofObstruction, std-3, sorry-free. It repackages stageR136_of's W/o/e interface into the natural obstruction shape and discharges the double-dual bookkeeping, so a caller need only supply the obstruction as a linear functional on the scalar-character space:

    obs : BoundaryLifts b F RF.TB → Module.Dual (ZMod 2) D_Rmod        (D_Rmod ≃ RF.DR)
hmB  : ∀ λ ≠ 0,  m_{Γ,λ}(B) = #{ g // obs g λ = 0 }
hobs : ∀ g,      obs g = 0  ↔  g lifts to Y
hfib : ∀ g,      obs g = 0  →  #(fibre of liftB over g) = z_R
⟹  (136):  |D_R|·e_Γ(Y) = z_R · Σ_λ (2 m_{Γ,λ}(B) − e_Γ(B)).

    Internally W := D_Rmodᵛ, o := obs, and e : D_R ≃ Wᵛ = D_Rmodᵛᵛ is the finite-dimensional double-dual Module.evalEquiv; hmB/hobs/hfib pass through verbatim. This is the reusable "obstruction module" object the ticket names, and it is the interface the concrete witness will target.

  • 🔨 Option A underway (user-approved 2026-07-05) — GQ2/RStageObstructionBuild.lean, std-3, sorry-free. Landed so far:

    • RCoverData RF — the compat structure (coverMap_λ : Y →* (scalarCover λ).cover with p_λ ∘ coverMap_λ = π_B), kept self-contained (no Enrichment edit; foldable in later);
    • lifts_scalarCover_of_liftB — the easy hobs direction (lifts-to-Y ⟹ lifts-through-every-p_λ);
    • trivialRCD — the M = ⊥ RadicalCoverData wrapping any bare CentralCover, which unlocks the whole CentralObstruction engine (ob, central_iff_ob_eq_zero) for plain "a hom lifts through the cover". This is the reuse hinge: scalarCover λ is a central 𝔽₂-cover of B, and its MLifts.Central at M = ⊥ is exactly the frame's mB-liftability.

    Progress on the obstruction core (GQ2/RStageObstructionBuild.lean, all std-3, sorry-free):

    1. ✅ mB ⟺ ob bridge — trivialRCD (M=⊥ cover wrapper) + central_iff_ob_eq_zero give liftsThroughCover_iff_homOb : g lifts through C ⟺ homOb C g = 0; cardTwoLinEquiv turns H²(Γ,𝔽₂) ≅ 𝔽₂ (from #H²=2).
    2. ✅ obs + hmB DONE — the extended datum RObstructionData (adds D_Rmod ≃ D_R and the pair : D_Rmod →ₗ (R→+𝔽₂) field with pair_coverMap); the single-set-lift defect rDefect; the connection homOb(scalarCover λ) g = H2mk(pair d ∘ rDefect) (homOb_eq_H2mk_pair); the obstruction functional obs : D_Rmod →ₗ 𝔽₂ (obsMapAdd additive + cardTwoLinEquiv, map_smul by the two-value case split); and hmB_holds — mB l = #{f // obs f.1.1 (toDR.symm l) = 0}, exactly stageR136_ofObstruction's hmB.
    3. ◐ hobs — the ⟸ direction DONE (folded into the assembler, step 5). The ⟹ direction is the hard separation, and its Frattini/framing wrapper is DONE (liftB_fibre_nonempty_of_homLift, std-3): a bare hom lift φ : Γ → Y of g (π_B∘φ = g) already lands in the liftB-fibre (surjective by surj_of_piB_surj = Frattini eq_top_of_map_frattini_quotient_top; framed because the framing factors through π_B via TB_head/TB_theta). Residual = the separation core: obs g = 0 ⟹ ∃ hom φ : Γ → Y with π_B∘φ = g. Route: obs g = 0 ⟺ ∀d, [pair d ∘ rDefect] = 0 ∈ H²(Γ,𝔽₂) (homOb_eq_H2mk_pair) ⟹ (separation) [rDefect] = 0 ∈ H²(Γ,R) ⟹ (coboundary) build c, set φ = c⁻¹·slift∘g. The separation is the deep piece: needs H²(Γ,R) for the g-twisted action + the (R^∨)^C-character injectivity H²(Γ,R) ↪ ∏_d H²(Γ,𝔽₂) (R elem-abelian + C-invariance of the framed obstruction) + the pushout-kernel structural link.
    4. ✅ hfib abstract torsor DONE — fibreCocycleEquiv + hfib_holds (std-3, sorry-free):
      • RCocycle RF f₀ — the R-stage torsor group Z¹_{Γ,ρ}(R) (continuous crossed 1-cocycles Γ → R for the f₀-conjugation action; u_one, twistHom);
      • R_le_ker_piY / R_le_ker_thetaY (needs hE2) — the framing preservation of R-twists;
      • surj_of_piB_surj — Frattini surjectivity;
      • fibreCocycleEquiv : {f // liftB f = g} ≃ RCocycle RF f₀.1.1 — the torsor bijection;
      • hfib_holds — #fibre = z_R, reduced to the source count #RCocycle = z_R (the 5.15/5.16 numeric + card_DR, discharged by d6 — a short citation).
    5. ✅ assemble DONE — stageR136_ofRObstructionData (std-3, sorry-free): feeds stageR136_ofObstruction with obs/hmB/(the easy hobs) discharged, reducing the entire (136) display to exactly the two hard-core hypotheses hsep (step 3 ⟹) and hfib (step 4).

    Complete + committed: steps 1–2 (obstruction map), step 5 (assembler + easy hobs), step 4 (the hfib fibre-torsor, its whole abstract content), and step 3's Frattini/framing wrapper. The single remaining piece is the hsep separation core — the deepest classical argument in §8's R-stage (the H²(Γ,R) twisted-cohomology injectivity via (R^∨)^C-characters). It needs a new H²(Γ,R) layer + the pushout-kernel structural field; a focused follow-up. hfib needs only the source Z¹-count from d6.

The gap: the scalar covers are not linked to the radical extension

RecursionFrame.scalarCover : (l : DR) → l ≠ 0 → CentralCover YB stores each p_λ : B_λ ↠ B as an abstract central 𝔽₂-cover of B. Its docstring reads "the pushout K_λ = K/ker λ, realized as Y/ker λ ↠ Y/R" — but that is documentation, not a field: nothing in the frame (or in Enrichment, which adds only the per-λ square forms q_λ/q̄_λ and factor sets dat_λ) exposes a map relating p_λ to the single radical extension Y ↠ B = Y/R (ker π_B = R = Φ(K)).

Two properties of obs depend on exactly that link and are not derivable without it:

  • (Lin) — linearity of the obstruction. We need obs g : D_R → 𝔽₂ (λ ↦ [g lifts through p_λ], as an element of D_Rᵛ) to be 𝔽₂-linear. This holds because obs g λ = λ_*(Obs_R(g)), the pushforward along λ : R → 𝔽₂ of the one radical-extension obstruction Obs_R(g) ∈ H²(Γ, R), and λ ↦ λ_* is linear (functoriality of H² in the coefficient module). If the p_λ are unrelated covers, there is no common Obs_R(g) and no reason for linearity.
  • (Sep) — the hobs separation. obs g = 0 ⟺ ∀ λ ∈ D_R, g lifts through p_λ, and we need this ⟺ g lifts to Y. With the pushout link, "lifts through every p_λ" ⟺ "Obs_R(g) dies against every λ ∈ (R^∨)^C", and the Frattini structure (R = Φ(K), eq_top_of_map_frattini_quotient_top) is what forces this to be lifting to Y. Without the link the two sides are unrelated.

Per the project rule ("if a proof needs an unstated input, that is a design escalation — flag on the board, discuss; never an axiom"), this is flagged rather than hacked.

Two ways to close it (recommend the frame extension)

Option A — extend the frame with the pushout compatibility (recommended). Add to RecursionFrame (or, less invasively, to Enrichment, keeping the bare frame untouched) a compatible realization family

cover_map : (l : DR) → (h : l ≠ 0) → Y →* (scalarCover l h).cover      -- q_λ : Y ↠ B_λ
cover_map_lifts_piB : (scalarCover l h).p ∘ cover_map l h = piB          -- p_λ ∘ q_λ = π_B
cover_map_ker : (cover_map l h).ker = (ker λ  as a subgroup of R ≤ Y)    -- kernel is ker λ

i.e. the datum that p_λ really is Y/ker λ ↠ Y/R. From it, Obs_R(g) ∈ H²(Γ,R) is the single radical obstruction and obs g λ = λ_*(Obs_R(g)) gives (Lin); (Sep) follows from ⋂_{λ∈(R^∨)^C} ker λ and the Frattini surjectivity. This is a co-owned SectionEight.lean edit to a structure — needs a fleet-lead / owner sign-off (the Enrichment-extension variant is the lighter touch, mirroring how P-16d1 added Enrichment without editing the bare frame).

Option B — build the witness only for the concrete 𝒴-frame (P-16d5/d6). There the covers are Y/ker λ by construction, so the compatibility holds definitionally and obs/(Lin)/(Sep) are provable in place; P-16d2 then reduces to "provide the concrete obs for 𝒴" and folds into the witness. Cleaner for correctness, but couples P-16d2 to d5/d6 (loses the reusable abstraction).

Construction route (once the compatibility is available)

De-risked precondition: R = Φ(K) is elementary abelian (and central in K, K⁴ = 1) by GQ2.SectionSeven.lemma_7_2 (proved, std-3): its middle conjunct is ∀ r ∈ B.R, r*r = 1. So R^∨, D_R = (R^∨)^C, and z_R = 2^{2·dim R + dim D_R} = |R|²·|D_R| are all well-founded — the obstruction/duality picture does not rest on an unverified exponent hypothesis.

  1. W, e, he0 — done, generic: stageR136_ofObstruction (this file). D_Rmod = D_R given 𝔽₂-module structure (it is (R^∨)^C, naturally a subspace of R^∨, elementary abelian by lemma_7_2); W = D_Rmodᵛ.

  2. Obs_R : BoundaryLifts(B) → H²(Γ, R) — the radical-extension obstruction, per lift g, via the pushout family (Option A/B). Per-λ, λ_*(Obs_R(g)) ∈ H²(Γ,𝔽₂) is exactly the GQ2.SectionEight.CentralObstruction.ob of the central cover p_λ (central_iff_ob_eq_zero), so obs g λ := ob_{p_λ}(g) and (Lin) is ob-functoriality in λ (the covers share the lift family through cover_map).

  3. hmB — near-definitional: m_{Γ,λ}(B) (RecursionFrame.mB) is #{g // g lifts through p_λ}, and obs g λ = 0 ⟺ g lifts through p_λ by central_iff_ob_eq_zero.

  4. hobs — (Sep): obs g = 0 ⟺ ∀λ, ob_{p_λ}(g)=0 ⟺ Obs_R(g)=0 ⟺ g lifts to Y; the last ⟺ is the pushout universal property + the Frattini surjectivity GQ2.eq_top_of_map_frattini_quotient_top (a lift's image is automatically all of Y).

  5. hfib — the z_R torsor count, this is where B6/B7 enter. The fibre of liftB over a liftable g is a torsor under the twisted cocycles Z¹(Γ, R) (the lift-difference cocycle; fiberLiftEquiv is the rank-1 𝔽₂ prototype). Its size is the 5.15/5.16 numeric: #Z¹(Γ, R) = |R|² · #(ElemDual R)^C — exactly

    • local (Γ = G_ℚ₂): GQ2.LocalLiftingDuality.card_Z1_eq / prop_5_16_bundle clause 2,
    • candidate (Γ = Γ_A): prop_5_15's IsSelfDual R clause 2 (#Z1w = |R|² · #(ElemDual R)^C),

    and #(ElemDual R)^C = |D_R| is card_DR (the C-invariant λ-kernels ↔ (R^∨)^C). Hence the fibre size is |R|² · |D_R| = z_R (RecursionFrame.zR) on the nose. So hfib is design-independent modulo the fibre-is-a-Z¹-torsor identification — and that identification uses only the honest extension Y ↠ B (RF.piB, kernel R), not the per-λ scalar covers, so it is not blocked by the compatibility gap above (only obs/hmB/hobs are). It does still need a twisted-Z¹(Γ,R)-torsor layer for R-coefficients (the repo has the rank-1 𝔽₂ prototype fiberLiftEquiv; general-R is new infra). Note R ≤ ker π_Y = L_Y (K ≤ P ≤ L_Y, so Φ(K) ≤ K ≤ L_Y), so the π_Y-framing is R-twist-invariant; the θ_Y-framing interaction is the one point to check.

Files / handoff

  • GQ2/RStageObstruction.lean — the reduction (landed, std-3). Not yet imported by GQ2.lean (leaf awaiting the P-16d6 splice, which will import GQ2.RStageObstruction); the guard scans it textually and it is violation-free.
  • Blocker owner: whoever holds the RecursionFrame/Enrichment structure (co-owned SectionEight.lean). Recommended: add the cover_map compatibility to Enrichment (light touch), then discharge steps 2–5 in a follow-up RStageObstruction-consumer, feeding stageR136_ofObstruction.