Generic helpers

noncomputable def Q2Presentation.Induction.BlockR.torsorOfEquiv {G S : Type} [AddGroup G] (e : S ≃ G) : AddTorsor G S

A nonempty set equinumerous with a group is a torsor over it.

Equations

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

noncomputable def Q2Presentation.Induction.BlockR.sigmaRestrict {ι : Type} {F : ι → Type} {P : ι → Prop} (hP : ∀ (i : ι), Nonempty (F i) → P i) : (i : ι) × F i ≃ (i : { i : ι // P i }) × F ↑i

Restrict a sigma type to the support of its fibres.

Equations

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

The cochain clauses and the torsor-data construction

(The former residual |Φ(K)| = 2 keep sec7_scalarCoverCountAgreement stood here; DELETED by the P8 surgery — audit/BLOCKR_P8_DESIGN.md §5.6. Its content is now derived through the R2–R5 children of the card-2 branch below, with the residual trust in the four coordinated keeps of Induction/BlockRecursionKeeps.lean.)

@[reducible, inline]

noncomputable abbrev Q2Presentation.Induction.BlockR.Bstar {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) : MinimalBlock p

The pinned block.

Equations

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

theorem Q2Presentation.Induction.BlockR.card_dual_eq_of_finite (W : Type) [AddCommGroup W] [Module (ZMod 2) W] [Finite W] : Nat.card (Module.Dual (ZMod 2) W) = Nat.card W

Finite 𝔽₂ duality preserves cardinality.

theorem Q2Presentation.Induction.BlockR.blockXR_eq_conjInvDuals {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) : (Bstar chief K X Fdet A Rdet N h).XR = Lifting.conjInvDuals (xrKernel chief K)

The block character space is the consumer invariant-dual space: Bstar.XR = conjInvDuals (xrKernel) — the two-sided XRTransport computation (conjOnR_eq_conjEndN_inv at y⁻¹).

theorem Q2Presentation.Induction.BlockR.blockZR_eq {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) : (Bstar chief K X Fdet A Rdet N h).zR = 2 ^ (2 * Module.finrank (ZMod 2) (Lifting.NAdd (xrKernel chief K))) * Nat.card ↥(Lifting.conjInvDuals (xrKernel chief K))

The block torsor size in the consumer spelling: z_R = 2^{2·dim R}·|𝒳_R|.

noncomputable def Q2Presentation.Induction.BlockR.blockObstructionA {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (g : boundaryFramedSurj boundaryPackage_GammaA (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd) : (Bstar chief K X Fdet A Rdet N h).obstructionSpace

The canonical candidate obstruction in block spelling: the XRObstruction defect pairing, transported along blockXR_eq_conjInvDuals.

Equations

• Q2Presentation.Induction.BlockR.blockObstructionA chief K X Fdet A Rdet N h g = Q2Presentation.Induction.xrObstructionDual chief K g ∘ₗ Submodule.inclusion ⋯

theorem Q2Presentation.Induction.BlockR.blockXR_inclusion_surjective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) : Function.Surjective ⇑(Submodule.inclusion ⋯)

The transport cast is surjective (it rides an equality).

theorem Q2Presentation.Induction.BlockR.blockObstructionA_eq_zero_iff {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (hR : 1 < Nat.card ↥(kernelFrattini K)) (g : boundaryFramedSurj boundaryPackage_GammaA (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd) : blockObstructionA chief K X Fdet A Rdet N h g = 0 ↔ Nonempty (TorsorProgram.liftHom p.fst (XRZero.NR chief K) ⋯ ⋯ boundaryPackage_GammaA p.snd g)

[A1] proven: the canonical candidate obstruction separates lift existence.

theorem Q2Presentation.Induction.BlockR.blockZ1_card_gammaA {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (hR : 1 < Nat.card ↥(kernelFrattini K)) (g : boundaryFramedSurj boundaryPackage_GammaA (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd) (f₀ : TorsorProgram.liftHom p.fst (XRZero.NR chief K) ⋯ ⋯ boundaryPackage_GammaA p.snd g) : Nat.card (TorsorProgram.Z1 p.fst (XRZero.NR chief K) ⋯ ⋯ boundaryPackage_GammaA p.snd g f₀) = (Bstar chief K X Fdet A Rdet N h).zR

[A2] proven: the uniform candidate cocycle count is z_R.

noncomputable def Q2Presentation.Induction.BlockR.blockObstructionQ {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (g : boundaryFramedSurj boundaryPackage_GQ2 (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd) : (Bstar chief K X Fdet A Rdet N h).obstructionSpace

The pinned local obstruction in block spelling: the local-duality keep's bundled witness (localObstruction, q2_localduality_general), transported along blockXR_eq_conjInvDuals — the verbatim mirror of blockObstructionA.

Equations

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

theorem Q2Presentation.Induction.BlockR.blockObstructionQ_eq_zero_iff {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (g : boundaryFramedSurj boundaryPackage_GQ2 (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd) : blockObstructionQ chief K X Fdet A Rdet N h g = 0 ↔ Nonempty (TorsorProgram.liftHom p.fst (XRZero.NR chief K) ⋯ ⋯ boundaryPackage_GQ2 p.snd g)

[Q1] pinned: the pinned local obstruction separates lift existence (the separation clause of the keep in block spelling; no hR, unlike the candidate side).

theorem Q2Presentation.Induction.BlockR.blockZ1_card_gq2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (g : boundaryFramedSurj boundaryPackage_GQ2 (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd) (f₀ : TorsorProgram.liftHom p.fst (XRZero.NR chief K) ⋯ ⋯ boundaryPackage_GQ2 p.snd g) : Nat.card (TorsorProgram.Z1 p.fst (XRZero.NR chief K) ⋯ ⋯ boundaryPackage_GQ2 p.snd g f₀) = (Bstar chief K X Fdet A Rdet N h).zR

[Q2] pinned: the uniform local cocycle count is z_R (the count clause of the keep + the 2^{2·dim R} rewrite, block spelling).

noncomputable def Q2Presentation.Induction.BlockR.blockCharDual {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (chi : Module.Dual (ZMod 2) (Bstar chief K X Fdet A Rdet N h).obstructionSpace) : ↥(Lifting.conjInvDuals (xrKernel chief K))

The invariant dual attached to a character of the block obstruction space: double-dual reflexivity (Module.evalEquiv at the finite 𝔽₂ space 𝒳_R) followed by the blockXR_eq_conjInvDuals transport — the χ ↔ λ leg of lem:obstructionseparation.

Equations

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

theorem Q2Presentation.Induction.BlockR.chi_blockObstructionA_eq {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (chi : Module.Dual (ZMod 2) (Bstar chief K X Fdet A Rdet N h).obstructionSpace) (g : boundaryFramedSurj boundaryPackage_GammaA (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd) : chi (blockObstructionA chief K X Fdet A Rdet N h g) = (xrObstructionDual chief K g) (blockCharDual chief K X Fdet A Rdet N h chi)

Characters of the candidate obstruction evaluate through the attached invariant dual (Module.apply_evalEquiv_symm_apply plus rfl-grade comp/inclusion unfolds).

theorem Q2Presentation.Induction.BlockR.chi_blockObstructionQ_eq {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (chi : Module.Dual (ZMod 2) (Bstar chief K X Fdet A Rdet N h).obstructionSpace) (g : boundaryFramedSurj boundaryPackage_GQ2 (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd) : chi (blockObstructionQ chief K X Fdet A Rdet N h g) = (localObstruction (xrKernel chief K) p.snd g) (blockCharDual chief K X Fdet A Rdet N h chi)

Characters of the pinned local obstruction evaluate through the same attached invariant dual.

theorem Q2Presentation.Induction.BlockR.blockCharDual_ne_zero {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (chi : Module.Dual (ZMod 2) (Bstar chief K X Fdet A Rdet N h).obstructionSpace) (hchi : chi ≠ 0) : ↑(blockCharDual chief K X Fdet A Rdet N h chi) ≠ 0

A nonzero character attaches a nonzero invariant dual (evalEquiv.symm is injective and the inclusion cast is value-preserving).

theorem Q2Presentation.Induction.BlockR.blockPerCharA_card_eq_coverCount {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (chi : Module.Dual (ZMod 2) (Bstar chief K X Fdet A Rdet N h).obstructionSpace) (hchi : chi ≠ 0) : Nat.card { g : boundaryFramedSurj boundaryPackage_GammaA (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd // chi (blockObstructionA chief K X Fdet A Rdet N h g) = 0 } = Nat.card { g : boundaryFramedSurj boundaryPackage_GammaA (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd // Nonempty (Lifting.scalarCoverLiftHom (xrKernel chief K) ↑(blockCharDual chief K X Fdet A Rdet N h chi) ⋯ boundaryPackage_GammaA p.snd g) }

Candidate per-character fibres are cover-lift counts (lem:obstructionseparation, candidate half, at λ := blockCharDual χ): for χ ≠ 0 the χ-fibre of the canonical candidate obstruction is the set of child maps that weakly lift through B_λ.

theorem Q2Presentation.Induction.BlockR.blockPerCharQ_card_eq_coverCount {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (chi : Module.Dual (ZMod 2) (Bstar chief K X Fdet A Rdet N h).obstructionSpace) (hchi : chi ≠ 0) : Nat.card { g : boundaryFramedSurj boundaryPackage_GQ2 (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd // chi (blockObstructionQ chief K X Fdet A Rdet N h g) = 0 } = Nat.card { g : boundaryFramedSurj boundaryPackage_GQ2 (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd // Nonempty (Lifting.scalarCoverLiftHom (xrKernel chief K) ↑(blockCharDual chief K X Fdet A Rdet N h chi) ⋯ boundaryPackage_GQ2 p.snd g) }

Local per-character fibres are cover-lift counts (the localObstruction_scalar clause of the keep at λ := blockCharDual χ).

noncomputable def Q2Presentation.Induction.BlockR.sourceBij {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (o : boundaryFramedSurj B (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd → (Bstar chief K X Fdet A Rdet N h).obstructionSpace) (hsep : ∀ (g : boundaryFramedSurj B (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd), o g = 0 ↔ Nonempty (TorsorProgram.liftHom p.fst (XRZero.NR chief K) ⋯ ⋯ B p.snd g)) : boundaryFramedSurj B p.fst p.snd ≃ (x : { g : boundaryFramedSurj B (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd // o g = 0 }) × TorsorProgram.liftHom p.fst (XRZero.NR chief K) ⋯ ⋯ B p.snd ↑x

One source's torsor bijection from the engine.

Equations

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

The per-character strata children (P8-lite, |Φ(K)| ≥ 4 branch)

For each nonzero character χ of the block obstruction space, the exact-image strata of the scalar cover B_{λ(χ)} (λ(χ) := blockCharDual χ) form a block of engine children; blockChildrenTail concatenates the blocks over a fixed enumeration of the nonzero characters, and the counting formula reads the χ-block back positionally (splitByLengths).

@[reducible, inline]

abbrev Q2Presentation.Induction.BlockR.BlockNZChar {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) : Type

The nonzero characters of the block obstruction space — the index type of the per-character strata blocks.

Equations

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

noncomputable def Q2Presentation.Induction.BlockR.blockCharIdx {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) : BlockNZChar chief K X Fdet A Rdet N h ≃ Fin (Nat.card (BlockNZChar chief K X Fdet A Rdet N h))

A fixed enumeration of the nonzero characters; the position of χ is the index of its strata block in the children tail.

Equations

• Q2Presentation.Induction.BlockR.blockCharIdx chief K X Fdet A Rdet N h = Finite.equivFin (Q2Presentation.Induction.BlockR.BlockNZChar chief K X Fdet A Rdet N h)

noncomputable def Q2Presentation.Induction.BlockR.blockCharPos {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (chi : Module.Dual (ZMod 2) (Bstar chief K X Fdet A Rdet N h).obstructionSpace) : ℕ

The block position of a character, as a total function (0 at χ = 0, where the counting formula never reads it).

Equations

• Q2Presentation.Induction.BlockR.blockCharPos chief K X Fdet A Rdet N h chi = if hchi : chi = 0 then 0 else ↑((Q2Presentation.Induction.BlockR.blockCharIdx chief K X Fdet A Rdet N h) ⟨chi, hchi⟩)

theorem Q2Presentation.Induction.BlockR.blockCharPos_of_ne {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) {chi : Module.Dual (ZMod 2) (Bstar chief K X Fdet A Rdet N h).obstructionSpace} (hchi : chi ≠ 0) : blockCharPos chief K X Fdet A Rdet N h chi = ↑((blockCharIdx chief K X Fdet A Rdet N h) ⟨chi, hchi⟩)

Value of blockCharPos at a nonzero character.

noncomputable def Q2Presentation.Induction.BlockR.blockStrataBlock {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) : List FramedPair

The strata block of the nonzero character c: the exact-image strata of the scalar cover at λ = blockCharDual c.1, as a list of framed pairs.

Equations

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

theorem Q2Presentation.Induction.BlockR.blockStrataBlock_sum_gammaA {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) : (List.map (⇑Cardinal.toNat ∘ framedCountA) (blockStrataBlock chief K X Fdet A Rdet N h c)).sum = 8 * Nat.card { g : boundaryFramedSurj boundaryPackage_GammaA (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd // Nonempty (Lifting.scalarCoverLiftHom (xrKernel chief K) ↑(blockCharDual chief K X Fdet A Rdet N h ↑c) ⋯ boundaryPackage_GammaA p.snd g) }

The c-block's A-count sum is 8·m_{A,λ(c)}(B) (sec7_scalarCoverPartition_gammaA in children-list form).

theorem Q2Presentation.Induction.BlockR.blockStrataBlock_sum_gq2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) : (List.map (⇑Cardinal.toNat ∘ framedCountQ) (blockStrataBlock chief K X Fdet A Rdet N h c)).sum = 8 * Nat.card { g : boundaryFramedSurj boundaryPackage_GQ2 (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd // Nonempty (Lifting.scalarCoverLiftHom (xrKernel chief K) ↑(blockCharDual chief K X Fdet A Rdet N h ↑c) ⋯ boundaryPackage_GQ2 p.snd g) }

The c-block's Q-count sum is 8·m_{Q,λ(c)}(B) (sec7_scalarCoverPartition_gq2 in children-list form).

theorem Q2Presentation.Induction.BlockR.blockStrataBlock_measure_lt {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (h4 : 4 ≤ Nat.card ↥(kernelFrattini K)) (c : BlockNZChar chief K X Fdet A Rdet N h) (q : FramedPair) : q ∈ blockStrataBlock chief K X Fdet A Rdet N h c → framedMeasure q < framedMeasure p

Every member of the c-block is strictly smaller once 4 ≤ |Φ(K)| (the per-child witness for the engine's small field; no stratum is assumed smaller — all are proven so through the uniform bound ≤ 2·(xrChild measure) < parent measure).

noncomputable def Q2Presentation.Induction.BlockR.blockChildrenTail {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) : List FramedPair

The full children tail: the concatenation of the strata blocks over the fixed enumeration of the nonzero characters.

Equations

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

theorem Q2Presentation.Induction.BlockR.blockChildrenTail_map_toNat {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (f : FramedPair → Cardinal.{u_1}) : List.map (⇑Cardinal.toNat ∘ f) (blockChildrenTail chief K X Fdet A Rdet N h) = List.flatMap (fun (i : Fin (Nat.card (BlockNZChar chief K X Fdet A Rdet N h))) => List.map (⇑Cardinal.toNat ∘ f) (blockStrataBlock chief K X Fdet A Rdet N h ((blockCharIdx chief K X Fdet A Rdet N h).symm i))) (List.finRange (Nat.card (BlockNZChar chief K X Fdet A Rdet N h)))

Mapping the children tail commutes with the block structure (List.map_flatMap, recorded at the tail's definitional unfolding).

theorem Q2Presentation.Induction.BlockR.blockChildrenTail_chunk {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (f : FramedPair → Cardinal.{u_1}) (c : BlockNZChar chief K X Fdet A Rdet N h) : (splitByLengths (List.map (fun (i : Fin (Nat.card (BlockNZChar chief K X Fdet A Rdet N h))) => (blockStrataBlock chief K X Fdet A Rdet N h ((blockCharIdx chief K X Fdet A Rdet N h).symm i)).length) (List.finRange (Nat.card (BlockNZChar chief K X Fdet A Rdet N h)))) (List.map (⇑Cardinal.toNat ∘ f) (blockChildrenTail chief K X Fdet A Rdet N h))).getD ↑((blockCharIdx chief K X Fdet A Rdet N h) c) [] = List.map (⇑Cardinal.toNat ∘ f) (blockStrataBlock chief K X Fdet A Rdet N h c)

Chunk readout: the c-chunk of the mapped children tail (split by the raw block lengths) is the mapped c-strata block.

theorem Q2Presentation.Induction.BlockR.blockChildrenTail_measure_lt {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (h4 : 4 ≤ Nat.card ↥(kernelFrattini K)) (c : FramedPair) : c ∈ blockChildrenTail chief K X Fdet A Rdet N h → framedMeasure c < framedMeasure p

Every member of the children tail is strictly smaller once 4 ≤ |Φ(K)|.

The card-2 R2–R5 children layer (audit/BLOCKR_P8_DESIGN.md §4)

For |Φ(K)| = 2 the children of one nonzero character χ are a TWO-LEVEL block: the R3 strata of every PROPER image stratum (enumerated by V5's properIdx), then — on the zero-edge branch of λ(χ) — the R5 phase-cover strata at the definite bundle's phase classes (enumerated by xtIdx).

@[reducible, inline]

noncomputable abbrev Q2Presentation.Induction.BlockR.blockLam {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (chi : Module.Dual (ZMod 2) (Bstar chief K X Fdet A Rdet N h).obstructionSpace) : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))

The invariant dual attached to a character, as a raw functional (the lamC of the design §3; reducible, so all P8-lite spellings unify).

Equations

• Q2Presentation.Induction.BlockR.blockLam chief K X Fdet A Rdet N h chi = ↑(Q2Presentation.Induction.BlockR.blockCharDual chief K X Fdet A Rdet N h chi)

theorem Q2Presentation.Induction.BlockR.blockLamInv {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (chi : Module.Dual (ZMod 2) (Bstar chief K X Fdet A Rdet N h).obstructionSpace) : blockLam chief K X Fdet A Rdet N h chi ∈ Lifting.conjInvDuals (xrKernel chief K)

The attached dual is conjugation-invariant (the hinvC slot).

noncomputable def Q2Presentation.Induction.BlockR.xtIdx {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : ↥(XT chief K) ≃ Fin (Nat.card ↥(XT chief K))

A fixed enumeration of 𝒳_T (mirror of properIdx); the position of χ' is its phase-chunk index.

Equations

• Q2Presentation.Induction.BlockR.xtIdx chief K = Finite.equivFin ↥(Q2Presentation.Induction.XT chief K)

noncomputable def Q2Presentation.Induction.BlockR.properSumRead {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (inner : List (List ℕ)) : ℕ

The proper-image subtraction read from an inner chunk list (Σ_{i<nJ} (chunk i).sum / 8; design §3.3).

Equations

• Q2Presentation.Induction.BlockR.properSumRead chief K inner = ∑ i ∈ Finset.range (Nat.card { J : Q2Presentation.Induction.mImageStrata chief K // ↑J ≠ ⊤ }), (inner.getD i []).sum / 8

noncomputable def Q2Presentation.Induction.BlockR.phaseSumRead {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (inner : List (List ℕ)) : ℕ

The phase-cover sum read from an inner chunk list (Σ_{j<nX} (chunk (nJ+j)).sum / 8; design §3.3's Sn).

Equations

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

noncomputable def Q2Presentation.Induction.BlockR.r2r5InnerBlocks {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) : List (List FramedPair)

The inner block list of one nonzero character (design §4.2): nJ proper-image strata blocks, then — on the zero-edge branch of λ(χ) — nX phase-cover strata blocks at the DEFINITE bundle's phase classes (else nothing; zeroEdgeZtermAt's dite matches).

Equations

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

noncomputable def Q2Presentation.Induction.BlockR.r2r5Block {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) : List FramedPair

The per-χ children block (design §4.2's r2r5Block).

Equations

• Q2Presentation.Induction.BlockR.r2r5Block chief K X Fdet A Rdet N h c = List.flatMap id (Q2Presentation.Induction.BlockR.r2r5InnerBlocks chief K X Fdet A Rdet N h c)

noncomputable def Q2Presentation.Induction.BlockR.r2r5InnerLengths {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) : List ℕ

The F-free inner length profile (the splitByLengths key).

Equations

• Q2Presentation.Induction.BlockR.r2r5InnerLengths chief K X Fdet A Rdet N h c = List.map List.length (Q2Presentation.Induction.BlockR.r2r5InnerBlocks chief K X Fdet A Rdet N h c)

noncomputable def Q2Presentation.Induction.BlockR.blockChildrenTail₂ {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) : List FramedPair

The card-2 children tail: the flatMap of the per-χ R2–R5 blocks over the SAME fixed enumeration as the 4 ≤ |Φ(K)| tail.

Equations

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

theorem Q2Presentation.Induction.BlockR.blockChildrenTail₂_map_toNat {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (f : FramedPair → Cardinal.{u_1}) : List.map (⇑Cardinal.toNat ∘ f) (blockChildrenTail₂ chief K X Fdet A Rdet N h) = List.flatMap (fun (i : Fin (Nat.card (BlockNZChar chief K X Fdet A Rdet N h))) => List.map (⇑Cardinal.toNat ∘ f) (r2r5Block chief K X Fdet A Rdet N h ((blockCharIdx chief K X Fdet A Rdet N h).symm i))) (List.finRange (Nat.card (BlockNZChar chief K X Fdet A Rdet N h)))

Mapping the card-2 tail commutes with the block structure (blockChildrenTail_map_toNat transplant).

theorem Q2Presentation.Induction.BlockR.blockChildrenTail₂_chunk {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (f : FramedPair → Cardinal.{u_1}) (c : BlockNZChar chief K X Fdet A Rdet N h) : (splitByLengths (List.map (fun (i : Fin (Nat.card (BlockNZChar chief K X Fdet A Rdet N h))) => (r2r5Block chief K X Fdet A Rdet N h ((blockCharIdx chief K X Fdet A Rdet N h).symm i)).length) (List.finRange (Nat.card (BlockNZChar chief K X Fdet A Rdet N h)))) (List.map (⇑Cardinal.toNat ∘ f) (blockChildrenTail₂ chief K X Fdet A Rdet N h))).getD ↑((blockCharIdx chief K X Fdet A Rdet N h) c) [] = List.map (⇑Cardinal.toNat ∘ f) (r2r5Block chief K X Fdet A Rdet N h c)

Outer chunk readout (blockChildrenTail_chunk transplant): the c-chunk of the mapped card-2 tail is the mapped c-block.

theorem Q2Presentation.Induction.BlockR.r2r5Block_chunk {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (f : FramedPair → Cardinal.{u_1}) (c : BlockNZChar chief K X Fdet A Rdet N h) (i : ℕ) (hi : i < (r2r5InnerBlocks chief K X Fdet A Rdet N h c).length) : (splitByLengths (r2r5InnerLengths chief K X Fdet A Rdet N h c) (List.map (⇑Cardinal.toNat ∘ f) (r2r5Block chief K X Fdet A Rdet N h c))).getD i [] = List.map (⇑Cardinal.toNat ∘ f) (r2r5InnerBlocks chief K X Fdet A Rdet N h c)[i]

Inner chunk readout (design §4.3): splitting the mapped c-block by the raw inner lengths recovers the mapped inner blocks — the generic splitByLengths_flatMap_getD at g := id.

theorem Q2Presentation.Induction.BlockR.le_length_r2r5InnerBlocks {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) : Nat.card { J : mImageStrata chief K // ↑J ≠ ⊤ } ≤ (r2r5InnerBlocks chief K X Fdet A Rdet N h c).length

The inner block list always contains the nJ proper blocks.

theorem Q2Presentation.Induction.BlockR.length_r2r5InnerBlocks_of_zeroEdge {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) (hZE : ZeroEdge chief K (blockLam chief K X Fdet A Rdet N h ↑c) ⋯) : (r2r5InnerBlocks chief K X Fdet A Rdet N h c).length = Nat.card { J : mImageStrata chief K // ↑J ≠ ⊤ } + Nat.card ↥(XT chief K)

On the zero-edge branch the inner list has exactly nJ + nX blocks.

theorem Q2Presentation.Induction.BlockR.r2r5InnerBlocks_getElem_proper {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) (i : ℕ) (hi : i < Nat.card { J : mImageStrata chief K // ↑J ≠ ⊤ }) (hi' : i < (r2r5InnerBlocks chief K X Fdet A Rdet N h c).length) : (r2r5InnerBlocks chief K X Fdet A Rdet N h c)[i] = properStrataChildren chief K (blockLam chief K X Fdet A Rdet N h ↑c) ⋯ ↑((properIdx chief K).symm ⟨i, hi⟩)

Position i < nJ of the inner list is the i-th proper block.

theorem Q2Presentation.Induction.BlockR.r2r5InnerBlocks_getElem_phase {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) (hZE : ZeroEdge chief K (blockLam chief K X Fdet A Rdet N h ↑c) ⋯) (j : ℕ) (hj : j < Nat.card ↥(XT chief K)) (hj' : Nat.card { J : mImageStrata chief K // ↑J ≠ ⊤ } + j < (r2r5InnerBlocks chief K X Fdet A Rdet N h c).length) : (r2r5InnerBlocks chief K X Fdet A Rdet N h c)[Nat.card { J : mImageStrata chief K // ↑J ≠ ⊤ } + j] = phaseStrataChildren chief K (Delta chief K (blockLam chief K X Fdet A Rdet N h ↑c) ⋯ (↑(theZeroEdgeBundle chief K (blockLam chief K X Fdet A Rdet N h ↑c) ⋯ ⋯ hZE)) ((xtIdx chief K).symm ⟨j, hj⟩)) ⋯ ⋯ ⋯

Position nJ + j of the inner list, on the zero-edge branch, is the j-th phase block at the DEFINITE bundle (getElem?-route: the dite is rewritten under getElem?, which carries no bound proof, so no dependent motive arises). Per-declaration fuel per the TransgressionCore precedent (round-1 whnf/isDefEq timeouts at this declaration).

theorem Q2Presentation.Induction.BlockR.blockChildrenTail₂_measure_lt {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (hR : 1 < Nat.card ↥(kernelFrattini K)) (q : FramedPair) : q ∈ blockChildrenTail₂ chief K X Fdet A Rdet N h → framedMeasure q < framedMeasure p

Every member of the card-2 children tail is strictly smaller at bare hR (design §4.5): proper blocks by properStrataChildren_measure_lt (the enumerated J carries J.1 ≠ ⊤ from the subtype), phase blocks by the branch-free phaseStrataChildren_measure_lt.

noncomputable def Q2Presentation.Induction.BlockR.r2r5InnerAt {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) (tt : List ℕ) : List (List ℕ)

The per-χ inner chunk list read from a tail-counts list (design §3.3's inner): the outer chunk at the χ-position, split by the raw inner lengths.

Equations

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

theorem Q2Presentation.Induction.BlockR.r2r5InnerAt_getD_realized {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (f : FramedPair → Cardinal.{u_1}) (c : BlockNZChar chief K X Fdet A Rdet N h) (i : ℕ) (hi : i < (r2r5InnerBlocks chief K X Fdet A Rdet N h c).length) : (r2r5InnerAt chief K X Fdet A Rdet N h c (List.map (⇑Cardinal.toNat ∘ f) (blockChildrenTail₂ chief K X Fdet A Rdet N h))).getD i [] = List.map (⇑Cardinal.toNat ∘ f) (r2r5InnerBlocks chief K X Fdet A Rdet N h c)[i]

Realized inner readout: at the realized card-2 tail, chunk i of r2r5InnerAt is the mapped i-th inner block (outer chunk + inner chunk, design §4.3).

noncomputable def Q2Presentation.Induction.BlockR.zeroEdgeZtermAt {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) (e : ℕ) (inner : List (List ℕ)) : ℕ

The zero-edge Z-term (design §3.3, at a nonzero character c): on the zero-edge branch of λ(c), the R4b closed form at the definite bundle and the definite sign (Sn read positionally from the inner chunks); on the nonzero-edge branch, the R4a closed form 2^{2·dimM − 1}·e.

Equations

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

theorem Q2Presentation.Induction.BlockR.zeroEdgeZtermAt_pos {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) (e : ℕ) (inner : List (List ℕ)) (hZE : ZeroEdge chief K (blockLam chief K X Fdet A Rdet N h ↑c) ⋯) : zeroEdgeZtermAt chief K X Fdet A Rdet N h c e inner = if zeroEdgeSign chief K (blockLam chief K X Fdet A Rdet N h ↑c) ⋯ ↑(theZeroEdgeBundle chief K (blockLam chief K X Fdet A Rdet N h ↑c) ⋯ ⋯ hZE) = true then (muT chief K * (2 ^ dimV chief K * e + 2 ^ (dimV chief K / 2 + 1) * phaseSumRead chief K inner) - muT chief K * 2 ^ (dimV chief K / 2) * 2 ^ rT chief K * e) / 2 ^ (rT chief K + 1) else (muT chief K * (2 ^ dimV chief K * e + 2 ^ (dimV chief K / 2) * 2 ^ rT chief K * e) - muT chief K * 2 ^ (dimV chief K / 2 + 1) * phaseSumRead chief K inner) / 2 ^ (rT chief K + 1)

zeroEdgeZtermAt, zero-edge branch.

theorem Q2Presentation.Induction.BlockR.zeroEdgeZtermAt_neg {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) (e : ℕ) (inner : List (List ℕ)) (hZE : ¬ZeroEdge chief K (blockLam chief K X Fdet A Rdet N h ↑c) ⋯) : zeroEdgeZtermAt chief K X Fdet A Rdet N h c e inner = 2 ^ (2 * dimM chief K - 1) * e

zeroEdgeZtermAt, nonzero-edge branch.

noncomputable def Q2Presentation.Induction.BlockR.cardTwoTerm {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (chi : Module.Dual (ZMod 2) (Bstar chief K X Fdet A Rdet N h).obstructionSpace) (counts : List ℕ) : ℕ

The card-2 χ ≠ 0 elementary term (design §3.3, dite-totalized in χ): zeroEdgeZterm − properTerm, both read positionally from the counts list (counts.tail.headI = the cChild count e_Γ(C), counts.tail.tail = the card-2 tail counts). At χ = 0 it is never read (the formula's χ = 0 branch fires first).

Equations

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

theorem Q2Presentation.Induction.BlockR.r2r5_properRead_gammaA {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) (i : ℕ) (hi : i < Nat.card { J : mImageStrata chief K // ↑J ≠ ⊤ }) : ((r2r5InnerAt chief K X Fdet A Rdet N h c (List.map (⇑Cardinal.toNat ∘ framedCountA) (blockChildrenTail₂ chief K X Fdet A Rdet N h))).getD i []).sum / 8 = mCount chief K (blockLam chief K X Fdet A Rdet N h ↑c) ⋯ (↑((properIdx chief K).symm ⟨i, hi⟩)) boundaryPackage_GammaA

Proper chunk i, candidate source: (chunk i).sum / 8 = m_{A,λ(c)}(J_i) (V4's transform through V5's list form; the division is exact).

theorem Q2Presentation.Induction.BlockR.r2r5_properRead_gq2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) (i : ℕ) (hi : i < Nat.card { J : mImageStrata chief K // ↑J ≠ ⊤ }) : ((r2r5InnerAt chief K X Fdet A Rdet N h c (List.map (⇑Cardinal.toNat ∘ framedCountQ) (blockChildrenTail₂ chief K X Fdet A Rdet N h))).getD i []).sum / 8 = mCount chief K (blockLam chief K X Fdet A Rdet N h ↑c) ⋯ (↑((properIdx chief K).symm ⟨i, hi⟩)) boundaryPackage_GQ2

Proper chunk i, local source.

theorem Q2Presentation.Induction.BlockR.r2r5_phaseRead_gammaA {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) (hZE : ZeroEdge chief K (blockLam chief K X Fdet A Rdet N h ↑c) ⋯) (j : ℕ) (hj : j < Nat.card ↥(XT chief K)) : ((r2r5InnerAt chief K X Fdet A Rdet N h c (List.map (⇑Cardinal.toNat ∘ framedCountA) (blockChildrenTail₂ chief K X Fdet A Rdet N h))).getD (Nat.card { J : mImageStrata chief K // ↑J ≠ ⊤ } + j) []).sum / 8 = phaseCount chief K (Delta chief K (blockLam chief K X Fdet A Rdet N h ↑c) ⋯ (↑(theZeroEdgeBundle chief K (blockLam chief K X Fdet A Rdet N h ↑c) ⋯ ⋯ hZE)) ((xtIdx chief K).symm ⟨j, hj⟩)) ⋯ ⋯ ⋯ boundaryPackage_GammaA

Phase chunk j, candidate source, zero-edge branch: (chunk (nJ+j)).sum / 8 = n_{A,0}(Δ_{χ'_j,κ}) at the definite bundle.

theorem Q2Presentation.Induction.BlockR.r2r5_phaseRead_gq2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) (hZE : ZeroEdge chief K (blockLam chief K X Fdet A Rdet N h ↑c) ⋯) (j : ℕ) (hj : j < Nat.card ↥(XT chief K)) : ((r2r5InnerAt chief K X Fdet A Rdet N h c (List.map (⇑Cardinal.toNat ∘ framedCountQ) (blockChildrenTail₂ chief K X Fdet A Rdet N h))).getD (Nat.card { J : mImageStrata chief K // ↑J ≠ ⊤ } + j) []).sum / 8 = phaseCount chief K (Delta chief K (blockLam chief K X Fdet A Rdet N h ↑c) ⋯ (↑(theZeroEdgeBundle chief K (blockLam chief K X Fdet A Rdet N h ↑c) ⋯ ⋯ hZE)) ((xtIdx chief K).symm ⟨j, hj⟩)) ⋯ ⋯ ⋯ boundaryPackage_GQ2

Phase chunk j, local source, zero-edge branch.

theorem Q2Presentation.Induction.BlockR.cardTwoRealizedA {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) : Nat.card { g : boundaryFramedSurj boundaryPackage_GammaA (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd // Nonempty (Lifting.scalarCoverLiftHom (xrKernel chief K) (blockLam chief K X Fdet A Rdet N h ↑c) ⋯ boundaryPackage_GammaA p.snd g) } = zeroEdgeZtermAt chief K X Fdet A Rdet N h c (eC chief K boundaryPackage_GammaA) (r2r5InnerAt chief K X Fdet A Rdet N h c (List.map (⇑Cardinal.toNat ∘ framedCountA) (blockChildrenTail₂ chief K X Fdet A Rdet N h))) - properSumRead chief K (r2r5InnerAt chief K X Fdet A Rdet N h c (List.map (⇑Cardinal.toNat ∘ framedCountA) (blockChildrenTail₂ chief K X Fdet A Rdet N h)))

The card-2 candidate realization (design §6.2, candidate column): m_{A,λ(c)}(B) = zeroEdgeZterm − properTerm at the realized children counts. R2 (sec7_properImageSubtraction_gammaA) + R3 readouts are PROVEN; the branch step consumes exactly keep 1 (through the recovered sec7_edgeHalving_gammaA) on ¬ZeroEdge and keep 3 (through theZeroEdgeBundle_countA) on ZeroEdge.

theorem Q2Presentation.Induction.BlockR.cardTwoRealizedQ {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (c : BlockNZChar chief K X Fdet A Rdet N h) : Nat.card { g : boundaryFramedSurj boundaryPackage_GQ2 (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd // Nonempty (Lifting.scalarCoverLiftHom (xrKernel chief K) (blockLam chief K X Fdet A Rdet N h ↑c) ⋯ boundaryPackage_GQ2 p.snd g) } = zeroEdgeZtermAt chief K X Fdet A Rdet N h c (eC chief K boundaryPackage_GQ2) (r2r5InnerAt chief K X Fdet A Rdet N h c (List.map (⇑Cardinal.toNat ∘ framedCountQ) (blockChildrenTail₂ chief K X Fdet A Rdet N h))) - properSumRead chief K (r2r5InnerAt chief K X Fdet A Rdet N h c (List.map (⇑Cardinal.toNat ∘ framedCountQ) (blockChildrenTail₂ chief K X Fdet A Rdet N h)))

The card-2 local realization (design §6.2, local column): mirror of cardTwoRealizedA, consuming exactly keep 2 (q2_edgeHalving) on ¬ZeroEdge and keep 4 (through theZeroEdgeBundle_countQ, at the SAME definite bundle as the candidate side) on ZeroEdge.

noncomputable def Q2Presentation.Induction.BlockR.blockLiftTorsorData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (hR : 1 < Nat.card ↥(kernelFrattini K)) : CentralCoverLiftTorsorData (Bstar chief K X Fdet A Rdet N h)

The §8 lift-torsor data over the pinned block (hoisted from the packet proof): candidate side fully proven ([A1]/[A2] + sourceBij), local side from the PINNED obstruction ([Q1]/[Q2] + sourceBij); the common cocycle model is (Fin dimExp → 𝔽₂) × 𝒳_R^∨, of size z_R.

Equations

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

noncomputable def Q2Presentation.Induction.BlockR.blockCountingPartialFormula {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (L : CentralCoverLiftTorsorData (Bstar chief K X Fdet A Rdet N h)) (C : CentralCoverChildrenData (Bstar chief K X Fdet A Rdet N h)) : CentralCoverSourcePartialFormula (Bstar chief K X Fdet A Rdet N h) L C

The split counting formula (P8-lite): at χ = 0 the partial count is the CHILD count (counts.headI — threaded through children, so the engine's induction hypothesis supplies the source-agreement there, m_{Γ,0}(B) = e_Γ(B), prop:finalfourier l.4249); at χ ≠ 0 with 4 ≤ |Φ(K)| it is the χ-strata chunk sum of the children counts divided by 8 (eq:covertransform at the scalar cover B_{λ(χ)}: the strata are children, so the engine IH supplies the per-stratum source-agreement, and the division is exact — at the realized lists the numerator is 8·m_{Γ,λ(χ)}(B) by sec7_scalarCoverPartition_gammaA/gq2); at χ ≠ 0 with |Φ(K)| = 2 it is the R2–R5 recursion term cardTwoTerm (design §3.3): zeroEdgeZterm − properTerm, both read positionally from the card-2 children counts — one shared source-independent term, so partialRecipe_of_sourceAgreement … rfl survives unchanged.

Equations

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

theorem Q2Presentation.Induction.BlockR.blockRealizationPacket_proven {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (X : MinimalBlockPreheadInvariantCharacterData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (Fdet : MinimalBlockPreheadExtraspecialEquivariantFamilyData (sec7RawTowerPacketCanonical chief K).preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData Fdet) (Rdet : MinimalBlockPreheadExtraspecialRadicalData Fdet) (N : MinimalBlockPreheadExtraspecialNonzeroData Fdet) (h : ¬ScalarTerminal p) (hR : 1 < Nat.card ↥(kernelFrattini K)) : Nonempty ((L : CentralCoverLiftTorsorData (Bstar chief K X Fdet A Rdet N h)) ×' (C : CentralCoverChildrenData (Bstar chief K X Fdet A Rdet N h)) ×' CentralCoverCandidatePartialFormulaRealization (Bstar chief K X Fdet A Rdet N h) L C (blockCountingPartialFormula chief K X Fdet A Rdet N h L C) ×' CentralCoverLocalPartialFormulaRealization (Bstar chief K X Fdet A Rdet N h) L C (blockCountingPartialFormula chief K X Fdet A Rdet N h L C))

The block realization packet, PROVEN over the engine, carrying BOTH source realizations of the split counting formula: candidate side fully proven ([A1]/[A2] theorems + the child-count identity at χ = 0), local side from the PINNED obstruction ([Q1]/[Q2] keep-clause theorems

• the proven χ = 0 child-count identity). The χ ≠ 0 branch converts to per-λ cover-lift counts on both sides (blockPerChar*_card_eq_coverCount) and is then closed through the |Φ(K)| case split (P8-lite, audit/BLOCKR_P8LITE_DESIGN.md):

• at 4 ≤ |Φ(K)| — WITHOUT any keep: the scalar-cover strata are children (each with the PROVEN strict-decrease witness ≤ 2·(xrChild measure) < parent measure), and BOTH realizations are the eight-lift partition theorems sec7_scalarCoverPartition_gammaA/gq2 read through the positional chunk of the children counts list, so the engine's strong induction (boundaryFramed_counts_equal_corrected) derives the per-character source-agreement stratum-by-stratum;
• at |Φ(K)| = 2 (the exact complement, Φ(K) ≤ L_Y being a 2-group) — the R2–R5 recursion (audit/BLOCKR_P8_DESIGN.md §6.2): children are xrChild :: cChild :: blockChildrenTail₂ (proper R3 strata + zero-edge R5 phase strata, all strictly smaller at bare hR), and each source's realization is blockPerChar*_card_eq_coverCount composed with cardTwoRealizedA/Q — R2 subtraction and all chunk readouts PROVEN, the edge branch closed per source by exactly the four coordinated keeps of Induction/BlockRecursionKeeps.lean (candidate: sec7_edgeTwistFlip_gammaA via the proven flip involution, sec7_zeroEdgeCount_gammaA; local: q2_edgeHalving, q2_zeroEdgeCount — both zero-edge keeps at the SAME definite pinned bundle theZeroEdgeBundle and definite sign zeroEdgeSign). The former residual count-agreement keep is DELETED: agreement is now derived per child by the engine IH. hcard (card_kernelFrattini_eq_two) is no longer consumed by an axiom; the branch hypotheses used are hR and h4.

The rewired branch

theorem Q2Presentation.Induction.BlockR.sec7_fourierBranch_of_rawPacket_XRnonzero_proven {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (h : ¬ScalarTerminal p) (hR : 1 < Nat.card ↥(kernelFrattini K)) (T : Sec7RawTowerPacket chief K) (hT : T = sec7RawTowerPacketCanonical chief K) (hchar : ∃ (lam : Module.Dual (ZMod 2) T.rawModuleData.R), lam ≠ 0 ∧ ∀ (c : T.rawModuleData.C), lam ∘ₗ ↑(T.rawActionData.actR c) = lam) : Nonempty (FourierBranchData p)

The 𝒳_R ≠ 0 branch over the PROVEN packet.

theorem Q2Presentation.Induction.BlockR.sec7_fourierBranch_of_frattiniNontrivial_decomposed'' {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (h : ¬ScalarTerminal p) (hR : 1 < Nat.card ↥(kernelFrattini K)) : Nonempty (FourierBranchData p)

The decomposed R ≠ 1 branch, fully proven-side wiring.