The generic (140) assembly

The source-generic wiring from the keystone chain (the Prop. 8.9 assembly) to the RecursionInputs.phase140 field, per (l, h) in the zero-edge case:

• Enrichment.descData — the DescData (En.radData l h) repackaging of the enrichment (1:1 fields; ker_piBC supplies hkerC0);
• descSigma/descSections — the chosen descended splitting (descended_splitting, Lemma 6.21) and normalized count-sections;
• phaseChi — the per-(l,h) phase-cover family ζ ↦ centralCoverOfCocycle (Δ_{ζ,κ_λ}) from the proved DeltaChi data;
• rho0_descData_rhoPrime — the transported lower map's C₀-descent is the original C-lift (rho0 ∘ rhoPrime = ρ.1.1), which makes the master count's sign match phaseSign on the nose through sign_iotaB_pullCoc_eq_lift_sign;
• hMobst_of_residues — the per-ρ phase-obstruction identity, from two_mul_card_centralImage at Δ := DeltaChi, sh := shChi, hkey := keystone;
• phase140_from_residues — the phase140-field display via phase140_of_phaseObstruction, parametric over the per-source residues {htriv, hfg, hH2, hsep, hpartial, hZcard, hGaussZ, hμ}.

All source-generic; the per-source leaves discharge the residues.

noncomputable def GQ2.SectionEight.RecursionFrame.Enrichment.descData {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) : AffineTLift.DescData (En.radData l h)

