theorem
Q2Presentation.Induction.sec7_xr_layer_data
{p : FramedPair}
(chief : FirstNonScalarChiefFactor p)
(K : KernelMinimal chief.toNonScalarChiefFactor)
(hR : 1 < Nat.card ↥(kernelFrattini K))
(hchar :
¬∃ (lam : Module.Dual (ZMod 2) (sec7RawTowerPacketCanonical chief K).rawModuleData.R),
lam ≠ 0 ∧ ∀ (c : (sec7RawTowerPacketCanonical chief K).rawModuleData.C),
lam ∘ₗ ↑((sec7RawTowerPacketCanonical chief K).rawActionData.actR c) = lam)
:
(∀
(g :
boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (xrKernel chief K).N ⋯ ⋯)
(TorsorProgram.quotientFrame p.fst (xrKernel chief K).N ⋯ ⋯ p.snd))
(q : Marking p.fst.Y),
(∀ (a : Gen), (QuotientGroup.mk' (xrKernel chief K).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) →
(∀ (a : Gen),
p.fst.qYMap (q a) = (ProfiniteGrp.Hom.hom p.snd.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))) →
Function.Surjective ⇑(Lifting.rowMap (xrKernel chief K) q)) ∧ ∀ (f : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))),
(∀ (y : p.fst.Y) (m : Lifting.NAdd (xrKernel chief K)), f ((Lifting.conjEndN (xrKernel chief K) y) m) = f m) → f = 0
The consolidated XR-layer statement, PROVEN (prop:defduality at
the Frattini layer in the 𝒳_R = 0 branch; manuscript l.4207–4262):
given no nonzero C-invariant duals on the raw R-module, the row
system at the Frattini kernel is surjective at every frame-compatible
marking (five-lemma + structured simple sections + the Bockstein step),
and invariant duals vanish in the consumer spelling (transport).
theorem
Q2Presentation.Induction.sec7_xrzero_cochainData_proven
{p : FramedPair}
(h : ¬ScalarTerminal p)
(chief : FirstNonScalarChiefFactor p)
(K : KernelMinimal chief.toNonScalarChiefFactor)
(hR : 1 < Nat.card ↥(kernelFrattini K))
(hchar :
¬∃ (lam : Module.Dual (ZMod 2) (sec7RawTowerPacketCanonical chief K).rawModuleData.R),
lam ≠ 0 ∧ ∀ (c : (sec7RawTowerPacketCanonical chief K).rawModuleData.C),
lam ∘ₗ ↑((sec7RawTowerPacketCanonical chief K).rawActionData.actR c) = lam)
:
∃ (kdim : ℕ),
(∀
(g :
boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (xrKernel chief K).N ⋯ ⋯)
(TorsorProgram.quotientFrame p.fst (xrKernel chief K).N ⋯ ⋯ p.snd)),
Nonempty (TorsorProgram.liftHom p.fst (xrKernel chief K).N ⋯ ⋯ boundaryPackage_GammaA p.snd g)) ∧ (∀
(g :
boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (xrKernel chief K).N ⋯ ⋯)
(TorsorProgram.quotientFrame p.fst (xrKernel chief K).N ⋯ ⋯ p.snd))
(f₀ : TorsorProgram.liftHom p.fst (xrKernel chief K).N ⋯ ⋯ boundaryPackage_GammaA p.snd g),
Nat.card (TorsorProgram.Z1 p.fst (xrKernel chief K).N ⋯ ⋯ boundaryPackage_GammaA p.snd g f₀) = 2 ^ (2 * kdim)) ∧ (∀
(g :
boundaryFramedSurj boundaryPackage_GQ2 (TorsorProgram.quotientFramedTarget p.fst (xrKernel chief K).N ⋯ ⋯)
(TorsorProgram.quotientFrame p.fst (xrKernel chief K).N ⋯ ⋯ p.snd)),
Nonempty (TorsorProgram.liftHom p.fst (xrKernel chief K).N ⋯ ⋯ boundaryPackage_GQ2 p.snd g)) ∧ ∀
(g :
boundaryFramedSurj boundaryPackage_GQ2 (TorsorProgram.quotientFramedTarget p.fst (xrKernel chief K).N ⋯ ⋯)
(TorsorProgram.quotientFrame p.fst (xrKernel chief K).N ⋯ ⋯ p.snd))
(f₀ : TorsorProgram.liftHom p.fst (xrKernel chief K).N ⋯ ⋯ boundaryPackage_GQ2 p.snd g),
Nat.card (TorsorProgram.Z1 p.fst (xrKernel chief K).N ⋯ ⋯ boundaryPackage_GQ2 p.snd g f₀) = 2 ^ (2 * kdim)
The XRZero cochain keep, PROVEN from the consolidated XR-layer keep
and the canonical local-duality keep, with kdim := dim R.