§8: the closed exact-image recursion (Proposition 8.9) #
The RecursionFrame on a §7 block, its derived layer and Enrichment, the boxed system
ClosedRecursion (displays (136)–(142)), the source-side input bundle RecursionInputs,
and the assembly steps partition137_of, prop_8_9_aux, stageR136_of.
Proposition 8.9: the closed exact-image recursion (displays (136)–(142)) #
Target-side data: the §7 block on 𝒴 with B = Y/R, C = Y/K, carried as a
RecursionFrame (quotient targets pinned by spec fields; the scalar characters
λ ∈ D_R = (R^∨)^C indexed by a finite type with a distinguished 0, nonzero λ
carrying their scalar central covers p_λ : B_λ ↠ B). The boxed equations are the
fields of the source-generic ClosedRecursion; prop_8_9 asserts the system for both
sources with one shared (μ, G⁰, phase family) — which is exactly how the §9 induction
consumes it (the paper pins μ = |B¹(V)||Z¹(T)| via 5.15/5.16, G⁰ as the Gauss sum of
the 7.4 form, and the family as the Δ_{χ,κ}-covers of (134); that pinning is the O-half's
construction, a flagged deviation).
The §8 recursion frame on a marked target with a §7 block: the two quotient stages
B = Y/R, C = Y/K as boundary-framed targets (pinned to 𝒴 by the spec fields), the
connecting epimorphism, the images of M = K/R and T = T₀, and the scalar character
index D_R with its central covers.
- YB : Type
The
B-stage group (paperB = Y/R). - groupB : Group self.YB
- finiteB : Finite self.YB
- topoB : TopologicalSpace self.YB
- discB : DiscreteTopology self.YB
- piB : Y →* self.YB
The projection
Y ↠ B. - piB_surj : Function.Surjective ⇑self.piB
- TB : MarkedTarget H E self.YB
The
B-stage boundary-framed target. - YC : Type
The
C-stage group (paperC = Y/K). - groupC : Group self.YC
- finiteC : Finite self.YC
- topoC : TopologicalSpace self.YC
- discC : DiscreteTopology self.YC
- piC : Y →* self.YC
The projection
Y ↠ C. - piC_surj : Function.Surjective ⇑self.piC
- TC : MarkedTarget H E self.YC
The
C-stage boundary-framed target. The connecting map
B ↠ C.- MB : Subgroup self.YB
The image of
M = K/RinB. - TBsub : Subgroup self.YB
The image of
T = T₀ = (K ⊓ S)·RinB. - DR : Type
The scalar character index
D_R = (R^∨)^C, with distinguished0. - fintypeDR : Fintype self.DR
- zeroDR : self.DR
- card_DR : Nat.card self.DR = Nat.card { R' : Subgroup Y // R'.Normal ∧ R' ≤ Blk.frattiniK ∧ R'.relIndex Blk.frattiniK ≤ 2 }
D_Rhas the size of the set ofλ-kernels:Y-normal subgroups ofRof relative index ≤ 2 (λ = 0 ↔ R' = R;Y-normality =C-invariance, thelemma_7_1_dualencoding). - scalarCover (l : self.DR) : l ≠ self.zeroDR → CentralCover self.YB
The scalar central cover
p_λ : B_λ ↠ Bof each nonzeroλ(paper §7.1: the pushoutK_λ = K/ker λ, realized asY/ker λ ↠ Y/R).
Instances For
z_R = |Z¹_{Γ,ρ}(R)| = 2^{2·dim R + dim D_R} (paper, before (136)), in card form:
|R|² · |D_R|.
Instances For
m_{Γ,λ}(B) (paper, before (136)): for λ = 0, e_Γ(B); for λ ≠ 0, the number of
boundary-framed exact-image maps onto B whose λ-scalar pushout vanishes — i.e. which
lift through p_λ (liftableCount at the top stratum).
Equations
- One or more equations did not get rendered due to their size.
Instances For
m_{Γ,λ}(J) for a proper exact-image stratum J < B (the summands of (137), computed
by (138)): boundary-framed exact-image maps onto the J-stratum lifting through p_λ.
Equations
- RF.mJ b F l h J hJ = GQ2.SectionEight.liftableCount b F RF.TB (RF.scalarCover l h) J hJ
Instances For
m_{Γ,λ}(J), totalized over all subgroups (0 when J misses the H-head — such
strata carry no boundary lifts, so the totalization is faithful).
Equations
Instances For
Z_{Γ,λ}(B/C) (paper, (137)): all p_λ-compatible lifts of boundary-framed
exact-image maps to C, without imposing generation in B — pairs of an exact-image
ρ onto the C-target and a boundary-compatible continuous lift m into B over it that
is λ-compatible (lifts through the scalar cover).
Encoding correction (deviation from the earlier encoding). The original encoding
took the cover-valued lift g itself as the pair datum; since the boundary equation of the
pulled-back target only constrains p_λ ∘ g, each λ-compatible B-lift m carries
exactly #Hom(Γ,𝔽₂) cover lifts (the z-scalar twists), so that encoding overcounts the
paper's Z_{Γ,λ}(B/C) by the factor 8 and contradicts (139) as displayed. The corrected
datum is the B-lift m with the existence of a cover lift — matching m_{Γ,λ}'s
∃-form and the paper's "compatible lifts … without imposing generation".
Equations
- One or more equations did not get rendered due to their size.
Instances For
n_{Γ,0}(ζ) for a phase cover C_ζ ↠ C ((141)/(142)): boundary-framed exact-image
maps onto the C-target that lift through the cover.
Equations
- RF.nPhase b F Cζ = Nat.card { f : GQ2.BoundaryLifts b F RF.TC // ∃ (g : Γ →ₜ* Cζ.cover), ∀ (γ : Γ), Cζ.p (g γ) = ↑↑f γ }
Instances For
The B-stage projection of a boundary lift (the Prop. 8.9 assembly, the (136) fibration map):
composing an exact-image boundary lift onto Y with π_B : Y ↠ B. Surjectivity is
inherited (π_B epi), continuity is free (Y discrete), and the boundary equation
transports along the spec fields TB_head/TB_theta.
Equations
Instances For
The frame-enrichment layer #
RecursionFrame pins the stages and the scalar covers only as bare group data; the
(139)/(140) analyses use more. First the derived layer facts — normality and
elementarity of M_B/T_B, forced by ker π_B = R = Φ(K) — then the Enrichment
structure carrying what the frame does not determine: per nonzero λ, the square form of
p_λ on M_B (§7.4; block-level constructibility = mForm_of_qbar in
GQ2/FrameEnrichment.lean), and the descended module V ≅ M_B/T_B over the C-stage
with the form q̄_λ and its fixed equivariant factor-set datum (κ⁰_{q̄_λ}, Lemma 6.1 —
the relative hypothesis of lemma_6_21, consumed by Lemma 8.7/Prop 8.8, the Prop. 8.9 assembly).
Enrichment.radData assembles the per-λ Lemma 8.6 datum; radData_noDescent_iff
aligns its descent clause with the (139)/(140) case split (the Prop. 8.9 assembly's hand-off to
lemma_8_6_local/_gammaA).
M_B ◁ B: image of the normal K under the surjection π_B.
M_B has exponent 2: squares of K lie in Φ(K) = ker π_B.
M_B is abelian: commutators of K lie in Φ(K) = ker π_B.
T_B is already the K ∩ S-image: the R-factor of T₀ = (K∩S)·R dies in B.
T_B ◁ B: image of the normal K ∩ S under the surjection π_B.
T_B ≤ M_B ((K ∩ S) ⊔ R ≤ K, via lemma_7_1_head).
ker π_{BC} = M_B: the connecting map B ↠ C has the M-layer as kernel.
π_{BC} is surjective (it covers the surjection π_C).
The head factors through π_{BC}: π^C_Y ∘ π_{BC} = π^B_Y (the spec fields + π_B
epi). Exported for the D5 boundary-framing argument (the Prop. 8.9 assembly/d6).
The decoration factors through π_{BC}: θ^C_Y ∘ π_{BC} = θ^B_Y.
Boundary-framing rides free over ρ (the Prop. 8.9 assembly, D5): a continuous hom into B lying
over a boundary-framed C-lift ρ is itself boundary-framed — both boundary components
factor through π_{BC}. This is why the IsBoundaryLift clause of zBC's pairs is
redundant, and no θ|_T hypotheses are needed in the count.
The frame enrichment (the Prop. 8.9 assembly): the per-λ data of the §8 analyses that the bare
frame does not determine. Square-form block: the form q_λ of the scalar cover on M_B
(cover square relation, T_B in the polar radical, vanishing on T_B) — with the derived
layer facts above, exactly a per-λ Lemma 8.6 datum (radData); §7.4 supplies it for the
concrete block (mForm_of_qbar). Descended block: the module V ≅ M_B/T_B over the
C-stage with the descended form q̄_λ (quadratic, nonsingular, invariant — Prop 7.4's
output) and a fixed equivariant factor-set datum for it (Lemma 6.1's κ⁰_{q̄_λ} — the
relative hypothesis of lemma_6_21, consumed by Lemma 8.7/Prop 8.8).
The square form of the scalar cover
p_λonM_B.- hq (l : RF.DR) (h : l ≠ RF.zeroDR) (x : (RF.scalarCover l h).cover) (hx : (RF.scalarCover l h).p x ∈ RF.MB) : x * x = (RF.scalarCover l h).z ^ (self.q l h ⟨(RF.scalarCover l h).p x, hx⟩).val
The cover square relation:
x̃² = z^{q_λ(x)}overM_B. - hrad (l : RF.DR) (h : l ≠ RF.zeroDR) (t : RF.YB) (ht : t ∈ RF.TBsub) (m : RF.YB) (hm : m ∈ RF.MB) : polarMul (self.q l h) (fun (a b : ↥RF.MB) => ⟨↑a * ↑b, ⋯⟩) ⟨t, ⋯⟩ ⟨m, hm⟩ = 0
T_Blies in the polar radical ofq_λ. q_λvanishes onT_B.- Vmod : Type
The descended module
V ≅ M_B/T_B(abstract carrier; the concrete frame will take Prop 7.4'sP/S-side model, whereq̄_λalready lives). - addV : AddCommGroup self.Vmod
- finV : Finite self.Vmod
The
C-stage action (conjugation, descended throughker π_{BC} = M_B).The descent surjection
M_B ↠ V.- descend_surj : Function.Surjective ⇑self.descend
ker(descend) = T_B.- descend_conj (bb : RF.YB) (m : ↥RF.MB) (hm : bb * ↑m * bb⁻¹ ∈ RF.MB) : self.descend ⟨bb * ↑m * bb⁻¹, hm⟩ = Multiplicative.ofAdd (RF.piBC bb • Multiplicative.toAdd (self.descend m))
descendintertwinesB-conjugation with the action throughπ_{BC}. The descended form
q̄_λonV.- hqbar (l : RF.DR) (h : l ≠ RF.zeroDR) (m : ↥RF.MB) : self.q l h m = self.qbar l h (Multiplicative.toAdd (self.descend m))
q_λ = q̄_λ ∘ descend. q̄_λis quadratic (polar form biadditive).q̄_λis nonsingular onV(Prop 7.4's nondegeneracy).q̄_λisC-invariant (Prop 7.4'sY-invariance, descended).The fixed equivariant factor-set datum for
q̄_λ(Lemma 6.1's base class).… satisfying Lemma 6.1's identities for
q̄_λ.
Instances For
The per-λ Lemma 8.6 datum assembled from the enrichment: cover p_λ, layers
M_B/T_B, with normality and elementarity derived from the frame and the block.
Equations
Instances For
The boxed system of Prop 8.9 for one source (Γ, b) and shared data
(μ, G⁰, phase family): the displays (136)–(140), with (141)/(142) folded into (140)
through the n_{Γ,0}-liftability form of the signed phase sum (flagged deviation, cf. the
(100)-into-(105) precedent), and all divisions multiplied out.
- eq136 : ↑(Nat.card RF.DR) * ↑(exactImageCount b F T) = ↑RF.zR * ∑ᶠ (l : RF.DR), (2 * ↑(RF.mB b F l) - ↑(exactImageCount b F RF.TB))
(136), multiplied out:
|D_R| · e_Γ(Y) = z_R · Σ_{λ ∈ D_R} (2 m_{Γ,λ}(B) − e_Γ(B)). - eq137 (l : RF.DR) (h : l ≠ RF.zeroDR) : ↑(RF.zBC b F l h) = ↑(RF.mB b F l) + ∑ᶠ (J : Subgroup RF.YB) (_ : J ∈ {J : Subgroup RF.YB | J ≠ ⊤ ∧ Subgroup.map RF.piBC J = ⊤}), ↑(RF.mJOn b F l h J)
(137), additively:
Z_{Γ,λ}(B/C) = m_{Γ,λ}(B) + Σ_{J < B, J ↠ C} m_{Γ,λ}(J)(the exact-image subtraction; strata missing theH-head contribute0through the totalizedmJOn). Index-set correction. The paper's sum runs over the proper strata surjecting ontoC(J ↠ C) — theC-level component of aZ-pair forces the image stratum ontoC, and properC-missing strata can carry nonzerom_{Γ,λ}(J), so the unrestricted sum would overcount. - eq138 (l : RF.DR) (h : l ≠ RF.zeroDR) (J : Subgroup RF.YB) (hJ : Function.Surjective ⇑(RF.TB.piY.comp J.subtype)) : 8 * RF.mJ b F l h J hJ = ∑ᶠ (J' : Subgroup (RF.scalarCover l h).cover) (_ : J' ∈ {J' : Subgroup (RF.scalarCover l h).cover | Subgroup.map (RF.scalarCover l h).p J' = J}), exactImageCountOn b F ((RF.scalarCover l h).pullTarget RF.TB) J'
(138): each proper summand of (137) opens into the eight-lift partition of the
λ-cover (Lemma 8.3's (124), instantiated atp_λ). - eq139 (l : RF.DR) (h : l ≠ RF.zeroDR) : (¬∃ (N : Subgroup (RF.scalarCover l h).cover), N.Normal ∧ Subgroup.map (RF.scalarCover l h).p N = RF.TBsub ∧ (RF.scalarCover l h).z ∉ N) → 2 * RF.zBC b F l h = Nat.card ↥RF.MB ^ 2 * exactImageCount b F RF.TC
(139): when the
λ-cover has nonzero radical edge (operationally: no descent toB/T, cf.RadicalCoverData.NoDescent), the compatible-lift count is the half-torsor value2^{2 dim M − 1} e_Γ(C), i.e.2 · Z_{Γ,λ}(B/C) = |M|² · e_Γ(C). - eq140 (l : RF.DR) (h : l ≠ RF.zeroDR) : (∃ (N : Subgroup (RF.scalarCover l h).cover), N.Normal ∧ Subgroup.map (RF.scalarCover l h).p N = RF.TBsub ∧ (RF.scalarCover l h).z ∉ N) → 2 * ↑(Nat.card DT) * ↑(RF.zBC b F l h) = ↑μ * (↑(Nat.card ↥RF.MB / Nat.card ↥RF.TBsub) * ↑(exactImageCount b F RF.TC) + G0 * ∑ᶠ (ζ : DT), (2 * ↑(RF.nPhase b F (phase l h ζ)) - ↑(exactImageCount b F RF.TC)))
(140)–(142), folded: when the
λ-cover descends (radical edge zero), the compatible-lift count is the constrained Gauss value over the per-λphase family (paper (134): the classesΔ_{χ,κ}carry the scalar-pushout classκ = κ_λof theλ-cover — a per-λ, rather than shared, family, matching the paper; seedocs/orchestration/p16d6e-assembly-plan.md§1A):2^{r+1} Z_{Γ,λ}(B/C) = μ (2^d e_Γ(C) + G⁰ Σ_{ζ ∈ D_T} (2 n_{Γ,0}(ζ_λ) − e_Γ(C))), with2^{r+1} = 2|D_T|and2^d = |M|/|T| = |V|.
Instances For
The (137) partition (the Prop. 8.9 assembly item 2): the partition137 input of RecursionInputs,
derived outright. A Z-pair is determined by its B-level lift m (the C-component is
π_{BC} ∘ m); stratifying by the exact image J = im m gives the top stratum (m_B, at
J = ⊤) plus the proper C-onto strata (m_J, via the corestriction equivalence), while
C-missing strata are empty (the pair's C-component is onto) and head-missing strata are
empty by the boundary-frame head surjectivity hhead — matching mJOn's zero branch.
The source-side input bundle of the Prop 8.9 assembly (the Prop. 8.9 assembly skeleton). Each field
is one gated derivation of the boxed recursion, with its intended supplier recorded; the
displays (137) and (138) are not inputs — prop_8_9_aux discharges them from the
proved partition137_of and lemma_8_3.
stageR136— the finalR-lifting stage: Fourier inversion (125)/lemma_8_4overD_R, thez_Rtorsor multiplicity (5.15/5.16 numerics at the abelianR), and the automatic surjectivity ofR-lifts (GQ2.eq_top_of_map_frattini_quotient_top, proved).half139— the nonzero-edge half count: thezBC ↔ MLiftsfibration bridge composed with the half-torsor Lemma 8.6 (lemma_8_6_localproved for theG_ℚ₂source;lemma_8_6_gammaA= the Γ_A half-torsor proof, gated on the Prop. 5.15 proof).phase140— the zero-edge constrained-Gauss value: the descendedV ⋊ Csplitting (lemma_6_21, proved), Lemma 8.7's affineT-lifting, the completed-square identity (135)/Prop 8.8, andlemma_8_5, summed over lower exact-image maps.
- stageR136 : ↑(Nat.card RF.DR) * ↑(exactImageCount b F T) = ↑RF.zR * ∑ᶠ (l : RF.DR), (2 * ↑(RF.mB b F l) - ↑(exactImageCount b F RF.TB))
The (136)-stage identity (gated:
lemma_8_4+z_Rnumerics + Frattini lift surjectivity). - half139 (l : RF.DR) (h : l ≠ RF.zeroDR) : (¬∃ (N : Subgroup (RF.scalarCover l h).cover), N.Normal ∧ Subgroup.map (RF.scalarCover l h).p N = RF.TBsub ∧ (RF.scalarCover l h).z ∉ N) → 2 * RF.zBC b F l h = Nat.card ↥RF.MB ^ 2 * exactImageCount b F RF.TC
The (139) half count (gated: the
zBCbridge + the source's Lemma 8.6). - phase140 (l : RF.DR) (h : l ≠ RF.zeroDR) : (∃ (N : Subgroup (RF.scalarCover l h).cover), N.Normal ∧ Subgroup.map (RF.scalarCover l h).p N = RF.TBsub ∧ (RF.scalarCover l h).z ∉ N) → 2 * ↑(Nat.card DT) * ↑(RF.zBC b F l h) = ↑μ * (↑(Nat.card ↥RF.MB / Nat.card ↥RF.TBsub) * ↑(exactImageCount b F RF.TC) + G0 * ∑ᶠ (ζ : DT), (2 * ↑(RF.nPhase b F (phase l h ζ)) - ↑(exactImageCount b F RF.TC)))
The (140) constrained-Gauss value (gated: 8.5 + 8.7 + (135)/8.8 + 6.21/6.22 chain); per-
λphase family per the paper'sΔ_{χ,κ_λ}(the Prop. 8.9 assembly amendment).
Instances For
The Prop 8.9 assembly step (the Prop. 8.9 assembly): given the source-side input bundle, the boxed
system holds — with (138) discharged from the proved lemma_8_3 (the eight-lift
partition, instantiated at each scalar cover p_λ over the B-stage target). The
side conditions (Γ profinite + t.f.g. hfg, #Hom(Γ,𝔽₂) = 8) are exactly lemma_8_3's;
both real sources satisfy them (lemma_8_2 and the boundary-frame data).
The (136) stage, combinatorial core (the Prop. 8.9 assembly item 1): the stageR136 input of
RecursionInputs follows from an obstruction-module datum for the R-stage. Given
- an
𝔽₂-moduleWwith an obstruction mapoon theB-stage lifts whose vanishing detects liftability toY(hobs), - an identification
e : D_R ≃ W^∨withe 0 = 0matching the scalar-pushout counts (hmB— "λ_* o = 0iff the lift factors through theλ-cover"), and - the constant fibre size
z_Rover liftable points (hfib— theR-lift torsor count; its nonempty-fibre surjectivity ontoYisGQ2.eq_top_of_map_frattini_quotient_top),
the display (136) follows by the liftB-fibration and the Fourier engine lemma_8_4.
The three inputs are the analytic residue of the stage: W/o/e come from the concrete
R-stage obstruction theory, hfib from the 5.15/5.16 Z¹-numerics of the source
interface.
Proposition 8.9 (closed exact-image recursion) — statement relocated to
GQ2/Prop89Close.lean (GQ2.SectionEight.prop_8_9), the Prop. 8.9 assembly capstone leaf (the
thm_4_2-relocation pattern: the statement is specialized to the concrete block frame
blockFrameImpl T Blk hE2, which this file cannot name — it sits above BlockFrameImpl.lean
in the import order). Two reviewed statement actions at the relocation
(docs/orchestration/p16d6e-assembly-plan.md §1):
- the phase family is per-
λ(phase : (l : DR) → l ≠ zeroDR → DT → CentralCover YC) — the paper's (134) classesΔ_{χ,κ}carry the scalar-pushout classκ = κ_λof theλ-cover, so the shared-family draft form was a transcription deviation (Bug-3 of the c-lane family; a shared family would force an unprovenzBC-l-independence); - the frame is the concrete block frame with hypothesis ledger
{hE2, hfgF (B1 → the §9 induction), hheadA, hheadF, hsimple, hfaith, hVne, hG0indep}and the §9 induction strengthening0 < Nat.card DTin the conclusion — general-RF(136) is not provable (no axioms tie the bare frame'sDR/zR/mBto obstruction theory; the Prop. 8.9 assembly built the R-stage againstblockFrameImplby decision), and SectionNine's inductive branch consumes the proposition exactly atblockFrame = blockFrameImpl.