The descent datum of the enrichment (design §8): the DescData repackaging of En at (l, h) — C₀ := C-stage, piC₀ := π_{BC} (kernel M_B by ker_piBC), and the descended module/form/factor-set fields verbatim.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GQ2.SectionEight.descSigma {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (Dsc : AffineTLift.Descent (En.radData l h)) : (En.descData l h).C0 →* RF.YB ⧸ (En.radData l h).T

The chosen descended splitting σ : C₀ →* Q (Lemma 6.21 in the zero-edge regime).

Equations

• GQ2.SectionEight.descSigma En l h Dsc = ⋯.choose

theorem GQ2.SectionEight.descSigma_spec {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (Dsc : AffineTLift.Descent (En.radData l h)) (cc : (En.descData l h).C0) : (AffineTLift.piQbar (En.descData l h)) ((descSigma En l h Dsc) cc) = cc

noncomputable def GQ2.SectionEight.descSections {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (Dsc : AffineTLift.Descent (En.radData l h)) : AffineTLift.CountSections (En.descData l h) (descSigma En l h Dsc)

The chosen normalized count-sections over descSigma.

Equations

• GQ2.SectionEight.descSections En l h Dsc = ⋯.some

noncomputable def GQ2.SectionEight.phaseChi {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (Dsc : AffineTLift.Descent (En.radData l h)) (ζ : ↥(AffineTLift.TCharC (En.radData l h))) : CentralCover RF.YC

The per-(l,h) phase-cover family (the paper's ζ ↦ C_{Δ_{ζ,κ_λ}}): the twisted product of the proved total scalar phase Δ_ζ, with the cocycle law and normalizations from the keystone file.

Equations

• GQ2.SectionEight.phaseChi En l h Dsc ζ = GQ2.SectionEight.AffineTLift.centralCoverOfCocycle (GQ2.SectionEight.AffineTLift.DeltaChi (GQ2.SectionEight.descSections En l h Dsc) Dsc ⋯ ζ) ⋯ ⋯ ⋯

theorem GQ2.SectionEight.card_TCharC_pos {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) : 0 < Nat.card ↥(AffineTLift.TCharC (En.radData l h))

The phase index is nonempty: 0 < #(T^∨)^C (the §9 induction strengthening's supplier).

theorem GQ2.SectionEight.rho0_descData_rhoPrime {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} {Γ : Type} [Group Γ] [TopologicalSpace Γ] (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (ρ : BoundaryLifts b F RF.TC) (γ : Γ) : (AffineTLift.rho0 (En.descData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)) γ = ↑↑ρ γ

The lower-map roundtrip: the C₀-descent of the transported lower map is the original C-exact-image map — rho0 (descData) (rhoPrime ρ) = ρ.1.1. This is what aligns the master count's ι_Γ(ρ'^*Δ)-signs with phaseSign's lift-condition at ρ.1.1.

def GQ2.SectionEight.GaussZResidue {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} {Γ : Type} [Group Γ] [TopologicalSpace Γ] [DistribMulAction Γ (ZMod 2)] (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (G0 : ℤ) : Prop

The source-Gauss residue (the Prop. 8.9 assembly): the exact hGaussZ input of phase140_from_residues — ∑ᶠ c : Z¹_{Γ,ρ'}(V), sign(Q⁰ c) = #V · G0 at every lower map. By the Prop. 8.9 assembly's layer (I) (gaussZ_reduction) this reduces to ∑_{Z¹⧸B¹} sign(Q̄⁰) = G0, the (83)-evaluation G0 = ∓2^m (the Prop. 8.9 assembly). A named abbreviation so the prop_8_9 ledger stays readable.

Equations

• One or more equations did not get rendered due to their size.

theorem GQ2.SectionEight.hMobst_of_residues {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] [DistribMulAction Γ (ZMod 2)] [ContinuousSMul Γ (ZMod 2)] (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (Dsc : AffineTLift.Descent (En.radData l h)) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (hfg : ∃ (s : Finset Γ), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hH2 : Nat.card (ContCoh.H2 Γ (ZMod 2)) = 2) (G0 : ℤ) (hsep : ∀ (ρ : BoundaryLifts b F RF.TC) (c : AffineTLift.VCocycle (En.descData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)), (∀ (χ : ↥(AffineTLift.TCharC (En.radData l h))), AffineTLift.betaChi (descSections En l h Dsc) ⋯ χ c = 0) → AffineTLift.TLiftable ⋯ c) (hpartial : ∀ (ρ : BoundaryLifts b F RF.TC) (χ : ↥(AffineTLift.TCharC (En.radData l h))), χ ≠ 0 → ∃ (c : AffineTLift.VCocycle (En.descData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)), AffineTLift.betaChi (descSections En l h Dsc) ⋯ χ c ≠ AffineTLift.betaChi (descSections En l h Dsc) ⋯ χ 0) (hZcard : ∀ (ρ : BoundaryLifts b F RF.TC), Nat.card (AffineTLift.VCocycle (En.descData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)) = Nat.card En.Vmod * Nat.card En.Vmod) (hGaussZ : ∀ (ρ : BoundaryLifts b F RF.TC), ∑ᶠ (c : AffineTLift.VCocycle (En.descData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)), sign (AffineTLift.QZero (En.descData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ) c) = ↑(Nat.card En.Vmod) * G0) (ρ : BoundaryLifts b F RF.TC) : 2 * ↑(Nat.card ↥(AffineTLift.TCharC (En.radData l h))) * ↑(Nat.card ↑(Set.range fun (f : { f : MLifts (En.radData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ) // MLifts.Central (En.radData l h) f }) => AffineTLift.redT (RF.rhoPrime b F (En.radData l h) ⋯ ρ) ↑f)) = ↑(Nat.card En.Vmod) * (↑(Nat.card En.Vmod) + G0 * ∑ᶠ (ζ : ↥(AffineTLift.TCharC (En.radData l h))), phaseSign RF b F (phaseChi En l h Dsc ζ) ρ)

The per-ρ phase-obstruction identity from the residues (the hMobst of the paper-faithful (140) reducer): the master count two_mul_card_centralImage at the keystone data (Δ := DeltaChi, sh := shChi, hkey := keystone), with each ±1 rewritten to the signed liftability through the phaseChi-cover via the roundtrip and the sign bridge.

theorem GQ2.SectionEight.phase140_from_residues {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {T : MarkedTarget H E Y} {Blk : SectionSeven.MinimalBlock T.LY} {RF : RecursionFrame T Blk} {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] [DistribMulAction Γ (ZMod 2)] [ContinuousSMul Γ (ZMod 2)] (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (En : RF.Enrichment) (l : RF.DR) (h : l ≠ RF.zeroDR) (Dsc : AffineTLift.Descent (En.radData l h)) (htriv : ∀ (γ : Γ) (m : ZMod 2), γ • m = m) (hfg : ∃ (s : Finset Γ), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hH2 : Nat.card (ContCoh.H2 Γ (ZMod 2)) = 2) (μ₀ : ℕ) (G0 : ℤ) (hμ : ∀ (ρ : BoundaryLifts b F RF.TC), Nat.card (CentralObstruction.TCocycle (En.radData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)) = μ₀) (hsep : ∀ (ρ : BoundaryLifts b F RF.TC) (c : AffineTLift.VCocycle (En.descData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)), (∀ (χ : ↥(AffineTLift.TCharC (En.radData l h))), AffineTLift.betaChi (descSections En l h Dsc) ⋯ χ c = 0) → AffineTLift.TLiftable ⋯ c) (hpartial : ∀ (ρ : BoundaryLifts b F RF.TC) (χ : ↥(AffineTLift.TCharC (En.radData l h))), χ ≠ 0 → ∃ (c : AffineTLift.VCocycle (En.descData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)), AffineTLift.betaChi (descSections En l h Dsc) ⋯ χ c ≠ AffineTLift.betaChi (descSections En l h Dsc) ⋯ χ 0) (hZcard : ∀ (ρ : BoundaryLifts b F RF.TC), Nat.card (AffineTLift.VCocycle (En.descData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)) = Nat.card En.Vmod * Nat.card En.Vmod) (hGaussZ : ∀ (ρ : BoundaryLifts b F RF.TC), ∑ᶠ (c : AffineTLift.VCocycle (En.descData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ)), sign (AffineTLift.QZero (En.descData l h) (RF.rhoPrime b F (En.radData l h) ⋯ ρ) c) = ↑(Nat.card En.Vmod) * G0) : 2 * ↑(Nat.card ↥(AffineTLift.TCharC (En.radData l h))) * ↑(RF.zBC b F l h) = ↑(Nat.card En.Vmod * μ₀) * (↑(Nat.card ↥RF.MB / Nat.card ↥RF.TBsub) * ↑(exactImageCount b F RF.TC) + G0 * ∑ᶠ (ζ : ↥(AffineTLift.TCharC (En.radData l h))), (2 * ↑(RF.nPhase b F (phaseChi En l h Dsc ζ)) - ↑(exactImageCount b F RF.TC)))

The (140) display from the residues (the RecursionInputs.phase140 field at (l, h), per-λ family phaseChi): phase140_of_phaseObstruction at the derived hMobst, the μ-torsor input hμ, and hWV := enrichment_card_Vmod.

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

• Lemma 6.21 = ⟦lem-transgression⟧