§A0 Char-2 and M-carrier helpers (the mIn/mOut one-spelling

bridges over the mChildDescend/mChildEquiv rfl-path — banked mixed-defeq-carrier fix-class: every A-wave statement reads THESE)

theorem Q2Presentation.Induction.chiTilde_act_of_mem {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (c : towerC K) {x : towerM K} (hx : x ∈ towerT K) : (chiTilde chief K chi) (((towerActM K) c) x) = (chiTilde chief K chi) x

χ̃-invariance of the M-action on T-elements (the gammaChiRaw_zero_on_T calculus, packaged): for x ∈ T, χ̃(c·x) = χ̃(x) — edgeTProj restricts to the identity on T, the subtype transport is sec7ActOnT_coe, and χ ∈ 𝒳_T is C-invariant (chi_act).

def Q2Presentation.Induction.mIn {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (m : towerM K) : (XRZero.xrChild chief K).fst.Y

The M-inclusion into the child (the tIn-spelling of TransgressionUnit.lean extended from T to all of M — hygiene def; the A2 calculus reads THIS spelling only).

Equations

• Q2Presentation.Induction.mIn chief K m = ↑((Q2Presentation.Induction.mChildDescend chief K) (Additive.toMul m))

theorem Q2Presentation.Induction.tIn_eq_mIn {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (t : ↥(towerT K)) : tIn chief K t = mIn chief K ↑t

tIn is mIn restricted along the T-coercion (rfl-bridge).

theorem Q2Presentation.Induction.mIn_mem {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (m : towerM K) : mIn chief K m ∈ mChild chief K

theorem Q2Presentation.Induction.mIn_add {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (m m' : towerM K) : mIn chief K (m + m') = mIn chief K m * mIn chief K m'

theorem Q2Presentation.Induction.mIn_injective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Function.Injective (mIn chief K)

theorem Q2Presentation.Induction.mIn_mk {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (m : towerM K) : (QuotientGroup.mk' (tChild chief K)) (mIn chief K m) = vInG chief K (Submodule.Quotient.mk m)

The T'-class of an mIn-value is the vInG-image of the head class (the vInG_mk readout, mIn-spelled).

theorem Q2Presentation.Induction.mIn_ofMul_symm {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (u : ↥(mChild chief K)) : mIn chief K (Additive.ofMul ((mChildEquiv chief K).symm u)) = ↑u

The mChildEquiv-roundtrip readout, stated at an ATOM subtype element (banked fix-class: never elaborate an equiv roundtrip at a set-bound compound — instantiate this lemma instead).

def Q2Presentation.Induction.mOut {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : (XRZero.xrChild chief K).fst.Y) : towerM K

The choice-packaged partial inverse of mIn (total; 0 off M' — the vOut pattern).

Equations

• Q2Presentation.Induction.mOut chief K x = if h : x ∈ Q2Presentation.Induction.mChild chief K then Additive.ofMul ((Q2Presentation.Induction.mChildEquiv chief K).symm ⟨x, h⟩) else 0

theorem Q2Presentation.Induction.mOut_def {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : (XRZero.xrChild chief K).fst.Y) : mOut chief K x = if h : x ∈ mChild chief K then Additive.ofMul ((mChildEquiv chief K).symm ⟨x, h⟩) else 0

Classical dite-form of mOut (cite this, never re-haveI a Decidable instance — the sGammaZ_def fix-class).

theorem Q2Presentation.Induction.mIn_mOut {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : (XRZero.xrChild chief K).fst.Y) (hx : x ∈ mChild chief K) : mIn chief K (mOut chief K x) = x

theorem Q2Presentation.Induction.mIn_conj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : (XRZero.xrChild chief K).fst.Y) (m : towerM K) : x * mIn chief K m * x⁻¹ = mIn chief K (((towerActM K) ((btProj chief K) ((QuotientGroup.mk' (tChild chief K)) x))) m)

Conjugation transport across mIn: conjugating an M-value by ANY child element acts by towerActM at its C-class (the mChildEquiv_conjOnMgrp intertwining, read through btProj at the T'-class — the A2 conjugation leg).

§A1 The γ-indexed chiDefect bridge (design §1.2 / unit A1: the

coboundary-difference route over the PROVEN edgeLRead_eq_chiDefect — import-only; N7 is never edited)

theorem Q2Presentation.Induction.edgeLRead_eq_chiDefect_indexed {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (chi : ↥(XT chief K)) (z : ↥(edgeZ1 chief K B ρ)) (m : ↑Γ.toProfinite.toTop → towerM K) (hmlc : IsLocallyConstant m) (hm : ∀ (γ : ↑Γ.toProfinite.toTop), Submodule.Quotient.mk (m γ) = ↑z γ) : edgeLRead chief K B ρ z chi = iotaRead Γ fun (γ γ' : ↑Γ.toProfinite.toTop) => (chiTilde chief K chi) (m γ + ((towerActM K) (lowerBar chief K B ρ γ)) (m γ') + m (γ * γ'))

A1 — the γ-indexed defect bridge: for ANY locally constant γ-indexed lift m : Γ → M of the twisted cocycle z (pointwise mk (m γ) = z γ — no set-section factorization required), the χ-constraint reading equals the ι-reading of the χ̃-pushout of the γ-indexed M-defect. Proof: against a chosen set-section the two defect cochains differ by the explicit continuous coboundary of γ ↦ χ̃(m γ − sec(z γ)) — the twisted term collapses by chiTilde_act_of_mem — and iotaRead_add_coboundary kills it.

§A2 Admissibility (design §1.2 — the one new proof): a FibHom

witness forces every χ-read to hit its χ_*e-target

def Q2Presentation.Induction.mLiftVal {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (l : mLift chief K B ρ) (γ : ↑Γ.toProfinite.toTop) : (XRZero.xrChild chief K).fst.Y

Carrier readout of an M-lift at the raw child carrier (the banked btLiftVal fix-class: only a DEF with the raw-typed signature keeps HMul homogeneous — ascriptions are impotent for instance search).

Equations

• Q2Presentation.Induction.mLiftVal chief K B ρ l γ = (ProfiniteGrp.Hom.hom ↑l) γ

theorem Q2Presentation.Induction.mLiftVal_mul {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (l : mLift chief K B ρ) (γ γ' : ↑Γ.toProfinite.toTop) : mLiftVal chief K B ρ l (γ * γ') = mLiftVal chief K B ρ l γ * mLiftVal chief K B ρ l γ'

def Q2Presentation.Induction.fibShear {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)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (Z : ZeroEdgeDescentData chief K lam hinv) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (l : mLift chief K B ρ) (γ : ↑Γ.toProfinite.toTop) : (XRZero.xrChild chief K).fst.Y

The sheared lift m̂(γ) = l(γ)·τ(ρ̄γ)⁻¹ (design §1.2: the M-valued correction of l by the pinning's τ-lift of the Csec-section).

Equations

• Q2Presentation.Induction.fibShear chief K lam hinv B Z ρ P l γ = Q2Presentation.Induction.mLiftVal chief K B ρ l γ * (P.tau (Q2Presentation.Induction.lowerBar chief K B ρ γ))⁻¹

theorem Q2Presentation.Induction.fibShear_mk {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)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (Z : ZeroEdgeDescentData chief K lam hinv) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (z : ↥(edgeZ1 chief K B ρ)) (l : mLift chief K B ρ) (hfib : FibHom chief K lam hinv B Z ρ P z ↑l) (γ : ↑Γ.toProfinite.toTop) : (QuotientGroup.mk' (tChild chief K)) (fibShear chief K lam hinv B Z ρ P l γ) = vInG chief K (↑z γ)

The shear reduces mod T' to the fibre coordinate: from FibHom and P.tau_proj, m̂(γ) has T'-class vInG(z γ) (the P.s-leg cancels).

theorem Q2Presentation.Induction.fibShear_mem {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)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (Z : ZeroEdgeDescentData chief K lam hinv) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (z : ↥(edgeZ1 chief K B ρ)) (l : mLift chief K B ρ) (hfib : FibHom chief K lam hinv B Z ρ P z ↑l) (γ : ↑Γ.toProfinite.toTop) : fibShear chief K lam hinv B Z ρ P l γ ∈ mChild chief K

The shear lands in the child M-layer (its T'-class lies in the V-layer, and T' ≤ M' absorbs the difference).

theorem Q2Presentation.Induction.fibShear_law {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)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (Z : ZeroEdgeDescentData chief K lam hinv) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (l : mLift chief K B ρ) (γ γ' : ↑Γ.toProfinite.toTop) : fibShear chief K lam hinv B Z ρ P l (γ * γ') = fibShear chief K lam hinv B Z ρ P l γ * (P.tau (lowerBar chief K B ρ γ) * fibShear chief K lam hinv B Z ρ P l γ' * (P.tau (lowerBar chief K B ρ γ))⁻¹) * tIn chief K (Z.eT (lowerBar chief K B ρ γ) (lowerBar chief K B ρ γ'))

The shear's multiplicativity defect is exactly e (the P.tau_eT calculus, group form): m̂(γγ′) = m̂(γ)·(τc m̂(γ′) τc⁻¹)· tIn(e(c,d)) at c = ρ̄γ, d = ρ̄γ′. No FibHom needed — this is the hom law of l against the pinning cocycle law alone.

def Q2Presentation.Induction.fibM {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)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (Z : ZeroEdgeDescentData chief K lam hinv) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (l : mLift chief K B ρ) : ↑Γ.toProfinite.toTop → towerM K

The γ-indexed M-lift fibM = mOut ∘ m̂ (total-function factorization — no proof-dependent subtype in the definition, so local constancy composes).

Equations

• Q2Presentation.Induction.fibM chief K lam hinv B Z ρ P l γ = Q2Presentation.Induction.mOut chief K (Q2Presentation.Induction.fibShear chief K lam hinv B Z ρ P l γ)

theorem Q2Presentation.Induction.fibM_lc {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)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (Z : ZeroEdgeDescentData chief K lam hinv) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (l : mLift chief K B ρ) : IsLocallyConstant (fibM chief K lam hinv B Z ρ P l)

theorem Q2Presentation.Induction.fibM_mIn {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)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (Z : ZeroEdgeDescentData chief K lam hinv) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (z : ↥(edgeZ1 chief K B ρ)) (l : mLift chief K B ρ) (hfib : FibHom chief K lam hinv B Z ρ P z ↑l) (γ : ↑Γ.toProfinite.toTop) : mIn chief K (fibM chief K lam hinv B Z ρ P l γ) = fibShear chief K lam hinv B Z ρ P l γ

theorem Q2Presentation.Induction.fibM_mk {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)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (Z : ZeroEdgeDescentData chief K lam hinv) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (z : ↥(edgeZ1 chief K B ρ)) (l : mLift chief K B ρ) (hfib : FibHom chief K lam hinv B Z ρ P z ↑l) (γ : ↑Γ.toProfinite.toTop) : Submodule.Quotient.mk (fibM chief K lam hinv B Z ρ P l γ) = ↑z γ

fibM lifts z pointwise through the head quotient (the A1 hm-slot).

theorem Q2Presentation.Induction.fibM_law {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)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (Z : ZeroEdgeDescentData chief K lam hinv) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (z : ↥(edgeZ1 chief K B ρ)) (l : mLift chief K B ρ) (hfib : FibHom chief K lam hinv B Z ρ P z ↑l) (γ γ' : ↑Γ.toProfinite.toTop) : fibM chief K lam hinv B Z ρ P l (γ * γ') = fibM chief K lam hinv B Z ρ P l γ + ((towerActM K) (lowerBar chief K B ρ γ)) (fibM chief K lam hinv B Z ρ P l γ') + ↑(Z.eT (lowerBar chief K B ρ γ) (lowerBar chief K B ρ γ'))

The exact M-defect law (design §1.2, additive form): fibM(γγ′) = fibM(γ) + ρ̄γ·fibM(γ′) + e(ρ̄γ, ρ̄γ′) in M, values of the correction in T — fibShear_law transported along mIn.

theorem Q2Presentation.Induction.fibHom_reads_eq {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)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (Z : ZeroEdgeDescentData chief K lam hinv) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (z : ↥(edgeZ1 chief K B ρ)) (l : mLift chief K B ρ) (hfib : FibHom chief K lam hinv B Z ρ P z ↑l) (chi : ↥(XT chief K)) : edgeLRead chief K B ρ z chi = edgeKappaRead chief K lam hinv Z B ρ chi

A2 — admissibility (design §1.2, lem:affinelifting's ⟹ half made literal): a FibHom witness over z forces every χ-constraint reading to hit its χ_*e-target. The γ-indexed defect of fibM is edgeChiE χ ON THE NOSE (fibM_law + char 2 + edgeTProj_of_mem), and A1 aligns its ι-reading with edgeLRead.

§A3–A5 The mLift-side double count (design §1.1): the pinned

σ-fibre partition and the per-fibre T'-torsor card

theorem Q2Presentation.Induction.card_fib_of_mem {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)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (Z : ZeroEdgeDescentData chief K lam hinv) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (z : ↥(edgeZ1 chief K B ρ)) (l0 : mLift chief K B ρ) (hl0 : FibHom chief K lam hinv B Z ρ P z ↑l0) (hT : Nat.card (weakLift (XRZero.xrChild chief K).fst (tChildKernel chief K) B (XRZero.xrChild chief K).snd ↑l0) = 2 ^ (2 * dimT chief K + rT chief K)) : Nat.card { l : mLift chief K B ρ // FibHom chief K lam hinv B Z ρ P z ↑l } = 2 ^ (2 * dimT chief K + rT chief K)

A3 — the nonempty fibre card: at any FibHom-witness l0 over z, the full FibHom-fibre is the T'-weak-lift torsor at l0 (the card_fib_dichotomy e2-equiv re-run at bare FibHom), of card 2^{2·dimT+rT} by the per-source hT-slot.

theorem Q2Presentation.Induction.card_mLift_eq_sum_fib {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)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (Z : ZeroEdgeDescentData chief K lam hinv) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) [Fintype ↥(edgeZ1 chief K B ρ)] [Finite (Γ ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y))] : Nat.card (mLift chief K B ρ) = ∑ z : ↥(edgeZ1 chief K B ρ), Nat.card { l : mLift chief K B ρ // FibHom chief K lam hinv B Z ρ P z ↑l }

A5 — the σ-fibre partition of the framed M-lift set over Z¹_ρ(V) through the pinned trivialization (Equiv.sigmaFiberEquiv at (edgeZ1EquivBtLift_pinned).symm ∘ modT, fibre condition rewritten by modT_eq_pinned_iff).

theorem Q2Presentation.Induction.card_mLift_eq_mul_cardA {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)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (Z : ZeroEdgeDescentData chief K lam hinv) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) [Fintype ↥(edgeZ1 chief K B ρ)] [Finite (Γ ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y))] (hT : ∀ (l0 : mLift chief K B ρ), Nat.card (weakLift (XRZero.xrChild chief K).fst (tChildKernel chief K) B (XRZero.xrChild chief K).snd ↑l0) = 2 ^ (2 * dimT chief K + rT chief K)) : Nat.card (mLift chief K B ρ) = 2 ^ (2 * dimT chief K + rT chief K) * Nat.card { z : ↥(edgeZ1 chief K B ρ) // ∃ (l : mLift chief K B ρ), FibHom chief K lam hinv B Z ρ P z ↑l }

A3+A5 assembled: the mLift card is 2^{2·dimT+rT} times the card of the admissible locus A = {z | ∃ l, FibHom z l} (empty fibres contribute 0; nonempty ones are T'-torsors).

§A6 The constraint-side count: fibres of the surjective edgeL

(multiplication form — no ℕ-subtraction anywhere)

theorem Q2Presentation.Induction.card_edgeL_fiber_mul {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)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (Z : ZeroEdgeDescentData chief K lam hinv) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (tok : IotaToken Γ) [Finite ↥(edgeZ1 chief K B ρ)] (hdel : EdgeDelSurj chief K B ρ) : Nat.card { z : ↥(edgeZ1 chief K B ρ) // (edgeL chief K B ρ tok) z = edgeKappa chief K lam hinv Z B ρ tok } * 2 ^ rT chief K = Nat.card ↥(edgeZ1 chief K B ρ)

A6 — the affine solution-set count (multiplication form): from the PROVEN ∂-surjectivity (hdel via edgeL_surjective_of_delSurj), |{z : L z = κ₀}|·2^{rT} = |Z¹_ρ(V)| — the κ₀-fibre of edgeL against |𝒳_T^∨| = 2^{rT}.

§A7 Assembly: subset + equal card ⟹ the affine iff (design §1.1

exit; source-generic core, per-source exits below)

theorem Q2Presentation.Induction.edgeAffineLifting_of_slots {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)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (Z : ZeroEdgeDescentData chief K lam hinv) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (P : ZeroEdgePinning chief K lam hinv Z) (tok : IotaToken Γ) [Fintype ↥(edgeZ1 chief K B ρ)] [Finite (Γ ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (XRZero.xrChild chief K).fst.Y))] (hdel : EdgeDelSurj chief K B ρ) (hM : Nat.card (mLift chief K B ρ) = 2 ^ (2 * dimM chief K)) (hW : Nat.card ↥(edgeZ1 chief K B ρ) = 2 ^ (2 * dimV chief K)) (hT : ∀ (l0 : mLift chief K B ρ), Nat.card (weakLift (XRZero.xrChild chief K).fst (tChildKernel chief K) B (XRZero.xrChild chief K).snd ↑l0) = 2 ^ (2 * dimT chief K + rT chief K)) : EdgeAffineLifting chief K lam hinv B Z ρ P

A7 — the source-generic dissolution core: given the token, the proven ∂-floor, and the three per-source numeric slots (|mLift| = 2^{2·dimM}, |Z¹_ρ(V)| = 2^{2·dimV}, the T'-fibre card), EdgeAffineLifting HOLDS. Double count: 2^{2·dimT+rT}·|A| = 2^{2·dimM} = 2^{2·dimV}·2^{2·dimT} and |B|·2^{rT} = 2^{2·dimV} force |A| = |B|; A2 gives A ⊆ B; finite equality of cards upgrades the inclusion to the biconditional.

The per-source exits (design §1.3 A7 / the Wave-1 deliverable):

statements binder-for-binder q2_edgeAffineLifting_gammaA/_gq2 (BlockRecursionKeeps.lean:429/:449) — the keeps-file swap replaces the axioms by these theorems with zero downstream rewiring.

theorem Q2Presentation.Induction.edgeAffineLifting_gammaA_proven {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)) (Z : ZeroEdgeDescentData chief K lam hinv) (P : ZeroEdgePinning chief K lam hinv Z) (ρ : boundaryFramedSurj boundaryPackage_GammaA (cChild chief K).fst (cChild chief K).snd) : EdgeAffineLifting chief K lam hinv boundaryPackage_GammaA Z ρ P

F-affine, candidate source — THEOREM (formerly the S9 floor q2_edgeAffineLifting_gammaA): at every pinning P of every bundle Z and every candidate lower map ρ, a twisted cocycle z ∈ Z¹_ρ(V) supports a framed M-lift through the pinned trivialization IFF its per-χ constraint readings hit the χ_*e-targets. Inputs: the token THEOREM sec7_candidate_iotaToken, the PROVEN edgeDelSurj_gammaA, and the N6-ledger cards (mChild_liftHom_card_gammaA, card_edgeZ1_gammaA, card_weakLift_tChild_gammaA). No new axiom, no Gauss content.

theorem Q2Presentation.Induction.edgeAffineLifting_gq2_proven {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)) (Z : ZeroEdgeDescentData chief K lam hinv) (P : ZeroEdgePinning chief K lam hinv Z) (ρ : boundaryFramedSurj boundaryPackage_GQ2 (cChild chief K).fst (cChild chief K).snd) : EdgeAffineLifting chief K lam hinv boundaryPackage_GQ2 Z ρ P

F-affine, local source — THEOREM (formerly the S9 floor q2_edgeAffineLifting_gq2): the G_{ℚ₂}-mirror, same statement shape. Inputs: the citable local token q2_trivialCoeff_h2_line (existing keep — no new trust), the PROVEN edgeDelSurj_gq2, and the clause-(d)-backed cards (mChild_liftHom_card_gq2, card_edgeZ1_gq2, card_weakLift_tChild_gq2).