@[reducible, inline]

noncomputable abbrev Q2Presentation.Induction.properRestrictTarget {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (J : mImageStrata chief K) : BoundaryFramedTarget

The restricted cover over an image stratum, pinned at the V1 witness.

Equations

• Q2Presentation.Induction.properRestrictTarget chief K lam hinv J = Q2Presentation.Lifting.restrictTarget (Q2Presentation.Induction.xrKernel chief K) lam hinv ↑J ⋯

@[reducible, inline]

noncomputable abbrev Q2Presentation.Induction.properRestrictKernel {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (J : mImageStrata chief K) : Lifting.ElementaryKernel (properRestrictTarget chief K lam hinv J)

Its order-2 deck kernel.

Equations

• Q2Presentation.Induction.properRestrictKernel chief K lam hinv J = Q2Presentation.Lifting.restrictKernel (Q2Presentation.Induction.xrKernel chief K) lam hinv ↑J ⋯

@[reducible, inline]

noncomputable abbrev Q2Presentation.Induction.properRestrictFrame {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (J : mImageStrata chief K) : BoundaryFrame (properRestrictTarget chief K lam hinv J)

Its frame (the parent frame, verbatim).

Equations

• Q2Presentation.Induction.properRestrictFrame chief K lam hinv J = Q2Presentation.Lifting.restrictFrame (Q2Presentation.Induction.xrKernel chief K) lam hinv ↑J ⋯ p.snd

@[reducible, inline]

abbrev Q2Presentation.Induction.properStrata {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (J : mImageStrata chief K) : Type

The R3 strata over J: subgroups of p_λ⁻¹(J) mapping onto J (the manuscript's J̃ ≤ p_λ⁻¹(J), p_λ(J̃) = J, spelled at the restricted target's subtype — design §6.6).

Equations

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

noncomputable def Q2Presentation.Induction.properStratumPair {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (J : mImageStrata chief K) (Jt : properStrata chief K lam hinv J) : FramedPair

The R3 stratum framed pair (nested exact image; measure |J̃ ∩ L̃|).

Equations

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

theorem Q2Presentation.Induction.sec7_properStratumTransform_gammaA {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (J : mImageStrata chief K) : 8 * mCount chief K lam hinv J boundaryPackage_GammaA = ∑ Jt : properStrata chief K lam hinv J, Nat.card (boundaryFramedSurj boundaryPackage_GammaA (properStratumPair chief K lam hinv J Jt).fst (properStratumPair chief K lam hinv J Jt).snd)

eq:recursionR3, candidate source: the 8-lift partition at the restricted cover over J.

theorem Q2Presentation.Induction.sec7_properStratumTransform_gq2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (J : mImageStrata chief K) : 8 * mCount chief K lam hinv J boundaryPackage_GQ2 = ∑ Jt : properStrata chief K lam hinv J, Nat.card (boundaryFramedSurj boundaryPackage_GQ2 (properStratumPair chief K lam hinv J Jt).fst (properStratumPair chief K lam hinv J Jt).snd)

eq:recursionR3, local source: the mirror for G_{ℚ₂}; the uniform 8 is cover_Z1_card_gq2, derived from the citable q2_localduality_general.

The measure lemmas (eq:properweighteddescent assembled)

theorem Q2Presentation.Induction.properStratumPair_measure_le {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (J : mImageStrata chief K) (Jt : properStrata chief K lam hinv J) : framedMeasure (properStratumPair chief K lam hinv J Jt) ≤ 2 * framedMeasure (mImageStratumPair chief K J)

Nested stratum measure ≤ 2·|J ∩ L_B| (generic bound + order-2 restricted kernel + V2's child-LY transport).

theorem Q2Presentation.Induction.properStratumPair_measure_lt {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (J : mImageStrata chief K) (hJ : ↑J ≠ ⊤) (hR : 1 < Nat.card ↥(kernelFrattini K)) (Jt : properStrata chief K lam hinv J) : framedMeasure (properStratumPair chief K lam hinv J Jt) < framedMeasure p

eq:properweighteddescent, assembled (l.4407): every R3 stratum over a PROPER image is strictly smaller than the PARENT p — on BOTH |Φ(K)|-branches (hR only, no h4, no hcard).