Documentation

Q2Presentation.Induction.Section7FrattiniTrivialElementary

Section 7: the corrected R = 1 elementary-stage branch #

This file lowers the residual sec7_fourierBranch_of_frattiniTrivial from a full arbitrary Fourier-branch packet to the specific elementary-stage packet that the manuscript uses when R = Φ(K) = 1.

Manuscript anchors: in thm:closedrecursion / the inductive step, if R = 1, then the middle quotient B = Y/R is just Y, so no nontrivial R-obstruction or scalar-pushout Fourier layer remains. The branch is the elementary stage (lem:elementarystage, eq:Mstage) with the lower quotient child C = Y/K and the proper exact-image children J < Y mapping onto C.

Lean shape: the obstruction space is fixed to the one-point 𝔽₂-module PUnit, so W = 0, dimExp = 0, and zR = 1. The residual is now split into a smaller core packet, where the partial-count identities are recorded only at the unique character of PUnit; the ordinary all-character elementary-stage data is assembled theorem-level from the subsingleton dual.

The zero obstruction map into the one-point 𝔽₂-module.

Equations
Instances For

    The zero-obstruction fibre is the whole elementary lift index.

    At the unique zero character, the elementary partial-count fibre is also the whole lift index.

    The lowered R = 1 residual: the elementary-stage data for the case B = Y/R = Y.

    It records only the data actually used by lem:elementarystage / eq:Mstage:

    • the lower child C = Y/K;
    • the proper exact-image subtraction children J < Y mapping onto C;
    • the common elementary partial-count recipe for the zero obstruction space;
    • the candidate and local source elementary lift-index sets and the corresponding zero-obstruction realization identities.

    This is strictly smaller than an arbitrary FourierBranchData p: the obstruction space, its dimension exponent, and the lift scalar are fixed as PUnit, 0, and 1.

    Instances For

      The smaller elementary-stage core packet for the R = 1 branch.

      Compared with Sec7FrattiniTrivialElementaryStageData, it stores the elementary partial-count identities only for the zero character. Since Module.Dual (ZMod 2) PUnit is subsingleton, the all-character fields of the ordinary stage data are recovered below by theorem-level assembly. This closes a concrete part of lem:elementarystage: there is no genuine Fourier family of characters in the W = 0 elementary stage.

      Instances For

        The exact-image child packet for the R = 1 elementary stage. This isolates the manuscript's child geometry (C = Y/K and the proper exact-image subtraction children) from the source-specific elementary lift counts.

        Instances For

          Child geometry for the R = 1 elementary stage #

          Every framed target has positive marked-kernel measure.

          The selected kernel lies in the tame-quotient kernel ker pi_Y.

          The manuscript kernel K selected over a genuine chief factor is nontrivial.

          If K = 1, then the condition KS = P in KernelMinimal would collapse to S = P, contradicting the strictness of the chief factor S < P. This closes the nontriviality part of the former lower-quotient residual rather than recording it as an assumption.

          The elementary layer K has cardinality greater than one.

          This is theorem-level Section 7 bookkeeping: it follows only from the corrected KernelMinimal join condition over the nontrivial chief factor, not from any remaining elementary-stage residual.

          The canonical lower framed target C = Y/K, assuming the decoration kills K.

          The hypothesis is exactly the framed quotient constructor missing from the current KernelMinimal API: the manuscript supplies it by lem:decorationblock. The group, marked kernel, tame quotient map, and decoration are all the literal quotient data.

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

            The lower quotient inherits the original boundary frame because H and E are preserved definitionally.

            Equations
            Instances For

              The lower quotient map Y → C = Y/K is onto.

              The lower quotient map preserves the boundary coordinates q_Y = (π_Y, θ_Y). Both coordinates are the defining quotient lifts.

              A proper exact-image subgroup J ≤ Y inherits the boundary-framed structure from Y; in the R = 1 branch the middle target B = Y, so these are precisely the subtraction children of eq:Mstage.

              Equations
              Instances For

                Manuscript-true child-geometry packet for the elementary stage when R = 1.

                This is deliberately only the target/child half of lem:elementarystage / eq:Mstage:

                • K is killed by the decoration, so the lower child is the literal quotient C = Y/K;
                • the proper subtraction terms are actual subgroups J < Y mapping onto C;
                • the strict-decrease estimates are proved below from the recorded cardinal equalities |L_Y| = |K| |L_C| and |J ∩ L_Y| = |J ∩ K| |L_C|, together with 2 |J ∩ K| ≤ |K|.

                It contains no source-specific lift-count identities.

                Instances For

                  Forget the semantic child-geometry packet to the split child-data interface used by Sec7FrattiniTrivialElementaryStageSplitData.

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

                    The lower-quotient half of the child geometry in the R = 1 elementary stage.

                    This isolates the manuscript's C = Y/K construction from the proper exact-image subtraction. Its fields are exactly the target-side facts used to build and bound the lower child: the decoration kills K, the elementary layer K is nontrivial, and the marked-kernel measure satisfies |L_Y| = |K| |L_C|.

                    Instances For

                      The narrowed lower-quotient residual for the R = 1 elementary stage.

                      The nontriviality field 1 < |K| has been removed from the residual and is proved by sec7_Ksub_card_gt_one. What remains is exactly the quotient-construction content of lem:decorationblock / the first identity in lem:strictdecrease: the decoration kills K, and the marked-kernel measure of the literal quotient C = Y/K satisfies |L_Y| = |K| |L_C|.

                      Instances For

                        Assemble the former lower-quotient packet from the narrowed quotient-construction packet and the theorem-level nontriviality of K.

                        Equations
                        • ⋯ = ⋯
                        Instances For

                          The proper exact-image half of the child geometry in the R = 1 elementary stage, relative to an already constructed lower quotient C = Y/K.

                          This is the finite subgroup enumeration in eq:Mstage: the subgroups J < Y mapping onto C, together with the exact-sequence cardinal estimate |J ∩ L_Y| = |J ∩ K| |L_C| and the properness bound 2 |J ∩ K| ≤ |K|.

                          Instances For

                            The narrowed proper-image family residual for the R = 1 elementary stage.

                            This is only the finite exact-image enumeration in eq:Mstage: the proper subgroups J < B = Y that still project to the lower quotient C = Y/K. It contains no cardinal estimates.

                            Instances For
                              @[reducible, inline]

                              The canonical finite index of proper exact-image subgroups in the R = 1 elementary stage. An element is an actual subgroup J ≤ B = Y satisfying exactly the conditions used in eq:Mstage: J < Y, it still projects onto the fixed tame quotient H, and its composite with the lower quotient map Y → C = Y/K is onto.

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

                                The canonical exact-image family, with no residual enumeration choice.

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

                                  The narrowed proper-image descent residual for the R = 1 elementary stage.

                                  This is only the cardinality half of eq:Mdescent, relative to an already enumerated family of proper exact images: |J ∩ L_Y| = |J ∩ K| |L_C| and the properness bound 2 |J ∩ K| ≤ |K|.

                                  Instances For

                                    Canonical eq:Mdescent cardinal data for the actual subtype-indexed exact-image family. This is strictly narrower than asking for descent data for an arbitrary chosen enumeration of the same subgroups: all enumeration bookkeeping is theorem-level.

                                    Instances For

                                      Pull canonical eq:Mdescent data back along any chosen enumeration of proper exact-image children.

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

                                        The decoration-kernel half of the lower-quotient construction in the R = 1 elementary stage. This is the precise target-side assertion from lem:decorationblock: the boundary decoration kills the selected elementary layer K, so the quotient C = Y/K inherits the same decoration.

                                        • Ksub_le_thetaY_ker : K.Ksub ≤ p.fst.thetaY.ker

                                          lem:decorationblock in the elementary branch: the boundary decoration kills K.

                                        Instances For

                                          The finite exact-sequence/cardinality half of the lower quotient C = Y/K. Relative to the already supplied decoration-kernel datum, this records exactly the marked-kernel measure identity |L_Y| = |K| |L_C|.

                                          Instances For

                                            Decoration and lower marked-kernel exact sequence for the R = 1 child #

                                            The decoration descended to the Frattini quotient K/Φ(K).

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

                                              The descended decoration, read as an additive homomorphism on M = K/Φ(K).

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

                                                The descended decoration as a ZMod 2-linear map M → E.

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

                                                  A C-invariant map M → E is zero, by the proved dual-invariant vanishing (M^∨)^C = 0.

                                                  Manuscript lem:decorationblock for the selected elementary layer: the decoration kills K.

                                                  Former lower-decoration residual, now theorem-level. The decoration-kernel statement follows from the already proved Section 7 simple-head mechanism: thetaY descends to a C-invariant linear map on M = K/Φ(K), and (M^∨)^C = 0 forces that map to vanish.

                                                  Exact-sequence data on marked kernels for the lower quotient C = Y/K.

                                                  This is the mechanism behind the former lower-measure atom: a map from L_Y onto L_C whose kernel is the selected elementary layer K.

                                                  Instances For

                                                    The lower marked-kernel exact sequence 1 → K → L_Y → L_C → 1 #

                                                    The quotient map Y → Y/K, restricted and corestricted to the marked kernels L_Y → L_C. The codomain is exactly the marked kernel of the literal lower child C = Y/K, namely the image of L_Y in the quotient.

                                                    Equations
                                                    Instances For

                                                      The lower marked-kernel map is onto, because L_C is defined as the image of L_Y in Y/K.

                                                      The kernel of L_Y → L_C is the selected layer K, viewed inside L_Y.

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

                                                        Closed lower marked-kernel exactness theorem (R = 1, child geometry). The exact sequence is the literal quotient sequence 1 → K → L_Y → L_C → 1 induced by Y → Y/K.

                                                        Former lower-measure residual, now theorem-level from exactness. The marked-kernel measure identity |L_Y| = |K| |L_C| is obtained by cardinality of a finite surjective homomorphism and the kernel equivalence with K.

                                                        Former lower-quotient core residual, now theorem-level from two smaller packets. The old core packet is assembled from the decoration-kernel fact and the lower quotient marked-kernel cardinal identity. The nontriviality field of the still older packet is proved separately by sec7_Ksub_card_gt_one.

                                                        Former lower-quotient residual, now theorem-level. The public packet is assembled from the narrowed quotient-construction residual and the proved nontriviality of the minimal kernel K.

                                                        Former proper-image family residual, now theorem-level. The finite exact-image family is the canonical subtype of subgroups J < B = Y satisfying the two surjectivity conditions from eq:Mstage; no residual enumeration choice remains.

                                                        Exact-sequence data for every canonical proper exact-image subgroup in the R = 1 elementary stage.

                                                        For each J < Y mapping onto C = Y/K, this records the restricted exact sequence 1 → J ∩ K → J ∩ L_Y → L_C → 1 behind eq:Mdescent.

                                                        Instances For

                                                          Restricted exact sequences for canonical proper exact images #

                                                          theorem Q2Presentation.Induction.sec7_subgroup_eq_top_of_ker_le_of_surjective_restrict {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) (J : Subgroup G) (hJ : Function.Surjective ⇑(f.comp J.subtype)) (hker : f.ker ≤ J) :
                                                          J = ⊤

                                                          If J maps onto a quotient and contains the kernel, then J is the whole group. This is the elementary finite-group argument behind the proper-image kernel bound.

                                                          The underlying element of the proper-image marked kernel J ∩ L_Y, read in Y.

                                                          Equations
                                                          Instances For

                                                            Compatibility of the lower quotient map with the tame quotient map.

                                                            The canonical restricted map J ∩ L_Y → L_C, induced by the quotient map Y → Y/K.

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

                                                              The canonical restricted map is onto L_C. If j ∈ J maps to a marked-kernel class in C, then compatibility with π_Y shows j ∈ L_Y.

                                                              The kernel of the restricted map is the literal intersection J ∩ K.

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

                                                                Closed canonical restricted-exactness theorem (R = 1, child geometry). For every canonical proper exact-image subgroup J < Y mapping onto C = Y/K, the restricted quotient map gives the exact sequence 1 → J ∩ K → J ∩ L_Y → L_C → 1; the half-cardinality bound comes from J ∩ K < K.

                                                                Former canonical descent residual, now theorem-level from restricted exactness. The cardinal formula |J ∩ L_Y| = |J ∩ K| |L_C| follows from finite exact-sequence cardinality applied to each canonical restricted map.

                                                                Former proper-image descent residual, now theorem-level. The old statement allowed an arbitrary chosen finite family. It is assembled by pulling the canonical eq:Mdescent data back along that family's subgroup map into the canonical subtype.

                                                                Former proper-image residual, now theorem-level. The public exact-image packet is assembled from the independent finite enumeration and cardinal-descent pieces of eq:Mstage / eq:Mdescent.

                                                                Former child-geometry residual, now theorem-level. The broad child-geometry packet is assembled from the manuscript's two independent target-side pieces: the lower quotient C = Y/K and the proper exact-image enumeration in the M-stage subtraction.

                                                                The exact-image child half of the R = 1 elementary-stage split packet is now assembled theorem-level from the child-geometry residual.

                                                                The normalized source-count packet for the R = 1 elementary stage, relative to a fixed child packet. The obstruction space has already collapsed to PUnit, so the residual stores literal lift-index cardinalities rather than cardinalities of vacuous zero-obstruction subtypes. The subtype-to-index conversion is proved below.

                                                                Instances For

                                                                  A split residual packet: child geometry plus normalized source-count data.

                                                                  Instances For

                                                                    The elementary-stage child list attached to the split child packet.

                                                                    Equations
                                                                    Instances For

                                                                      Assemble the old core packet from child data plus normalized count data. The only work here is the theorem-level conversion from the vacuous zero-obstruction subtype to the full lift index.

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

                                                                        The elementary-stage child list: the lower quotient child followed by the proper-image subtraction children.

                                                                        Equations
                                                                        Instances For

                                                                          Assemble the ordinary FourierBranchData packet from the lowered R = 1 elementary-stage data.

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

                                                                            The all-character candidate partial identity follows from the single zero-character identity because the dual of PUnit is subsingleton.

                                                                            The all-character local partial identity follows from the single zero-character identity because the dual of PUnit is subsingleton.

                                                                            Assemble the previous elementary-stage data packet from the smaller core packet.

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

                                                                              The elementary-stage numerical functional from eq:Mstage:

                                                                              N([e(C), e(J₁), ..., e(Jₙ)]) = z_M * e(C) - Σ e(Jᵢ).

                                                                              The empty-list value is unused by the assembled child packet, but making the function total keeps the normalized-count interface independent of a separate nonempty-list subtype.

                                                                              Equations
                                                                              Instances For

                                                                                A manuscript-shaped normalized source-count packet for the R = 1 elementary stage.

                                                                                Compared with Sec7FrattiniTrivialElementaryNormalizedCountData, this stores the actual eq:Mstage functional: the common lift multiplicity is 2^(2 dim M), and the candidate and local lift-index cardinalities are obtained from the lower child and the proper-image subtraction children by the same formula.

                                                                                Instances For

                                                                                  The lift-multiplicity half of the R = 1 elementary source-count calculation.

                                                                                  This is the numerical part of lem:elementarystage: the common size of the cocycle torsor for an M-lift is 2^(2 dim M). It is separated from the source-specific lift-index realizations and from exact-image subtraction.

                                                                                  • dimM : ℕ

                                                                                    The dimension of the elementary layer M over 𝔽₂.

                                                                                  • liftMultiplicity : ℕ

                                                                                    The common lift multiplicity |Z¹_{Γ,ρ}(M)| = 2^(2 dim M).

                                                                                  • liftMultiplicity_eq : self.liftMultiplicity = 2 ^ (2 * self.dimM)

                                                                                    The manuscript multiplicity formula.

                                                                                  Instances For

                                                                                    The source-specific elementary lift indices, after the multiplicity has been fixed.

                                                                                    This records only the realization of the candidate and local exact-image counts as the cardinalities of their elementary lift-index sets. It contains no subtraction formula.

                                                                                    • XA : Type

                                                                                      Candidate-source elementary lift index.

                                                                                    • finXA : Fintype self.XA
                                                                                    • XQ : Type

                                                                                      Local-source elementary lift index.

                                                                                    • finXQ : Fintype self.XQ
                                                                                    • realizeA_card : framedCountA p = ↑(Nat.card self.XA)

                                                                                      Candidate elementary lift identity, normalized to the full lift index.

                                                                                    • realizeQ_card : framedCountQ p = ↑(Nat.card self.XQ)

                                                                                      Local elementary lift identity, normalized to the full lift index.

                                                                                    Instances For

                                                                                      The exact-image subtraction half of eq:Mstage, relative to fixed lift indices.

                                                                                      This is the common source-independent functional z_M · e(C) - Σ_{J<C} e(J), instantiated for the candidate and local sources.

                                                                                      Instances For

                                                                                        Forget the eq:Mstage-shaped count packet to the normalized zero-obstruction count interface used by the existing elementary-stage assembly.

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

                                                                                          The actual elementary-layer dimension used by the R = 1 M-stage.

                                                                                          In the manuscript notation this is dim_{𝔽₂} M, with M = K/Φ(K). The current concrete Section 7 tower realizes this as towerM K; when R = Φ(K) = 1, this is the elementary layer lifted in eq:Mstage.

                                                                                          Equations
                                                                                          Instances For

                                                                                            The source-level cocycle groups controlling the elementary M-lift torsors.

                                                                                            This is the source-theoretic content behind the old multiplicity residual: for both sources, the relevant Z¹_{Γ,ρ}(M) groups have cardinality 2^(2 dim M), with dim M fixed to the literal concrete module towerM K. It is smaller than Sec7FrattiniTrivialElementaryMStageMultiplicityData: it no longer allows an arbitrary dimension or an arbitrary common multiplicity detached from the manuscript module layer.

                                                                                            Instances For

                                                                                              Candidate-side constructor for the actual word-complex cocycle group in the R = 1 M-stage.

                                                                                              The three endomorphisms are the evaluated candidate word-complex operators on the literal module M = towerM K: Sinv = ρ(σ)⁻¹, T = ρ(τ), and P is the norm operator appearing in Lifting.Z1. The current framed-pair interface does not yet carry the lower source map/marking from which these endomorphisms are computed, so this is the smallest constructor atom left by the existing API: it pins the candidate cocycle object to Q2Presentation.Lifting.Z1 rather than to an arbitrary additive group.

                                                                                              Instances For

                                                                                                Candidate-side cardinality formula for the actual word-complex cocycle group.

                                                                                                Instances For

                                                                                                  Local-source constructor for the actual continuous local cocycle group in the R = 1 M-stage.

                                                                                                  The bundled finite discrete representation is the local G_{ℚ₂}-module whose underlying 𝔽₂-space is linearly identified with the concrete target module towerM K. The continuous local cocycle group is then A.Z1 from Local.Cohomology.

                                                                                                  • The local finite discrete G_{ℚ₂}-module corresponding to M = towerM K.

                                                                                                  • module_equiv : self.A.V ≃ₗ[ZMod 2] towerM K

                                                                                                    Identification of the local coefficient module with the concrete Section 7 module.

                                                                                                  • The local source quotient through which this coefficient representation factors.

                                                                                                    This is the Lean form of the source-interface assertion that the local G_{ℚ₂} action on the selected coefficient module is the same finite C = Y/K action as the target-side tower action.

                                                                                                  • source_surjective : Function.Surjective ⇑self.source

                                                                                                    The source-interface map realizes the whole finite quotient C = towerC K.

                                                                                                  • module_equiv_action (g : ↑GQ2Profinite.toProfinite.toTop) (v : self.A.V) : self.module_equiv ((self.A.ρ g) v) = ((towerActM K) (self.source g)) (self.module_equiv v)

                                                                                                    Equivariance of the chosen linear identification with the concrete tower action.

                                                                                                  • finZQ : Fintype ↥self.A.Z1

                                                                                                    Finiteness of the literal local continuous cocycle group A.Z1.

                                                                                                  Instances For

                                                                                                    Local-source cardinality formula for the actual continuous local cocycle group.

                                                                                                    Instances For

                                                                                                      Candidate-source elementary lift-index realization, separated from the local side.

                                                                                                      • XA : Type

                                                                                                        Candidate-source elementary M-lift index.

                                                                                                      • finXA : Fintype self.XA
                                                                                                      • realizeA_card : framedCountA p = ↑(Nat.card self.XA)

                                                                                                        Candidate boundary-framed count realized as the cardinality of the lift index.

                                                                                                      Instances For

                                                                                                        Local-source elementary lift-index realization, separated from the candidate side.

                                                                                                        • XQ : Type

                                                                                                          Local-source elementary M-lift index.

                                                                                                        • finXQ : Fintype self.XQ
                                                                                                        • realizeQ_card : framedCountQ p = ↑(Nat.card self.XQ)

                                                                                                          Local boundary-framed count realized as the cardinality of the lift index.

                                                                                                        Instances For

                                                                                                          Candidate eq:Mstage exact-image subtraction, separated from the local side.

                                                                                                          Instances For

                                                                                                            Local eq:Mstage exact-image subtraction, separated from the candidate side.

                                                                                                            Instances For

                                                                                                              Candidate-side word-operator datum for the literal word complex on M = towerM K.

                                                                                                              This is the smaller candidate-side semantic input behind the former cocycle-group constructor. It records the evaluated candidate action operators and their finite-word linear shadows (lem:jacobian, lem:h0shadow) but does not include either the cocycle group itself or its cardinality. Finiteness of the corresponding Lifting.Z1 is theorem-level because towerM K is a finite 𝔽₂-module.

                                                                                                              • S : Module.End (ZMod 2) (towerM K)

                                                                                                                The candidate operator ρ(σ) on M = towerM K.

                                                                                                              • Sinv : Module.End (ZMod 2) (towerM K)

                                                                                                                The candidate operator ρ(σ)⁻¹ on M = towerM K.

                                                                                                              • T : Module.End (ZMod 2) (towerM K)

                                                                                                                The candidate operator ρ(τ) on M = towerM K.

                                                                                                              • X₀ : Module.End (ZMod 2) (towerM K)

                                                                                                                The candidate operator ρ(x₀) on M = towerM K.

                                                                                                              • X₁ : Module.End (ZMod 2) (towerM K)

                                                                                                                The candidate operator ρ(x₁) on M = towerM K.

                                                                                                              • P : Module.End (ZMod 2) (towerM K)

                                                                                                                The candidate norm operator P = 1 + T + ⋯ appearing in Lifting.Z1.

                                                                                                              • sinv_left : self.Sinv * self.S = 1

                                                                                                                Sinv is the left inverse of the evaluated σ-operator.

                                                                                                              • tame_shadow : self.Sinv * self.T * self.S = self.T ^ 2

                                                                                                                The tame row shadow of the candidate word complex.

                                                                                                              • norm_shadow : self.P * (self.T - 1) = 0

                                                                                                                The norm row shadow P·(T-1)=0.

                                                                                                              • wild_shadow : (self.P + self.Sinv) * (self.X₁ - 1) = 0

                                                                                                                The wild row shadow (P+Sinv)·(X₁-1)=0.

                                                                                                              Instances For

                                                                                                                Candidate-side finrank formula for the literal word-complex cocycle group.

                                                                                                                This is the linear-algebraic content of lem:elementarystage on the candidate side: candidate deformation duality plus (M^∨)^C = 0 gives dim Z¹_{Γ_A,ρ}(M) = 2·dim M. The old cardinality packet is recovered below from this rank formula by the finite-vector-space identity |V| = 2^(finrank V) over 𝔽₂.

                                                                                                                Instances For

                                                                                                                  The lower candidate action on the literal Section 7 module M = towerM K, viewed as a monoid representation into linear endomorphisms.

                                                                                                                  The already-proved concrete tower gives towerActM K : towerC K →* (towerM K ≃ₗ towerM K). This definition forgets the inverse map of each linear equivalence, producing the representation used by the candidate word complex.

                                                                                                                  Equations
                                                                                                                  Instances For

                                                                                                                    The missing candidate lower source/marking for the R = 1 M-stage.

                                                                                                                    This is deliberately smaller and more source-specific than the former operator packet. It records a genuine candidate epimorphism to the lower quotient C = towerC K, its four marked values σ, τ, x₀, x₁, and the candidate relators seen in that lower quotient. No linear operators or cocycle cardinalities are chosen here.

                                                                                                                    Instances For

                                                                                                                      The tame shadow follows by applying the lower action to the candidate tame relator.

                                                                                                                      The tame relator in the word-language implies the explicit right-conjugation relation on the marked generators. This is the tiny local form needed to turn an admissible lower marking into the lower-source packet below.

                                                                                                                      A smaller source-side residual for the candidate lower quotient in the R = 1 M-stage.

                                                                                                                      Instead of postulating a continuous epimorphism Γ_A ↠ C = towerC K together with its four generator values and the two relators, this atom records only an admissible finite marking of the lower quotient. The actual epimorphism and its generator values are then recovered theorem-level from the already-proved finite-quotient semantics GammaA_epi_equiv_admissible (manuscript prop:epi-semantics).

                                                                                                                      • q : Marking (towerC K)

                                                                                                                        The admissible candidate marking of the lower quotient C = towerC K.

                                                                                                                      • admissible : Admissible self.q

                                                                                                                        The marking satisfies the two candidate relators, generates C, and has wild values in O₂(C).

                                                                                                                      Instances For

                                                                                                                        The finite presented lower marking of C = towerC K.

                                                                                                                        This is the presentation half of admissibility: a concrete finite marking of the lower quotient, generation, and the two candidate relators. It intentionally does not record wild-core membership; that is the separate finite O₂(C) datum below.

                                                                                                                        • q : Marking (towerC K)

                                                                                                                          The finite lower candidate marking of C = towerC K.

                                                                                                                        • generated : generates self.q

                                                                                                                          The marked images generate C.

                                                                                                                        • tame : tameRel self.q

                                                                                                                          The tame candidate relator holds in C.

                                                                                                                        • wild : wildRel self.q

                                                                                                                          The wild candidate relator holds in C.

                                                                                                                        • x0_mem_twoCore : self.q Gen.x0 ∈ twoCore (towerC K)

                                                                                                                          The lower image of x₀ lies in O₂(C); stored here so the later core projections do not quantify over an arbitrary unrelated presented marking.

                                                                                                                        • x1_mem_twoCore : self.q Gen.x1 ∈ twoCore (towerC K)

                                                                                                                          The lower image of x₁ lies in O₂(C); stored here so the later core projections do not quantify over an arbitrary unrelated presented marking.

                                                                                                                        Instances For

                                                                                                                          The finite wild-core half of the lower admissible marking.

                                                                                                                          For the already-chosen finite presented lower marking, this records exactly the remaining condition from prop:epi-semantics: the two wild marked values land in O₂(C).

                                                                                                                          Instances For

                                                                                                                            Route245 split of the Route244 lower finite candidate-marking atoms #

                                                                                                                            The bare finite lower candidate marking of C = towerC K.

                                                                                                                            This is strictly smaller than the former presented-marking atom: it contains only the four elements of the lower quotient, with no generation or relator assertions.

                                                                                                                            Instances For

                                                                                                                              The generation half of the finite lower presented marking.

                                                                                                                              • generated : generates mark.q

                                                                                                                                The marked images generate C.

                                                                                                                              Instances For

                                                                                                                                The tame-relator half of the finite lower presented marking.

                                                                                                                                • tame : tameRel mark.q

                                                                                                                                  The tame candidate relator holds in C.

                                                                                                                                Instances For

                                                                                                                                  The wild-relator half of the finite lower presented marking.

                                                                                                                                  • wild : wildRel mark.q

                                                                                                                                    The wild candidate relator holds in C.

                                                                                                                                  Instances For

                                                                                                                                    The source-map residual behind the finite lower candidate marking.

                                                                                                                                    This is the corrected provenance datum for the Route245 finite-marking split: instead of asserting generation/relators/core membership for an arbitrary bare function Gen → towerC K, it records the actual lower candidate epimorphism Γ_A ↠ C = towerC K. The six formerly visible finite-marking atoms are then recovered from GammaA_epi_equiv_admissible.

                                                                                                                                    Instances For

                                                                                                                                      A boundary-framed source map to the literal lower quotient C = Y/K.

                                                                                                                                      This is a stricter manuscript-shaped provenance datum than a bare map Γ_A ↠ towerC K: it records an actual candidate boundary-framed surjection to the lower child constructed from the same quotient and the same inherited frame. The bare finite source-map packet below is recovered by forgetting the boundary-compatibility proof and the framing predicate.

                                                                                                                                      Instances For

                                                                                                                                        Finite marking form of the lower boundary-source datum.

                                                                                                                                        The decoration-kernel hypothesis is supplied by the already-proved lem:decorationblock theorem (sec7_frattiniTrivial_elementaryLowerDecorationData). This residual is therefore strictly finite and candidate-side: it gives an admissible marking of the literal lower quotient C = Y/K whose generator values already satisfy the inherited boundary equation. The continuous boundary-framed epimorphism is then recovered theorem-level from GammaA_epi_equiv_admissible and generator-density.

                                                                                                                                        Instances For

                                                                                                                                          The finite admissible-marking half of the lower boundary source.

                                                                                                                                          This separates the manuscript's finite Γ_A-quotient datum from the inherited boundary frame: the marking already satisfies the candidate presentation, but no boundary equation is stored here.

                                                                                                                                          Instances For

                                                                                                                                            The inherited-boundary compatibility half of the lower source.

                                                                                                                                            For the already chosen finite admissible marking, this is exactly the generator-level boundary-frame equation. The all-elements boundary-framed surjection is reconstructed below by GammaA_epi_equiv_admissible and gammaGen_hom_ext.

                                                                                                                                            Instances For

                                                                                                                                              Route251 split of the lower-boundary finite source atoms #

                                                                                                                                              The carrier half of the lower-boundary finite marking: only the four marked candidate images in the literal lower quotient C = Y/K.

                                                                                                                                              Instances For

                                                                                                                                                The generation component of admissibility for the lower-boundary marking.

                                                                                                                                                • generated : generates carrier.q

                                                                                                                                                  The marked images generate C.

                                                                                                                                                Instances For

                                                                                                                                                  The tame-relator component of admissibility for the lower-boundary marking.

                                                                                                                                                  • tame : tameRel carrier.q

                                                                                                                                                    The tame candidate relator holds in the lower quotient.

                                                                                                                                                  Instances For

                                                                                                                                                    The wild-relator component of admissibility for the lower-boundary marking.

                                                                                                                                                    • wild : wildRel carrier.q

                                                                                                                                                      The wild candidate relator holds in the lower quotient.

                                                                                                                                                    Instances For

                                                                                                                                                      The x₀ two-core component of admissibility for the lower-boundary marking.

                                                                                                                                                      Instances For

                                                                                                                                                        The x₁ two-core component of admissibility for the lower-boundary marking.

                                                                                                                                                        Instances For

                                                                                                                                                          The actual lower-boundary candidate source map behind the finite carrier. This is the manuscript source datum: an epimorphism Γ_A ↠ C = Y/K together with the two coordinate forms of the inherited boundary equation on the four distinguished generators.

                                                                                                                                                          Instances For

                                                                                                                                                            Checkpoint 254 split of the lower-boundary finite-frame input #

                                                                                                                                                            The source-level finite lower-boundary frame: an actual candidate epimorphism to the inherited lower quotient, together with the generator-level inherited boundary equation. This is the remaining candidate-side source datum; the finite presentation and O₂ components below are recovered theorem-level from GammaA_epi_equiv_admissible, not assumed separately.

                                                                                                                                                            Instances For

                                                                                                                                                              The finite lower-boundary carrier: a marking of the inherited lower quotient that is known to come from an actual candidate epimorphism. The source map fields are not extra finite presentation assumptions; they are exactly what lets the generation, relator, and O₂ components be proved from prop:epi-semantics.

                                                                                                                                                              Instances For

                                                                                                                                                                Full boundary-framed source map for the inherited lower finite frame.

                                                                                                                                                                This is one step closer to Definition 4.1 than the checkpoint-255 generator-only source atom: it records an actual candidate epimorphism Γ_A ↠ C = Y/K satisfying the inherited boundary-frame equation for every element of Γ_A. The generator-level finite-frame source datum used below is recovered by evaluating this equality on gammaGen.

                                                                                                                                                                Instances For

                                                                                                                                                                  Canonical source object for the inherited lower finite frame.

                                                                                                                                                                  Instead of storing the homomorphism, surjectivity, and boundary equation as separate custom fields, this packet stores an actual member of the canonical boundary-framed surjection type e_{Γ_A}^β(C). The full map datum above is recovered by projecting this subtype.

                                                                                                                                                                  Instances For

                                                                                                                                                                    Canonical finite admissible quotient for the inherited lower frame.

                                                                                                                                                                    This is below the checkpoint-257 source atom: it contains only the finite marking of the literal lower quotient C = Y/K together with the candidate finite-quotient presentation conditions. The continuous epimorphism from Γ_A is reconstructed theorem-level by GammaA_epi_equiv_admissible.

                                                                                                                                                                    Instances For

                                                                                                                                                                      Generator-level inherited-boundary compatibility for the chosen finite quotient.

                                                                                                                                                                      This is the second half of the lower-frame source construction: once the admissible marking is fixed, the boundary equation is only required on the four dense universal generators. The all-elements boundary-framed equation is recovered below by gammaGen_hom_ext.

                                                                                                                                                                      Instances For

                                                                                                                                                                        Carrier for the finite admissible quotient of the inherited lower frame.

                                                                                                                                                                        This is the next split below the checkpoint-258 admissible-quotient atom: first choose only the literal finite marking of C = Y/K; the five finite-presentation clauses are kept as separate manuscript-shaped inputs below.

                                                                                                                                                                        Instances For

                                                                                                                                                                          Finite tower-level source marking with inherited boundary coordinates.

                                                                                                                                                                          This is the strictly smaller manuscript datum below the generator-level source-map leaf: it contains no continuous homomorphism Γ_A → C and no surjectivity assertion. It only records an admissible finite quotient marking of the concrete tower quotient towerC K = Y/K, plus the two inherited boundary coordinates of that marking on the four distinguished generators. The actual epimorphism and its exact image are recovered below from GammaA_epi_equiv_admissible.

                                                                                                                                                                          Instances For

                                                                                                                                                                            Lower tame/pro-2 tower compatibility datum for the inherited lower finite frame.

                                                                                                                                                                            This is one step below the checkpoint-336 tower-marking packet. It still records only a finite admissible marking of the concrete tower quotient towerC K, but the boundary coordinates are not phrased through the already-paired boundary map β : ∂_bd → H × E. Instead, they are stated separately against the two primitive boundary factors: the tame map α : T_tame → H and the pro-2 decoration map ψ : Π → E. The paired β-coordinate equalities of the old packet are recovered theorem-level using BoundaryFrame.beta_def, boundaryBeta_apply, and the two projections of boundaryPackage_GammaA.toBoundary.

                                                                                                                                                                            Instances For

                                                                                                                                                                              Pointwise tame/pro-2 factor compatibility datum for the inherited lower finite frame.

                                                                                                                                                                              This is below the previous factor-compatibility packet: it keeps the same finite admissible tower marking, but it no longer stores the two boundary-factor equations as functions ∀ a : Gen. Instead it records the eight literal generator rows separately. The functional statement is reconstructed theorem-level by case analysis on Gen.

                                                                                                                                                                              Instances For

                                                                                                                                                                                Checkpoint 339: one pro-2 row is theorem-level from admissibility #

                                                                                                                                                                                Seven-row pointwise tame/pro-2 factor datum for the inherited lower finite frame.

                                                                                                                                                                                Compared with the checkpoint-338 point packet, the pro-2 decoration row on τ is no longer primitive: it is recovered theorem-level from admissibility by sec7_lowerBoundary_theta_tau_row_from_admissible.

                                                                                                                                                                                Instances For

                                                                                                                                                                                  Checkpoint 340: tame x₀/x₁ rows from lower-kernel membership #

                                                                                                                                                                                  A smaller pointwise packet for the inherited lower finite frame.

                                                                                                                                                                                  Compared with the checkpoint-339 seven-row packet, the tame rows on x₀ and x₁ are not assumed as boundary equalities. Instead this packet records the strictly local statement that the two chosen wild generator values land in the marked lower kernel L_C = ker(π_C). Since the candidate tame quotient kills the universal x₀ and x₁, the two tame rows are recovered theorem-level below.

                                                                                                                                                                                  Instances For

                                                                                                                                                                                    Concrete-generator version of the kernel-reduced pointwise packet.

                                                                                                                                                                                    Compared with Sec7FrattiniTrivialElementaryMStageCandidateLowerBoundaryTowerTamePro2PointKernelReducedData, this datum no longer mentions the candidate boundary maps on the five remaining tame/pro-2 generator rows. It records the same lower finite marking against the concrete boundary generators tameSigma, tameTau, piSigma, piX0, and piX1; the old rows are recovered below using gammaTameMap_apply_sigma, gammaTameMap_apply_tau, and the p_gammaGen_* pro-2 generator theorems.

                                                                                                                                                                                    Instances For

                                                                                                                                                                                      Checkpoint 342: the O₂(C) part of admissibility is theorem-level #

                                                                                                                                                                                      Presented concrete-generator kernel packet for the inherited lower finite frame.

                                                                                                                                                                                      Compared with the checkpoint-341 concrete-kernel packet, this datum no longer assumes full Admissible q. It records only the presentation part of admissibility (generation plus the tame and wild relators), together with the already local lower-kernel memberships for the wild generators. The two O₂(C) clauses required for Admissible q are recovered theorem-level below from the normal 2-subgroup L_C ◁ C: since L_C is a normal 2-subgroup, L_C ≤ O₂(C).

                                                                                                                                                                                      Instances For

                                                                                                                                                                                        Checkpoint 343: the source map now determines q and the presentation rows #

                                                                                                                                                                                        Source-level concrete-generator datum for the inherited lower finite frame.

                                                                                                                                                                                        This is strictly below the checkpoint-342 presented concrete-kernel packet. The primitive no longer chooses an arbitrary q : Gen → towerC K, and it no longer assumes generates q, tameRel q, or wildRel q. Instead it records the actual candidate source epimorphism Γ_A ↠ towerC K; the lower marking is defined theorem-level as its four generator values, and the presentation part is recovered from GammaA_epi_equiv_admissible.

                                                                                                                                                                                        The fields that remain primitive are precisely the lower-boundary source data not provided by finite-quotient semantics: the two concrete tame rows, the two lower-kernel memberships, and the three concrete pro-2 rows.

                                                                                                                                                                                        Instances For

                                                                                                                                                                                          The new primitive source-level concrete-generator kernel datum.

                                                                                                                                                                                          It is below the checkpoint-342 residual because it does not assume the lower marking or any of the three finite presentation clauses; those are reconstructed below from the source epimorphism by GammaA_epi_equiv_admissible.

                                                                                                                                                                                          The checkpoint-342 presented concrete-generator datum is theorem-level from the source-level datum. The marking is the generator-value marking of the source epimorphism, and generation plus both candidate relators are obtained from finite-quotient semantics.

                                                                                                                                                                                          The checkpoint-341 concrete-generator kernel packet is theorem-level from the presented concrete-kernel datum. The only lost field is full admissibility, whose O₂(C) clauses are reconstructed from the two lower-kernel memberships.

                                                                                                                                                                                          The checkpoint-340 kernel-reduced packet is theorem-level from the concrete-generator packet. The five remaining tame/pro-2 rows are transported along the already-proved generator-image theorems for the candidate tame and pro-2 boundary maps.

                                                                                                                                                                                          The checkpoint-339 seven-row point packet is theorem-level from the kernel-reduced packet: the tame rows on x₀ and x₁ are forced by lower-kernel membership and by the candidate tame quotient identities γ_A(x₀)=γ_A(x₁)=1 in Ttame.

                                                                                                                                                                                          The checkpoint-338 eight-row point packet is theorem-level from the seven-row packet: the omitted pro-2 decoration row on τ is forced by oddness of tame inertia and the elementary 2-group decoration target.

                                                                                                                                                                                          Primitive source-map mechanism for the inherited lower finite frame, now theorem-level from the finite tower-level marking compatibility datum above.

                                                                                                                                                                                          The candidate epimorphism is obtained by applying GammaA_epi_equiv_admissible to the admissible marking of towerC K; the two generator boundary coordinates are transported along the resulting generator-value identity. This avoids assuming the epimorphism or its surjectivity as primitive data and does not reintroduce the split finite-frame admissibility fields.

                                                                                                                                                                                          The checkpoint-334 semantic leaf is now theorem-level from the more primitive source-map mechanism: the full boundary-framed equation follows because the two finite maps to H × E agree on the dense universal generators.

                                                                                                                                                                                          Former tame-relator primitive for the split finite admissible quotient, now recovered from GammaA_epi_equiv_admissible applied to the carrier's actual source epimorphism.

                                                                                                                                                                                          Former wild-relator primitive for the split finite admissible quotient, now recovered from GammaA_epi_equiv_admissible applied to the carrier's actual source epimorphism.

                                                                                                                                                                                          Former finite admissible-quotient atom, now theorem-level from the carrier plus the five literal finite-presentation and O₂ clauses.

                                                                                                                                                                                          Former generator-level lower finite-frame source atom, now theorem-level from a full boundary-framed candidate epimorphism to the inherited lower quotient.

                                                                                                                                                                                          Former finite-frame marking input, now theorem-level from the carrier plus the five presentation/O₂ components of the inherited lower finite quotient.

                                                                                                                                                                                          Former lower-boundary source-map input, now theorem-level from a finite admissible lower marking plus its generator-level inherited-boundary equation.

                                                                                                                                                                                          Former generation input for the lower-boundary finite marking, now theorem-level from candidate finite-quotient semantics applied to the carrier source map.

                                                                                                                                                                                          Former lower-boundary admissible-marking atom, now theorem-level from the literal finite presentation components: carrier, generation, tame relator, wild relator, and the separate x₀/x₁ two-core assertions.

                                                                                                                                                                                          The tame-quotient coordinate of the inherited-boundary generator equation.

                                                                                                                                                                                          Instances For

                                                                                                                                                                                            The elementary-decoration coordinate of the inherited-boundary generator equation.

                                                                                                                                                                                            Instances For

                                                                                                                                                                                              Former Route249 lower-boundary marking leaf, now theorem-level from two strictly smaller manuscript components: finite admissibility of the lower quotient marking and its inherited boundary-frame generator equation.

                                                                                                                                                                                              The finite target morphism induced by the combined tame/decorated quotient map q_Y = (π_Y, θ_Y).

                                                                                                                                                                                              Equations
                                                                                                                                                                                              Instances For

                                                                                                                                                                                                Former lower boundary-surjection leaf, now theorem-level from the finite admissible marking with generator boundary compatibility. The proof is exactly prop:epi-semantics: an admissible finite marking gives Γ_A ↠ C; since both maps to H × E agree on the four dense generators, the boundary-framed equation holds for all γ : Γ_A.

                                                                                                                                                                                                Remaining source-map input for the lower finite candidate quotient, now theorem-level from the boundary-framed lower-child source datum. The resulting packet forgets exactly what the later finite-quotient consequences do not use: the inherited frame and the boundary-compatibility equation.

                                                                                                                                                                                                Route245 residual closed theorem-level: the bare finite lower candidate marking of C = towerC K is the generator-value marking of the lower source map.

                                                                                                                                                                                                The finite lower marking attached to a source map is admissible, by the candidate finite-quotient semantics.

                                                                                                                                                                                                The x₀-core half of the finite wild-core datum.

                                                                                                                                                                                                Instances For

                                                                                                                                                                                                  The x₁-core half of the finite wild-core datum.

                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                    Former Route244 presented-marking residual, now theorem-level from four smaller finite quotient atoms: the bare marking, generation, tame relator, and wild relator.

                                                                                                                                                                                                    Former Route243 finite-admissible-marking residual, now theorem-level from the two smaller finite quotient atoms: the presented lower marking and its O₂(C) wild-core membership.

                                                                                                                                                                                                    The missing finite-word/Fox calculation which turns the lower candidate relators into the wild row shadow on M = towerM K.

                                                                                                                                                                                                    Unlike the old word-operator atom, this does not choose operators. The operators are definitionally the images of the source values under towerActM K, and P is definitionally the norm of τ. The lone field is the manuscript calculation lem:h0shadow / lem:fullwordledger specialized to this lower source: from the recorded wild relator and its evaluated word ledger, the wild row shadow follows.

                                                                                                                                                                                                    • wild_shadow_from_relator : (src.P + src.Sinv) * (src.X₁ - 1) = 0

                                                                                                                                                                                                      The wild row shadow obtained from the candidate wild relator by the finite-word ledger (lem:h0shadow and lem:fullwordledger). The explicit argument forces this datum to be a relator-to-shadow calculation, not an arbitrary shadow assertion.

                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                      A stricter finite-word ledger atom for the candidate wild row.

                                                                                                                                                                                                      This records the Fox fundamental identity before cancelling the norm term: P·(T-1) + (P+S⁻¹)·(X₁-1) = 0. The cancellation P·(T-1)=0 is already proved theorem-level from the norm definition (src.norm_shadow), so the older CandidateRelatorShadowData is recovered below without postulating its final form directly. The premise is the actual evaluated candidate wild relator in the lower marking, not an arbitrary proposition.

                                                                                                                                                                                                      • wild_row_fundamental_from_relator : Q2Word.wildRelator.eval src.marking = 1 → src.P * (src.T - 1) + (src.P + src.Sinv) * (src.X₁ - 1) = 0

                                                                                                                                                                                                        The manuscript wild-row Fox identity obtained from lem:h0shadow and lem:fullwordledger, before the separate norm cancellation.

                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                        Route240 split of the two Route239 candidate residuals #

                                                                                                                                                                                                        The previous Route239 frontier exposed two candidate-side atoms:

                                                                                                                                                                                                        The declarations below split those atoms into smaller manuscript-shaped pieces and reassemble the Route239 names theorem-level. This keeps the existing downstream API unchanged while making the next residual frontier more local:

                                                                                                                                                                                                        A candidate lower epimorphism Γ_A ↠ C = towerC K.

                                                                                                                                                                                                        This is the Route241 lowering of the Route240 marking/exact-image surface: the literal marking is no longer an arbitrary Gen → C; it is definitionally the image of the four universal generators under a concrete continuous candidate homomorphism, and the surjectivity field records the exact-image assertion needed to recover admissibility from GammaA_epi_equiv_admissible.

                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                          The literal lower candidate marking of C = towerC K, tied to an actual candidate homomorphism from Γ_A.

                                                                                                                                                                                                          Compared with the Route240 structure, the marking is not free data: the field q_eq records that it is exactly the image of the four universal generators under hom. This makes the generation, relator, and O₂(C) fields theorem-level consequences of the separate surjectivity datum and GammaA_epi_equiv_admissible.

                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                            The lower marking generates the lower quotient C. This is the generation part of admissibility, recovered from candidate finite-quotient semantics.

                                                                                                                                                                                                            • generated : generates mark.q

                                                                                                                                                                                                              The marked images of σ,τ,x₀,x₁ generate C.

                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                              The two candidate relators on the lower marking of C.

                                                                                                                                                                                                              • tame : tameRel mark.q

                                                                                                                                                                                                                The tame relation τ^σ = τ².

                                                                                                                                                                                                              • wild : wildRel mark.q

                                                                                                                                                                                                                The wild relation h₀ u₁⁻¹ x₁^σ c₀ = 1.

                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                The lower wild generators land in the finite 2-core of C.

                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                  The carrier part of the lower candidate homomorphism Γ_A ⟶ C = towerC K.

                                                                                                                                                                                                                  This Route242 atom separates the construction of the map from its exact-image assertion. The old Route241 residual CandidateLowerHomData is recovered theorem-level by combining this carrier with the separate surjectivity datum below.

                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                    The exact-image part of the lower candidate homomorphism.

                                                                                                                                                                                                                    This is the literal surjectivity assertion for the carrier above; it is smaller than the old combined homomorphism packet because it contains no choice of the homomorphism.

                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                      Former Route242 carrier residual, now theorem-level from the finite admissible lower marking and candidate epimorphism semantics. The finite marking is transported to an epimorphism by GammaA_epi_equiv_admissible; the carrier stores that map together with its certified exact image.

                                                                                                                                                                                                                      Former Route242 surjectivity residual, now theorem-level: surjectivity is part of the certified carrier obtained from the finite admissible marking above.

                                                                                                                                                                                                                      The admissibility of the marking attached to an exact lower candidate image.

                                                                                                                                                                                                                      Former Route239 lower-marking atom, now theorem-level from the four smaller finite-quotient pieces: marking, generation, relators, and O₂(C) wild-core membership.

                                                                                                                                                                                                                      The h₀ factor contribution in the candidate wild-row ledger.

                                                                                                                                                                                                                      • term : Module.End (ZMod 2) (towerM K)

                                                                                                                                                                                                                        First-order contribution of h₀.

                                                                                                                                                                                                                      • shadow : self.term = 0

                                                                                                                                                                                                                        h₀ has the first-order shadow of x₀², hence zero in characteristic two.

                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                        The u₁⁻¹ factor contribution in the candidate wild-row ledger.

                                                                                                                                                                                                                        • term : Module.End (ZMod 2) (towerM K)

                                                                                                                                                                                                                          First-order contribution of u₁⁻¹.

                                                                                                                                                                                                                        • shadow : self.term = src.P * (src.T - 1) + src.P * (src.X₁ - 1)

                                                                                                                                                                                                                          The u₁⁻¹ term contributes the two norm pieces.

                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                          The x₁^σ factor contribution in the candidate wild-row ledger.

                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                            The commutator factor c₀=[d₀,z₀] contribution in the candidate wild-row ledger.

                                                                                                                                                                                                                            • term : Module.End (ZMod 2) (towerM K)

                                                                                                                                                                                                                              First-order contribution of c₀=[d₀,z₀].

                                                                                                                                                                                                                            • shadow : self.term = 0

                                                                                                                                                                                                                              The commutator c₀=[d₀,z₀] has no first-order contribution.

                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                              The product-rule/Fox fundamental sum for the four actual wild-row factors.

                                                                                                                                                                                                                              This Route241 atom contains only the formal product-rule assembly of the four already separated factor contributions; it does not identify any individual factor.

                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                The literal finite-word ledger for the candidate wild row.

                                                                                                                                                                                                                                This Route247 residual is the manuscript table of lem:h0shadow and lem:fullwordledger, specialized to the already chosen lower source map. It is strictly more literal than the former product-rule core atom: it no longer quantifies over arbitrary selected factor records. Instead, it states the evaluated four summands in the exact manuscript order

                                                                                                                                                                                                                                h₀, u₁⁻¹, x₁^σ, c₀

                                                                                                                                                                                                                                after the factor shadows have already been substituted. The formal product-rule packet for arbitrary factor records is recovered theorem-level below by rewriting those records with their shadow fields.

                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                  The manuscript factor-table version of the finite-word ledger.

                                                                                                                                                                                                                                  This is one step below the former literal-row atom: instead of asserting the already summed row, it records the four factor contributions in the order of lem:fullwordledger (h₀, u₁⁻¹, x₁^σ, c₀) together with their shadows from lem:h0shadow and the raw Fox product rule for the actual lower wild relator. The literal summed row is recovered theorem-level by substituting these four shadows.

                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                    The h₀ row of the manuscript finite-word ledger (lem:h0shadow): the first-order shadow of h₀ is the shadow of x₀², hence zero in characteristic two.

                                                                                                                                                                                                                                    • h0Term : Module.End (ZMod 2) (towerM K)

                                                                                                                                                                                                                                      First-order contribution of h₀.

                                                                                                                                                                                                                                    • h0_shadow : self.h0Term = 0

                                                                                                                                                                                                                                      h₀ contributes zero in the elementary row.

                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                      The u₁⁻¹ row of the manuscript finite-word ledger.

                                                                                                                                                                                                                                      • u1InvTerm : Module.End (ZMod 2) (towerM K)

                                                                                                                                                                                                                                        First-order contribution of u₁⁻¹.

                                                                                                                                                                                                                                      • u1_inv_shadow : self.u1InvTerm = src.P * (src.T - 1) + src.P * (src.X₁ - 1)

                                                                                                                                                                                                                                        The inverse norm term contributes P(T-1) + P(X₁-1).

                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                        The x₁^σ row of the manuscript finite-word ledger.

                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                          The c₀=[d₀,z₀] row of the manuscript finite-word ledger.

                                                                                                                                                                                                                                          • c0Term : Module.End (ZMod 2) (towerM K)

                                                                                                                                                                                                                                            First-order contribution of c₀=[d₀,z₀].

                                                                                                                                                                                                                                          • c0_shadow : self.c0Term = 0

                                                                                                                                                                                                                                            The commutator factor has no first-order contribution.

                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                            The raw product-rule row for the actual lower wild relator, after the four manuscript factor terms have been chosen but before substituting their evaluated shadows.

                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                              Route250 split of the five manuscript wild-row atoms #

                                                                                                                                                                                                                                              The term-carrier half of the h₀ row: it chooses the first-order contribution of h₀ before proving the lem:h0shadow zero evaluation.

                                                                                                                                                                                                                                              • h0Term : Module.End (ZMod 2) (towerM K)

                                                                                                                                                                                                                                                First-order contribution of h₀.

                                                                                                                                                                                                                                              • h0Term_shadow : self.h0Term = 0

                                                                                                                                                                                                                                                The chosen h₀ term has the zero shadow from lem:h0shadow.

                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                The shadow half of the h₀ row (lem:h0shadow): the chosen h₀ term is zero.

                                                                                                                                                                                                                                                • h0_shadow : term.h0Term = 0

                                                                                                                                                                                                                                                  h₀ contributes zero in the elementary row.

                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                  The term-carrier half of the u₁⁻¹ row.

                                                                                                                                                                                                                                                  • u1InvTerm : Module.End (ZMod 2) (towerM K)

                                                                                                                                                                                                                                                    First-order contribution of u₁⁻¹.

                                                                                                                                                                                                                                                  • u1InvTerm_shadow : self.u1InvTerm = src.P * (src.T - 1) + src.P * (src.X₁ - 1)

                                                                                                                                                                                                                                                    The inverse norm term contributes P(T-1) + P(X₁-1).

                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                    The shadow half of the u₁⁻¹ row: the inverse ω₂-norm factor contributes P(T-1) + P(X₁-1).

                                                                                                                                                                                                                                                    • u1_inv_shadow : term.u1InvTerm = src.P * (src.T - 1) + src.P * (src.X₁ - 1)

                                                                                                                                                                                                                                                      The inverse norm term contributes P(T-1) + P(X₁-1).

                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                      The term-carrier half of the x₁^σ row.

                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                        The shadow half of the x₁^σ row: conjugation by σ contributes S⁻¹.

                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                          The term-carrier half of the commutator row c₀=[d₀,z₀].

                                                                                                                                                                                                                                                          • c0Term : Module.End (ZMod 2) (towerM K)

                                                                                                                                                                                                                                                            First-order contribution of c₀=[d₀,z₀].

                                                                                                                                                                                                                                                          • c0Term_shadow : self.c0Term = 0

                                                                                                                                                                                                                                                            The commutator factor has no first-order contribution.

                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                            The shadow half of the commutator row: c₀ has no first-order contribution.

                                                                                                                                                                                                                                                            • c0_shadow : term.c0Term = 0

                                                                                                                                                                                                                                                              The commutator factor has no first-order contribution.

                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                              The Fox-derivative expansion part of the product rule for the actual wild relator.

                                                                                                                                                                                                                                                              This is strictly before the final relator-triviality cancellation: it says that the sum of the four manuscript factor rows is the derivative expansion of the evaluated wild relator, namely ρ(wildRelator) - 1 on M. The theorem below supplies the final ρ(wildRelator)-1 = 0 cancellation from src.wild_rel / hwild.

                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                The literal, already evaluated, Fox-derivative row for the actual four-factor wild relator after substituting the manuscript factor shadows. This is the remaining finite-word expansion datum; the individual term carriers and shadows below are now chosen theorem-level.

                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                  Collapsed manuscript input for the Fox derivative of the actual wild relator.

                                                                                                                                                                                                                                                                  This is one step smaller than the former literal expanded row: it records the derivative as the two manuscript operator blocks P(T-1) and (P+S⁻¹)(X₁-1). The displayed four-summand literal row is recovered theorem-level below by distributivity and additive regrouping.

                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                    Block-carrier form of the collapsed candidate wild-row Fox derivative.

                                                                                                                                                                                                                                                                    The manuscript row is split into its two operator blocks, the norm block P(T-1) and the x₁ block (P+S⁻¹)(X₁-1), plus the product-rule expansion for the sum of these blocks. The checkpoint-255 collapsed expression is recovered by substituting the two block shadows.

                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                      Term-level Fox product rule for the actual four-factor wild relator.

                                                                                                                                                                                                                                                                      This is below the collapsed two-block row: the four manuscript factor terms are still visible, and the row is only collapsed after substituting the already-proved shadows for h₀, u₁⁻¹, x₁^σ, and c₀.

                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                        Canonical four-factor Fox product rule for the actual manuscript wild word.

                                                                                                                                                                                                                                                                        This is below the checkpoint-257 term-carrier product rule: it states the product rule only after substituting the canonical manuscript first-order terms for h₀, u₁⁻¹, x₁^σ, and c₀. The carrier-dependent statement is recovered by the four term-shadow equalities.

                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                          Canonical four-factor row after the manuscript word ledger and final relator cancellation.

                                                                                                                                                                                                                                                                          This is below the checkpoint-258 product-rule atom: it no longer carries the target r-1, because that term is theorem-level zero once the evaluated wild relator is 1. It is the factor-ordered row of lem:fullwordledger after substituting the canonical contributions of h₀, u₁⁻¹, x₁^σ, and c₀.

                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                            Checkpoint262: lower the canonical product-rule core to prefix-factor shadows #

                                                                                                                                                                                                                                                                            The pure four-factor Fox/product-rule sum for the evaluated manuscript wild word.

                                                                                                                                                                                                                                                                            This is purely algebraic: it is the telescoping product-rule expression (ρ a - 1) + ρ(a)(ρ b - 1) + ρ(ab)(ρ c - 1) + ρ(abc)(ρ d - 1) for a=h₀, b=u₁⁻¹, c=x₁^σ, and d=c₀. The factor-specific manuscript ledger is kept out of this definition and isolated in the four prefix-shadow atoms below.

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

                                                                                                                                                                                                                                                                              Pure four-factor product rule for the evaluated wild word.

                                                                                                                                                                                                                                                                              The proof is independent of the manuscript row calculation and independent of the candidate relator-shadow chain: after unfolding only the top-level definition of Q2Word.wildRelator, it is the standard noncommutative telescoping identity ρ(abcd)-1 = (ρa-1)+ρa(ρb-1)+ρ(ab)(ρc-1)+ρ(abc)(ρd-1).

                                                                                                                                                                                                                                                                              Prefix-shadow datum for the h₀ manuscript factor.

                                                                                                                                                                                                                                                                              This is one of the four smaller manuscript-row atoms replacing the former single canonical product-rule core. It identifies the chosen first-order h₀ row with its prefix Fox contribution ρ(h₀)-1; the already-existing shadow field then says this contribution is zero in the elementary row.

                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                Lower zero-degree manuscript atom for the h₀ factor.

                                                                                                                                                                                                                                                                                This is strictly below the former H0PrefixShadowData: it no longer mentions an arbitrary first-order term carrier. It records only the factor-action consequence of lem:h0shadow needed by the prefix product rule, namely that the actual evaluated h₀ factor acts trivially on the elementary module M.

                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                  Lower finite-word atom for the inverse norm factor u₁⁻¹.

                                                                                                                                                                                                                                                                                  This is below the former U1InvPrefixShadowData: it is independent of the chosen term carrier and states the actual Fox calculation for the u₁⁻¹ factor itself. The prefix multiplier ρ(h₀) is inserted theorem-level using H0PrefixActionData.

                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                    Lower prefix finite-word atom for the conjugate factor x₁^σ.

                                                                                                                                                                                                                                                                                    This is below the former X1ConjPrefixShadowData: it no longer refers to the selected term carrier, and records only the manuscript Fox-prefix calculation for the actual third factor of h₀ u₁⁻¹ x₁^σ c₀.

                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                      Lower prefix finite-word atom for the commutator factor c₀=[d₀,z₀].

                                                                                                                                                                                                                                                                                      This is below the former C0PrefixShadowData: it removes the term carrier and records only the zero first-order prefix contribution of the actual commutator factor from the manuscript ledger.

                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                        Checkpoint264: lower the four factor/Fox atoms to internal word/Fox ledgers #

                                                                                                                                                                                                                                                                                        The internal six-factor Fox sum of h₀.

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

                                                                                                                                                                                                                                                                                          The internal Fox sum of the conjugate factor x₁^σ, including the already accrued external prefix h₀u₁⁻¹.

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

                                                                                                                                                                                                                                                                                            The internal Fox sum of the commutator factor c₀=[d₀,z₀], including the already accrued external prefix h₀u₁⁻¹x₁^σ.

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

                                                                                                                                                                                                                                                                                              Lower internal manuscript atom for h₀: the six-factor Fox sum of x₀^{g₀} x₀ d_g d₀ d₀² h_c vanishes.

                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                Lower internal manuscript atom for u₁⁻¹: the inverse rule has been separated from the ω₂-norm Fox calculation for u₁=(x₁τ)^{ω₂}.

                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                  Lower internal manuscript atom for x₁^σ: expand the conjugate σ⁻¹ x₁ σ before collapsing it to the third-prefix row.

                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                    Lower internal manuscript atom for c₀=[d₀,z₀]: expand the commutator before collapsing it to a zero fourth-prefix contribution.

                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                      Checkpoint265: split the internal Fox leaves into factor-row data #

                                                                                                                                                                                                                                                                                                      Row-level finite-word data for the six internal factors of h₀ = x₀^{g₀} x₀ d_g d₀ d₀² h_c.

                                                                                                                                                                                                                                                                                                      This is below the checkpoint264 H0ExpandedFoxData leaf: the six Fox summands are named separately, and the residual cancellation is only the sum of these six rows.

                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                        Row-level finite-word data for the inverse ω₂-norm factor u₁⁻¹.

                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                          Row-level finite-word data for the conjugate x₁^σ=σ⁻¹x₁σ.

                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                            Row-level finite-word data for the commutator c₀=[d₀,z₀].

                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                              Checkpoint266: row-data leaves lowered to canonical row-sum leaves #

                                                                                                                                                                                                                                                                                                              Canonical row from the first internal h₀ factor x₀^{g₀}.

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

                                                                                                                                                                                                                                                                                                                Canonical row from the second internal h₀ factor x₀.

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

                                                                                                                                                                                                                                                                                                                  Canonical row from the internal h₀ factor d_g.

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

                                                                                                                                                                                                                                                                                                                    Canonical row from the internal h₀ factor d₀.

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

                                                                                                                                                                                                                                                                                                                      Canonical row from the internal h₀ factor d₀².

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

                                                                                                                                                                                                                                                                                                                        Canonical row from the final internal h₀ factor h_c.

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

                                                                                                                                                                                                                                                                                                                          Canonical row from the leading σ⁻¹ in x₁^σ.

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

                                                                                                                                                                                                                                                                                                                            Canonical row from the middle x₁ in x₁^σ.

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

                                                                                                                                                                                                                                                                                                                              Canonical row from the closing σ in x₁^σ.

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

                                                                                                                                                                                                                                                                                                                                Canonical row from the factor d₀⁻¹ in c₀=[d₀,z₀].

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

                                                                                                                                                                                                                                                                                                                                  Canonical row from the factor z₀⁻¹ in c₀=[d₀,z₀].

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

                                                                                                                                                                                                                                                                                                                                    Canonical row from the factor d₀ in c₀=[d₀,z₀].

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

                                                                                                                                                                                                                                                                                                                                      Canonical row from the factor z₀ in c₀=[d₀,z₀].

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

                                                                                                                                                                                                                                                                                                                                        Checkpoint269: current action leaves lowered to composable action identities #

                                                                                                                                                                                                                                                                                                                                        Checkpoint332 lower primitive for the h₀ head: keep only the additive zero of the inverse-preimage row. The checkpoint331 adjacent u₀⁻¹*u₀ cancellation target is recovered theorem-level by applying u₀ and cancelling the displayed inverse pair.

                                                                                                                                                                                                                                                                                                                                        Checkpoint332 bridge recovering the checkpoint331 h₀ head adjacent cancellation row from the lower inverse-preimage difference-zero primitive.

                                                                                                                                                                                                                                                                                                                                        Checkpoint331 bridge closing the checkpoint330 h₀ head difference-zero residual from the lower adjacent-cancellation row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint329 bridge for the checkpoint328 h₀ head atom: reapply x₀ to the inverse-preimage equality and cancel x₀*x₀⁻¹.

                                                                                                                                                                                                                                                                                                                                        Checkpoint328 bridge for the checkpoint327 h₀ head atom: the lower datum states the core equality before reapplying the visible outer g action. Apply g and cancel g*g⁻¹ in the opened core.

                                                                                                                                                                                                                                                                                                                                        Checkpoint327 bridge for the checkpoint326 h₀ head atom: the new datum states the same core row before applying the visible outer g⁻¹ action. Apply g⁻¹ and cancel g⁻¹*g on the left.

                                                                                                                                                                                                                                                                                                                                        Checkpoint326 bridge for the checkpoint325 h₀ head atom: apply x₀⁻¹ to the lower core-opened equality and cancel the visible inverse pair.

                                                                                                                                                                                                                                                                                                                                        Checkpoint325 bridge for the h₀ head: reapply u₀ to the lower preimage row and cancel the adjacent u₀*u₀⁻¹ pair.

                                                                                                                                                                                                                                                                                                                                        Checkpoint324 bridge for the h₀ head: reapply the visible x₀ · u₀⁻¹ prefix to the new preimage-core row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint323 bridge for the h₀ head: the checkpoint322 row with the two opened σ₂ actions follows from the stripped-core row by reapplying g = σ₂².

                                                                                                                                                                                                                                                                                                                                        Checkpoint322 bridge for the h₀ head: the checkpoint321 g-core-opened row follows from the lower row in which the two visible g = σ₂² actions have already been opened as successive σ₂ tower actions.

                                                                                                                                                                                                                                                                                                                                        Checkpoint320 bridge for the h₀ head: the old fully stripped preimage-core row is recovered from the checkpoint321 row by applying g⁻¹ and cancelling the outer g⁻¹*g action pair.

                                                                                                                                                                                                                                                                                                                                        Checkpoint319 bridge for the h₀ head: the applied-u₀⁻¹ preimage row is recovered from the checkpoint320 row by applying x₀⁻¹ and cancelling the visible x₀⁻¹*x₀ action pair.

                                                                                                                                                                                                                                                                                                                                        Checkpoint318 bridge for the h₀ head: the checkpoint317 stripped-preimage row follows from the still smaller row with the remaining u₀⁻¹ action removed from the left hand side.

                                                                                                                                                                                                                                                                                                                                        Checkpoint317 bridge for the h₀ head: the checkpoint316 head row is recovered from the row with the outer x₀ action removed by reapplying x₀ and cancelling x₀*x₀⁻¹.

                                                                                                                                                                                                                                                                                                                                        Checkpoint315 h₀ head atom, now theorem-level from the checkpoint316 fully stripped preimage-core row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint314 h₀ head atom, now theorem-level from the checkpoint315 prefix-stripped preimage core.

                                                                                                                                                                                                                                                                                                                                        Checkpoint312 fully nested head row, now theorem-level from the smaller inner action rewrite immediately above.

                                                                                                                                                                                                                                                                                                                                        Checkpoint332 lower primitive for the h₀ tail: retain only the additive zero of the stripped inverse-preimage row. The checkpoint331 row is recovered by applying the visible x₀ action and cancelling x₀*x₀⁻¹.

                                                                                                                                                                                                                                                                                                                                        Checkpoint328 bridge for the checkpoint327 h₀ tail atom: the lower datum is the inverse-preimage equality after the x₀ action has already been applied. Apply x₀⁻¹, then u₀, and cancel the two displayed inverse pairs.

                                                                                                                                                                                                                                                                                                                                        Checkpoint327 bridge for the checkpoint326 h₀ tail atom: the new datum states the row after applying u₀ to the visible x₀⁻¹ preimage. Apply u₀⁻¹ and then x₀, cancelling the two adjacent inverse-action pairs.

                                                                                                                                                                                                                                                                                                                                        Checkpoint326 bridge for the checkpoint325 h₀ tail atom: apply x₀⁻¹ to the lower core-opened equality and cancel the adjacent inverse pair.

                                                                                                                                                                                                                                                                                                                                        Checkpoint323 bridge for the h₀ tail: reapply g = σ₂² to the stripped precore row and rewrite the product action as two successive σ₂ actions.

                                                                                                                                                                                                                                                                                                                                        Checkpoint322 bridge for the h₀ tail: recover the checkpoint321 opened-g precore row from the lower statement where the left g = σ₂² action is already split into two successive σ₂ actions.

                                                                                                                                                                                                                                                                                                                                        Checkpoint320 bridge for the h₀ tail: recover the fully stripped precore row from the checkpoint321 row by applying g⁻¹ and cancelling g⁻¹*g.

                                                                                                                                                                                                                                                                                                                                        Checkpoint319 bridge for the h₀ tail: the applied-x₀⁻¹ preimage row is recovered from the checkpoint320 row by applying u₀⁻¹ and cancelling the visible u₀⁻¹*u₀ action pair.

                                                                                                                                                                                                                                                                                                                                        Checkpoint318 bridge for the h₀ tail: the checkpoint317 row follows by reapplying the stripped x₀⁻¹ and u₀ actions and cancelling the adjacent inverse-action pairs.

                                                                                                                                                                                                                                                                                                                                        Checkpoint317 bridge for the h₀ tail: the checkpoint316 tail row is recovered from the row with the visible u₀⁻¹ preimage removed by applying u₀⁻¹ and cancelling u₀⁻¹*u₀.

                                                                                                                                                                                                                                                                                                                                        Checkpoint311 nested tail-to-z₀⁻¹ row, recovered theorem-level from the checkpoint312 row after cancelling the common outer g⁻¹ action.

                                                                                                                                                                                                                                                                                                                                        Checkpoint308 list datum for h₀, now theorem-level from the still more literal row in which the final z₀⁻¹ = g⁻¹*x₀⁻¹*g action has been opened into its three successive tower-action factors.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveTowerActionSixFactorD0ExpandedRawInlineSevenActionTailTripleInverseCancellationHcNestedDgInvD0SplitD0InvOpenedAllProductActionsSplitApplyPointwiseData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        ((towerActM K) (powOmega2 src.sigma ^ 2)⁻¹) (((towerActM K) src.x₀) (((towerActM K) (powOmega2 (src.x₀ * src.tau))⁻¹) (((towerActM K) (powOmega2 src.sigma ^ 2)) (((towerActM K) src.x₀) (((towerActM K) (powOmega2 (src.x₀ * src.tau))⁻¹) (((towerActM K) (powOmega2 src.sigma ^ 2)⁻¹) (((towerActM K) (powOmega2 (src.x₀ * src.tau))) (((towerActM K) src.x₀⁻¹) (((towerActM K) (powOmega2 src.sigma ^ 2)) (((towerActM K) (powOmega2 (src.x₀ * src.tau))) (((towerActM K) src.x₀⁻¹) m))))))))))) = ((towerActM K) src.x₀) (((towerActM K) (powOmega2 (src.x₀ * src.tau))⁻¹) (((towerActM K) src.x₀) (((towerActM K) (powOmega2 (src.x₀ * src.tau))⁻¹) (((towerActM K) src.x₀) (((towerActM K) (powOmega2 (src.x₀ * src.tau))⁻¹) (((towerActM K) (powOmega2 src.sigma ^ 2)⁻¹) (((towerActM K) src.x₀) (((towerActM K) (powOmega2 (src.x₀ * src.tau))⁻¹) (((towerActM K) (powOmega2 src.sigma ^ 2)) (((towerActM K) src.x₀⁻¹) (((towerActM K) ((powOmega2 src.sigma ^ 2)⁻¹ * src.x₀ * powOmega2 src.sigma ^ 2)⁻¹) m)))))))))))
                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveTowerActionSixFactorD0ExpandedRawInlineSevenActionTailTripleInverseCancellationHcNestedDgInvD0SplitD0InvOpenedProductActionSplitApplyPointwiseData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        ((towerActM K) (powOmega2 src.sigma ^ 2)⁻¹) (((towerActM K) src.x₀) (((towerActM K) (powOmega2 (src.x₀ * src.tau))⁻¹) (((towerActM K) (powOmega2 src.sigma ^ 2)) (((towerActM K) (src.x₀ * (powOmega2 (src.x₀ * src.tau))⁻¹)) (((towerActM K) (powOmega2 src.sigma ^ 2)⁻¹) (((towerActM K) (powOmega2 (src.x₀ * src.tau))) (((towerActM K) src.x₀⁻¹) (((towerActM K) (powOmega2 src.sigma ^ 2)) (((towerActM K) (powOmega2 (src.x₀ * src.tau))) (((towerActM K) src.x₀⁻¹) m)))))))))) = ((towerActM K) (src.x₀ * (powOmega2 (src.x₀ * src.tau))⁻¹)) (((towerActM K) (src.x₀ * (powOmega2 (src.x₀ * src.tau))⁻¹)) (((towerActM K) (src.x₀ * (powOmega2 (src.x₀ * src.tau))⁻¹)) (((towerActM K) (powOmega2 src.sigma ^ 2)⁻¹) (((towerActM K) (src.x₀ * (powOmega2 (src.x₀ * src.tau))⁻¹)) (((towerActM K) (powOmega2 src.sigma ^ 2)) (((towerActM K) src.x₀⁻¹) (((towerActM K) ((powOmega2 src.sigma ^ 2)⁻¹ * src.x₀ * powOmega2 src.sigma ^ 2)⁻¹) m)))))))
                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveTowerActionSixFactorD0ExpandedRawInlineSevenActionTailTripleInverseCancellationHcNestedDgInvD0SplitD0InvOpenedApplyPointwiseData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        ((towerActM K) (powOmega2 src.sigma ^ 2)⁻¹) (((towerActM K) (src.x₀ * (powOmega2 (src.x₀ * src.tau))⁻¹)) (((towerActM K) (powOmega2 src.sigma ^ 2)) (((towerActM K) (src.x₀ * (powOmega2 (src.x₀ * src.tau))⁻¹)) (((towerActM K) (powOmega2 src.sigma ^ 2)⁻¹) (((towerActM K) (powOmega2 (src.x₀ * src.tau))) (((towerActM K) src.x₀⁻¹) (((towerActM K) (powOmega2 src.sigma ^ 2)) (((towerActM K) (powOmega2 (src.x₀ * src.tau))) (((towerActM K) src.x₀⁻¹) m))))))))) = ((towerActM K) (src.x₀ * (powOmega2 (src.x₀ * src.tau))⁻¹)) (((towerActM K) (src.x₀ * (powOmega2 (src.x₀ * src.tau))⁻¹)) (((towerActM K) (src.x₀ * (powOmega2 (src.x₀ * src.tau))⁻¹)) (((towerActM K) (powOmega2 src.sigma ^ 2)⁻¹) (((towerActM K) (src.x₀ * (powOmega2 (src.x₀ * src.tau))⁻¹)) (((towerActM K) (powOmega2 src.sigma ^ 2)) (((towerActM K) src.x₀⁻¹) (((towerActM K) ((powOmega2 src.sigma ^ 2)⁻¹ * src.x₀ * powOmega2 src.sigma ^ 2)⁻¹) m)))))))
                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveTowerActionSixFactorD0ExpandedRawInlineSevenActionTailTripleInverseCancellationHcNestedDgInvD0SplitApplyPointwiseData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        ((towerActM K) (powOmega2 src.sigma ^ 2)⁻¹) (((towerActM K) (powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹)⁻¹) (((towerActM K) (powOmega2 src.sigma ^ 2)) (((towerActM K) (powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹)⁻¹) (((towerActM K) (powOmega2 src.sigma ^ 2)⁻¹) (((towerActM K) (powOmega2 (src.x₀ * src.tau))) (((towerActM K) src.x₀⁻¹) (((towerActM K) (powOmega2 src.sigma ^ 2)) (((towerActM K) (powOmega2 (src.x₀ * src.tau))) (((towerActM K) src.x₀⁻¹) m))))))))) = ((towerActM K) (powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹)⁻¹) (((towerActM K) (powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹)⁻¹) (((towerActM K) (powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹)⁻¹) (((towerActM K) (powOmega2 src.sigma ^ 2)⁻¹) (((towerActM K) (powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹)⁻¹) (((towerActM K) (powOmega2 src.sigma ^ 2)) (((towerActM K) src.x₀⁻¹) (((towerActM K) ((powOmega2 src.sigma ^ 2)⁻¹ * src.x₀ * powOmega2 src.sigma ^ 2)⁻¹) m)))))))

                                                                                                                                                                                                                                                                                                                                        Checkpoint303 primitive datum for h₀, now theorem-level from the checkpoint304 split of the remaining d_g⁻¹ action.

                                                                                                                                                                                                                                                                                                                                        Checkpoint302 primitive datum for h₀, now theorem-level from the checkpoint303 pointwise split of the two visible non-inverse d₀ actions.

                                                                                                                                                                                                                                                                                                                                        Checkpoint300 primitive datum for h₀, now theorem-level from the checkpoint301 fully inlined tail-triple row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint299 primitive datum for h₀, now theorem-level from the checkpoint300 tail-triple inverse cancellation core.

                                                                                                                                                                                                                                                                                                                                        Checkpoint298 primitive atom for h₀, now theorem-level from the checkpoint299 head-inverse/tail-cancellation datum.

                                                                                                                                                                                                                                                                                                                                        Checkpoint297 primitive atom for h₀, now theorem-level from the fully inlined checkpoint298 pointwise value row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint296 h₀ zero-deviation atom, now theorem-level from the literal raw seven-action value equality. This exposes the point-value computation as the new leaf instead of assuming the subtraction-normalized form.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveTowerActionSixFactorD0ExpandedRawNestedD0SquareExpandedFixesPointTowerApplyPointwiseData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        have sigma2 := powOmega2 src.sigma; have g0 := sigma2 ^ 2; have d0 := powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹; have dg := g0⁻¹ * d0 * g0; have hc := dg⁻¹ * d0⁻¹ * dg * d0; have a := g0⁻¹ * src.x₀ * g0; have b := src.x₀; ((towerActM K) a) (((towerActM K) b) (((towerActM K) dg) (((towerActM K) d0) (((towerActM K) d0) (((towerActM K) d0) (((towerActM K) hc) m)))))) = m

                                                                                                                                                                                                                                                                                                                                        Checkpoint295 lower atom for h₀, now theorem-level from the still more literal zero-deviation seven-action atom above.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveTowerActionSixFactorD0ExpandedRawNestedFixesPointTowerApplyPointwiseData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        have sigma2 := powOmega2 src.sigma; have g0 := sigma2 ^ 2; have d0 := powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹; have dg := g0⁻¹ * d0 * g0; have hc := dg⁻¹ * d0⁻¹ * dg * d0; have a := g0⁻¹ * src.x₀ * g0; have b := src.x₀; have d0sq := d0 ^ 2; ((towerActM K) a) (((towerActM K) b) (((towerActM K) dg) (((towerActM K) d0) (((towerActM K) d0sq) (((towerActM K) hc) m))))) = m

                                                                                                                                                                                                                                                                                                                                        Checkpoint294 nested six-factor datum, now theorem-level from the still more literal pointwise atom where the d₀² action has been expanded into two d₀ actions.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveTowerActionSixFactorD0ExpandedRawProductFixesPointTowerApplyPointwiseData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        have sigma2 := powOmega2 src.sigma; have g0 := sigma2 ^ 2; have d0 := powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹; have dg := g0⁻¹ * d0 * g0; have hc := dg⁻¹ * d0⁻¹ * dg * d0; have a := g0⁻¹ * src.x₀ * g0; have b := src.x₀; have d0sq := d0 ^ 2; ((towerActM K) (a * b * dg * d0 * d0sq * hc)) m = m

                                                                                                                                                                                                                                                                                                                                        Checkpoint293 product-action fixed-point atom for h₀, now theorem-level from the literal nested six-factor action datum.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveTowerActionSixFactorD0ExpandedRawProductFoxRowTowerApplyPointwiseData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        have sigma2 := powOmega2 src.sigma; have g0 := sigma2 ^ 2; have d0 := powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹; have dg := g0⁻¹ * d0 * g0; have hc := dg⁻¹ * d0⁻¹ * dg * d0; have a := g0⁻¹ * src.x₀ * g0; have b := src.x₀; have d0sq := d0 ^ 2; ((towerActM K) a) m - m + ((towerActM K) a) (((towerActM K) b) m - m) + ((towerActM K) a) (((towerActM K) b) (((towerActM K) dg) m - m)) + ((towerActM K) a) (((towerActM K) b) (((towerActM K) dg) (((towerActM K) d0) m - m))) + ((towerActM K) a) (((towerActM K) b) (((towerActM K) dg) (((towerActM K) d0) (((towerActM K) d0sq) m - m)))) + ((towerActM K) a) (((towerActM K) b) (((towerActM K) dg) (((towerActM K) d0) (((towerActM K) d0sq) (((towerActM K) hc) m - m))))) = 0

                                                                                                                                                                                                                                                                                                                                        Checkpoint292 raw h₀ six-factor Fox row, now theorem-level from the smaller product-fixed-point datum and the formal six-factor product rule.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveTowerActionSixFactorD0ExpandedRawProductFoxRowApplyPointwiseData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        have sigma2 := powOmega2 src.sigma; have g0 := sigma2 ^ 2; have d0 := powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹; have dg := g0⁻¹ * d0 * g0; have hc := dg⁻¹ * d0⁻¹ * dg * d0; have a := g0⁻¹ * src.x₀ * g0; have b := src.x₀; have d0sq := d0 ^ 2; have ρ := sec7MStageCandidateActionEnd K; (ρ a - 1 + ρ a * (ρ b - 1) + ρ a * ρ b * (ρ dg - 1) + ρ a * ρ b * ρ dg * (ρ d0 - 1) + ρ a * ρ b * ρ dg * ρ d0 * (ρ d0sq - 1) + ρ a * ρ b * ρ dg * ρ d0 * ρ d0sq * (ρ hc - 1)) m = 0

                                                                                                                                                                                                                                                                                                                                        Checkpoint291 h₀ pointwise endomorphism row, now theorem-level from the raw towerActM six-factor pointwise row.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveTowerActionSixFactorD0ExpandedRawProductFoxRowOperatorData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) :
                                                                                                                                                                                                                                                                                                                                        have sigma2 := powOmega2 src.sigma; have g0 := sigma2 ^ 2; have d0 := powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹; have dg := g0⁻¹ * d0 * g0; have hc := dg⁻¹ * d0⁻¹ * dg * d0; have a := g0⁻¹ * src.x₀ * g0; have b := src.x₀; have d0sq := d0 ^ 2; have ρ := sec7MStageCandidateActionEnd K; ρ a - 1 + ρ a * (ρ b - 1) + ρ a * ρ b * (ρ dg - 1) + ρ a * ρ b * ρ dg * (ρ d0 - 1) + ρ a * ρ b * ρ dg * ρ d0 * (ρ d0sq - 1) + ρ a * ρ b * ρ dg * ρ d0 * ρ d0sq * (ρ hc - 1) = 0

                                                                                                                                                                                                                                                                                                                                        Former checkpoint290 h₀ operator row, now theorem-level from the pointwise applied six-factor row.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveTowerActionSixFactorD0ExpandedRawProductOperatorData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) :
                                                                                                                                                                                                                                                                                                                                        have sigma2 := powOmega2 src.sigma; have g0 := sigma2 ^ 2; have d0 := powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹; have dg := g0⁻¹ * d0 * g0; have hc := dg⁻¹ * d0⁻¹ * dg * d0; have a := g0⁻¹ * src.x₀ * g0; have b := src.x₀; have d0sq := d0 ^ 2; have A := ↑((towerActM K) (a * b * dg * d0 * d0sq * hc)); A = 1

                                                                                                                                                                                                                                                                                                                                        Checkpoint289 lower atom for h₀, now theorem-level from the still-lower six-factor Fox row.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveTowerActionSixFactorD0ExpandedRawProductValueApplyPointwiseData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        have sigma2 := powOmega2 src.sigma; have g0 := sigma2 ^ 2; have d0 := powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹; have dg := g0⁻¹ * d0 * g0; have hc := dg⁻¹ * d0⁻¹ * dg * d0; have a := g0⁻¹ * src.x₀ * g0; have b := src.x₀; have d0sq := d0 ^ 2; ((towerActM K) (a * b * dg * d0 * d0sq * hc)) m = m

                                                                                                                                                                                                                                                                                                                                        Checkpoint287 pointwise h₀ residual, now theorem-level from the checkpoint288 operator residual. The proof is intentionally pointwise and avoids any broad simp over the six manuscript factors.

                                                                                                                                                                                                                                                                                                                                        Checkpoint287 lowering for the rooted h₀ tower-action atom. The residual is now the single concrete action of the literal six-factor manuscript product, rather than the fully nested application of the six primitive actions. The old checkpoint286 pointwise nested statement is recovered only from functoriality of towerActM K : towerC K →* (towerM K ≃ₗ[ZMod 2] towerM K).

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveActionSixFactorD0ExpandedRawNestedValueApplyPointwiseData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        have ρ := sec7MStageCandidateActionEnd K; have sigma2 := powOmega2 src.sigma; have g0 := sigma2 ^ 2; have d0 := powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹; (ρ (g0⁻¹ * src.x₀ * g0)) ((ρ src.x₀) ((ρ (g0⁻¹ * d0 * g0)) ((ρ d0) ((ρ (d0 ^ 2)) ((ρ ((g0⁻¹ * d0 * g0)⁻¹ * d0⁻¹ * (g0⁻¹ * d0 * g0) * d0)) m))))) = m

                                                                                                                                                                                                                                                                                                                                        Checkpoint284 h₀ residual, now theorem-level from the checkpoint285 concrete towerActM six-factor statement above.

                                                                                                                                                                                                                                                                                                                                        This proof deliberately avoids the failed checkpoint285 simp bridge through nested endomorphism coercions. Instead it keeps all manuscript group factors opaque and uses a single change to forget the applied endomorphism action pointwise, matching the concrete tower-action statement exactly.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveActionSixFactorD0ExpandedProductFixesPointData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        have ρ := sec7MStageCandidateActionEnd K; have sigma2 := powOmega2 src.sigma; have g0 := sigma2 ^ 2; have d0 := powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹; have dg := g0⁻¹ * d0 * g0; have hc := dg⁻¹ * d0⁻¹ * dg * d0; have a := g0⁻¹ * src.x₀ * g0; have b := src.x₀; have d0sq := d0 ^ 2; have prod := ρ a * ρ b * ρ dg * ρ d0 * ρ d0sq * ρ hc; prod m = m

                                                                                                                                                                                                                                                                                                                                        Checkpoint282 lower atom for h₀, now theorem-level from the checkpoint283 raw nested primitive-action value.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveActionSixFactorD0ExpandedRawApplyPointwiseData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        have ρ := sec7MStageCandidateActionEnd K; have sigma2 := powOmega2 src.sigma; have g0 := sigma2 ^ 2; have d0 := powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹; have dg := g0⁻¹ * d0 * g0; have hc := dg⁻¹ * d0⁻¹ * dg * d0; have a := g0⁻¹ * src.x₀ * g0; have b := src.x₀; have d0sq := d0 ^ 2; have prod := ρ a * ρ b * ρ dg * ρ d0 * ρ d0sq * ρ hc; prod m - m = 0

                                                                                                                                                                                                                                                                                                                                        Checkpoint281 lower atom for h₀, now theorem-level from the checkpoint282 primitive fixed-point statement.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveActionSixFactorD0ExpandedSubOneApplyPointwiseData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        have ρ := sec7MStageCandidateActionEnd K; have sigma2 := powOmega2 src.sigma; have g0 := sigma2 ^ 2; have d0 := powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹; have dg := g0⁻¹ * d0 * g0; have hc := dg⁻¹ * d0⁻¹ * dg * d0; have a := g0⁻¹ * src.x₀ * g0; have b := src.x₀; have d0sq := d0 ^ 2; have prod := ρ a * ρ b * ρ dg * ρ d0 * ρ d0sq * ρ hc; (prod - 1) m = 0

                                                                                                                                                                                                                                                                                                                                        Checkpoint279 lower atom for h₀, now theorem-level from the checkpoint281 raw pointwise displacement form.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveActionSixFactorD0ExpandedNestedApplyPointwiseData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        have ρ := sec7MStageCandidateActionEnd K; have sigma2 := powOmega2 src.sigma; have g0 := sigma2 ^ 2; have d0 := powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹; (ρ (g0⁻¹ * src.x₀ * g0)) ((ρ src.x₀) ((ρ (g0⁻¹ * d0 * g0)) ((ρ d0) ((ρ (d0 ^ 2)) ((ρ ((g0⁻¹ * d0 * g0)⁻¹ * d0⁻¹ * (g0⁻¹ * d0 * g0) * d0)) m))))) = m

                                                                                                                                                                                                                                                                                                                                        Checkpoint278 primitive nested h₀ action atom, now theorem-level from the smaller six-factor deviation identity.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveActionSixFactorNestedApplyPointwiseData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        have ρ := sec7MStageCandidateActionEnd K; have sigma2 := powOmega2 src.sigma; have g0 := sigma2 ^ 2; have d0 := powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹; have dg := g0⁻¹ * d0 * g0; have hc := dg⁻¹ * d0⁻¹ * dg * d0; have a := g0⁻¹ * src.x₀ * g0; have b := src.x₀; have d0sq := d0 ^ 2; (ρ a) ((ρ b) ((ρ dg) ((ρ d0) ((ρ d0sq) ((ρ hc) m))))) = m

                                                                                                                                                                                                                                                                                                                                        Checkpoint277 primitive six-factor nested-application atom, now theorem-level from the still more literal d₀-expanded nested action atom.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveActionSixFactorFixedPointwiseData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        have ρ := sec7MStageCandidateActionEnd K; have sigma2 := powOmega2 src.sigma; have g0 := sigma2 ^ 2; have d0 := powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹; have dg := g0⁻¹ * d0 * g0; have hc := dg⁻¹ * d0⁻¹ * dg * d0; have a := g0⁻¹ * src.x₀ * g0; have b := src.x₀; have d0sq := d0 ^ 2; (ρ a * ρ b * ρ dg * ρ d0 * ρ d0sq * ρ hc) m = m

                                                                                                                                                                                                                                                                                                                                        Checkpoint276 primitive six-factor fixed-point atom for h₀, now theorem-level from the still more literal nested application of the six primitive actions.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveActionH0TrivialPointwiseData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        have ρ := sec7MStageCandidateActionEnd K; have sigma2 := powOmega2 src.sigma; have g0 := sigma2 ^ 2; have d0 := powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹; have dg := g0⁻¹ * d0 * g0; have hc := dg⁻¹ * d0⁻¹ * dg * d0; have a := g0⁻¹ * src.x₀ * g0; have b := src.x₀; have d0sq := d0 ^ 2; (ρ (a * b * dg * d0 * d0sq * hc) - 1) m = 0

                                                                                                                                                                                                                                                                                                                                        Checkpoint275 primitive h₀ deviation row, now theorem-level from the lower fixed-point action product atom.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveActionSixFactorRowsPointwiseData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        have ρ := sec7MStageCandidateActionEnd K; have sigma2 := powOmega2 src.sigma; have g0 := sigma2 ^ 2; have d0 := powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹; have dg := g0⁻¹ * d0 * g0; have hc := dg⁻¹ * d0⁻¹ * dg * d0; have a := g0⁻¹ * src.x₀ * g0; have b := src.x₀; have d0sq := d0 ^ 2; (ρ a - 1 + ρ a * (ρ b - 1) + ρ (a * b) * (ρ dg - 1) + ρ (a * b * dg) * (ρ d0 - 1) + ρ (a * b * dg * d0) * (ρ d0sq - 1) + ρ (a * b * dg * d0 * d0sq) * (ρ hc - 1)) m = 0

                                                                                                                                                                                                                                                                                                                                        Checkpoint274 pointwise primitive action-row atom for h₀, now theorem-level from triviality of the evaluated manuscript word h₀ plus the six-factor product rule.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedPrimitiveActionSixFactorRowsSumZeroData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) :
                                                                                                                                                                                                                                                                                                                                        have ρ := sec7MStageCandidateActionEnd K; have sigma2 := powOmega2 src.sigma; have g0 := sigma2 ^ 2; have d0 := powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹; have dg := g0⁻¹ * d0 * g0; have hc := dg⁻¹ * d0⁻¹ * dg * d0; have a := g0⁻¹ * src.x₀ * g0; have b := src.x₀; have d0sq := d0 ^ 2; ρ a - 1 + ρ a * (ρ b - 1) + ρ (a * b) * (ρ dg - 1) + ρ (a * b * dg) * (ρ d0 - 1) + ρ (a * b * dg * d0) * (ρ d0sq - 1) + ρ (a * b * dg * d0 * d0sq) * (ρ hc - 1) = 0

                                                                                                                                                                                                                                                                                                                                        Former checkpoint273 primitive endomorphism-row atom for h₀, now theorem-level from the pointwise primitive row above.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptH0ExpandedRawEvalSixFactorRowsSumZeroData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) :

                                                                                                                                                                                                                                                                                                                                        Former checkpoint272 raw-evaluation six-row atom for h₀, now theorem-level from the direct primitive lower-quotient action statement above.

                                                                                                                                                                                                                                                                                                                                        Checkpoint296 u₁⁻¹ raw inverse-value atom, now theorem-level from the linearity-expanded value statement. The new leaf records the two visible P-images separately before recombining them as P (X m - m).

                                                                                                                                                                                                                                                                                                                                        Checkpoint294 raw inverse-deviation datum for u₁⁻¹, now theorem-level from the simpler positive-deviation equality.

                                                                                                                                                                                                                                                                                                                                        Checkpoint293 inverse-row zero-sum for u₁⁻¹, now theorem-level from the raw inverse-deviation equality.

                                                                                                                                                                                                                                                                                                                                        Checkpoint292 non-inverted u₁ row, now theorem-level by applying the u₁ action to the inverse-factor row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint291 u₁⁻¹ non-inverted pointwise endomorphism row, now theorem-level from the raw towerActM norm-row application.

                                                                                                                                                                                                                                                                                                                                        Former checkpoint290 u₁⁻¹ non-inverted row, now theorem-level by endomorphism extensionality from the pointwise row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint289 residual for u₁⁻¹, now theorem-level from the lower non-inverted norm row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint288 u₁⁻¹ operator residual, now theorem-level from the narrower checkpoint289 raw inverse-rule residual plus the local inverse-factor algebra lemma.

                                                                                                                                                                                                                                                                                                                                        Checkpoint287 lowering for u₁⁻¹: the residual is the operator identity ρ(u₁⁻¹)-1 = P(ρ(x₁)-1) in Module.End, and the old pointwise tower-action statement is only its value at m.

                                                                                                                                                                                                                                                                                                                                        Checkpoint284 u₁⁻¹ residual, now theorem-level from the checkpoint285 concrete tower-action deviation identity.

                                                                                                                                                                                                                                                                                                                                        Checkpoint283 u₁⁻¹ residual, now theorem-level from the checkpoint284 pointwise deviation identity.

                                                                                                                                                                                                                                                                                                                                        Checkpoint282 lower atom for u₁⁻¹, now theorem-level from the checkpoint283 single-deviation norm value.

                                                                                                                                                                                                                                                                                                                                        Checkpoint281 lower atom for u₁⁻¹, now theorem-level from the checkpoint282 raw pointwise value form.

                                                                                                                                                                                                                                                                                                                                        Checkpoint280 residual for u₁⁻¹, now theorem-level from the checkpoint281 raw pointwise deviation form.

                                                                                                                                                                                                                                                                                                                                        Checkpoint279 lower atom for u₁⁻¹, now theorem-level from the still more literal checkpoint280 expanded primitive-application row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint278 primitive u₁⁻¹ deviation atom, now theorem-level from the smaller inverse-deviation row plus the formal inverse-factor identity.

                                                                                                                                                                                                                                                                                                                                        Checkpoint277 expanded u₁⁻¹ application row, now theorem-level from the primitive-deviation row by linearity of the two endomorphisms.

                                                                                                                                                                                                                                                                                                                                        Checkpoint276 primitive u₁⁻¹ application row, now theorem-level from the fully expanded application of the two primitive deviations.

                                                                                                                                                                                                                                                                                                                                        Checkpoint275 primitive u₁⁻¹ row, now theorem-level from the lower application-level x₁ row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint274 pointwise primitive action-row atom for u₁⁻¹, now theorem-level from the smaller x₁-only row and the norm cancellation P(T-1)=0.

                                                                                                                                                                                                                                                                                                                                        Former checkpoint273 primitive endomorphism-row atom for u₁⁻¹, now theorem-level from the pointwise primitive norm row above.

                                                                                                                                                                                                                                                                                                                                        The bare conjugation action calculation for x₁^σ is theorem-level.

                                                                                                                                                                                                                                                                                                                                        After unfolding the three internal factors, it is the ring identity (S⁻¹ X₁ S)-1 = S⁻¹(X₁-1)S, using the already-proved inverse relation S⁻¹S=1.

                                                                                                                                                                                                                                                                                                                                        Checkpoint298 primitive atom for the P/σ⁻¹ part of x₁^σ, now theorem-level from the checkpoint299 separated-difference zero row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint297 primitive atom for the P/σ⁻¹ part of x₁^σ, now theorem-level from the grouped difference-balance checkpoint298 row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint296 P/S⁻¹ raw additive balance, now theorem-level from the subtraction-zero four-image statement. The new leaf is the literal additive zero row before applying sub_eq_zero.

                                                                                                                                                                                                                                                                                                                                        Checkpoint295 expanded untransported-deviation equality, now theorem-level from the still more literal additive balance above.

                                                                                                                                                                                                                                                                                                                                        Checkpoint294 untransported concrete x₁ deviation equality, now theorem-level from the expanded pointwise equality.

                                                                                                                                                                                                                                                                                                                                        Checkpoint293 untransported-deviation kernel for x₁^σ, now theorem-level from the raw pointwise equality of the two visible images.

                                                                                                                                                                                                                                                                                                                                        Checkpoint292 transported-deviation kernel, now theorem-level from the smaller untransported kernel statement and the formal S·S⁻¹ cancellation.

                                                                                                                                                                                                                                                                                                                                        Checkpoint291 transported-deviation kernel pointwise row, now theorem-level from its raw towerActM application form.

                                                                                                                                                                                                                                                                                                                                        Former checkpoint290 transported-deviation kernel, now theorem-level from its pointwise applied kernel form.

                                                                                                                                                                                                                                                                                                                                        Checkpoint289 residual for x₁^σ, now theorem-level from the factored transported-deviation kernel statement.

                                                                                                                                                                                                                                                                                                                                        Checkpoint288 P/S⁻¹ deviation equality, now theorem-level from the narrower checkpoint289 kernel statement.

                                                                                                                                                                                                                                                                                                                                        Checkpoint287 lowering for the P/S⁻¹ part of x₁^σ: the residual is an operator equality on the concrete x₁ deviation, not a pointwise value.

                                                                                                                                                                                                                                                                                                                                        Checkpoint284 projector/transport residual, now theorem-level from the checkpoint285 concrete tower-action deviation statement.

                                                                                                                                                                                                                                                                                                                                        Checkpoint283 x₁^σ projector/transport residual, now theorem-level from the checkpoint284 canonical S⁻¹ deviation statement.

                                                                                                                                                                                                                                                                                                                                        Checkpoint282 lower atom for x₁^σ, now theorem-level from the checkpoint283 single-deviation value equality.

                                                                                                                                                                                                                                                                                                                                        Checkpoint281 lower atom for x₁^σ, now theorem-level from the checkpoint282 expanded deviation equality.

                                                                                                                                                                                                                                                                                                                                        Checkpoint280 residual for x₁^σ, now theorem-level from the checkpoint281 fully expanded pointwise kernel balance.

                                                                                                                                                                                                                                                                                                                                        Checkpoint279 lower atom for x₁^σ, now theorem-level from the narrower checkpoint280 kernel form of the deviation-range comparison.

                                                                                                                                                                                                                                                                                                                                        Checkpoint278 primitive P(X₁-1)/σ⁻¹(X₁-1) pointwise atom, now theorem-level from the smaller deviation-image row statement.

                                                                                                                                                                                                                                                                                                                                        Checkpoint277 expanded P(X₁-1)/σ⁻¹(X₁-1) application equality, now theorem-level from the primitive-deviation row by linearity.

                                                                                                                                                                                                                                                                                                                                        Checkpoint276 primitive P(X₁-1)/σ⁻¹(X₁-1) application row, now theorem-level from the fully expanded pointwise deviation equality.

                                                                                                                                                                                                                                                                                                                                        Checkpoint275 primitive P(X₁-1)/σ⁻¹(X₁-1) row, now theorem-level from the lower application-level coordinate equality.

                                                                                                                                                                                                                                                                                                                                        Checkpoint328 bridge for the checkpoint327 transported-square zero row: the new datum isolates the single corner as the sum of the other three corners. In characteristic two this immediately gives the closed four-corner zero row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint319 bridge for the transported-square row: rewrite the raw four-corner balance as the previously exposed subtraction-zero difference of the two single-action cores.

                                                                                                                                                                                                                                                                                                                                        Checkpoint302 primitive datum for the transported-square part of x₁^σ, now theorem-level from the checkpoint303 fully distributed pointwise value row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint300 primitive datum for the transported-square part of x₁^σ, now theorem-level from the checkpoint301 fully inlined value formula.

                                                                                                                                                                                                                                                                                                                                        Checkpoint299 primitive datum for the transported-square part of x₁^σ, now theorem-level from the checkpoint300 transported-difference value formula.

                                                                                                                                                                                                                                                                                                                                        Checkpoint298 primitive atom for the transported-square part of x₁^σ, now theorem-level from the checkpoint299 transported-difference deviation row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint297 primitive atom for the transported-square part of x₁^σ, now theorem-level from the grouped delta-difference checkpoint298 row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint296 transported-square raw value atom, now theorem-level from the literal subtraction-zero form of the same expanded point-value row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint295 expanded transported-square delta step, now theorem-level from the raw value statement above.

                                                                                                                                                                                                                                                                                                                                        Checkpoint294 compact transported-square delta step, now theorem-level from the expanded pointwise equality.

                                                                                                                                                                                                                                                                                                                                        Checkpoint293 untransported transported-square balance, now theorem-level from the raw square-step equality.

                                                                                                                                                                                                                                                                                                                                        Checkpoint292 pre-transport square balance, now theorem-level from the smaller inner balance before the outer σ⁻¹ transport.

                                                                                                                                                                                                                                                                                                                                        Checkpoint291 pre-transport square balance, now theorem-level from the raw σ⁻¹/x₁ transported-deviation pointwise equation.

                                                                                                                                                                                                                                                                                                                                        Former checkpoint290 pre-transport operator balance, now theorem-level from the pointwise transported-square balance.

                                                                                                                                                                                                                                                                                                                                        Checkpoint289 transported-square residual, now theorem-level from the lower pre-transport balance.

                                                                                                                                                                                                                                                                                                                                        Checkpoint288 transported-square operator balance, now theorem-level from the checkpoint289 factored right-transport balance. The proof uses only add_mul, not a broad simplification pass over the transported-square context.

                                                                                                                                                                                                                                                                                                                                        Checkpoint286 transported-square residual, now theorem-level from the checkpoint287 operator-balance statement above.

                                                                                                                                                                                                                                                                                                                                        The proof is performance-safe: it applies the operator equality to the single point m and rewrites only the three visible deviation terms (X - 1) _; it deliberately avoids any global simplification of the transported square.

                                                                                                                                                                                                                                                                                                                                        Checkpoint283 transported-square residual, now theorem-level from the checkpoint285 concrete tower-action balance.

                                                                                                                                                                                                                                                                                                                                        Checkpoint282 lower atom for x₁^σ, now theorem-level from the checkpoint283 raw-deviation transported-square balance.

                                                                                                                                                                                                                                                                                                                                        Checkpoint281 lower atom for x₁^σ, now theorem-level from the checkpoint282 primitive double-application balance.

                                                                                                                                                                                                                                                                                                                                        Checkpoint280 residual for x₁^σ, now theorem-level from the checkpoint281 raw balance form.

                                                                                                                                                                                                                                                                                                                                        Checkpoint279 lower atom for x₁^σ, now theorem-level from the checkpoint280 raw S⁻¹/X₁/S transported-square cancellation.

                                                                                                                                                                                                                                                                                                                                        Checkpoint278 transported-row square atom, now theorem-level from the smaller zero-cancellation form.

                                                                                                                                                                                                                                                                                                                                        Checkpoint277 transported σ⁻¹ row with the carried coordinate expanded, now theorem-level from the canonical row/carried-endomorphism square identity.

                                                                                                                                                                                                                                                                                                                                        Checkpoint276 transported σ⁻¹ row application atom, now theorem-level from the fully expanded transported-coordinate defect.

                                                                                                                                                                                                                                                                                                                                        Checkpoint275 transported-row square identity, now theorem-level from the lower application-level transport-defect coordinate equality.

                                                                                                                                                                                                                                                                                                                                        Checkpoint274 pointwise primitive transport-defect atom for x₁^σ, now theorem-level from the two smaller pointwise coordinate calculations above.

                                                                                                                                                                                                                                                                                                                                        Former checkpoint273 primitive endomorphism-level transport-defect atom for x₁^σ, now theorem-level from the pointwise primitive row above.

                                                                                                                                                                                                                                                                                                                                        Former checkpoint271 expanded transport-defect atom, now theorem-level from the primitive raw-evaluation σ⁻¹,x₁,σ transport statement.

                                                                                                                                                                                                                                                                                                                                        Former checkpoint270 transport-defect atom, now theorem-level from the expanded P(X₁-1) row statement.

                                                                                                                                                                                                                                                                                                                                        Former checkpoint269 prefix-transport atom for the x₁^σ contribution, now theorem-level from the lower transport-defect identity.

                                                                                                                                                                                                                                                                                                                                        Checkpoint332 lower primitive for c₀=[d₀,z₀]: record only the pointwise additive zero for the relative u₀⁻¹*x₀ action. The checkpoint331 primitive x₀/u₀ action-coincidence row is recovered by applying u₀ and cancelling the visible inverse pair.

                                                                                                                                                                                                                                                                                                                                        Checkpoint328 bridge for the checkpoint327 c₀ product-fix atom: the new primitive datum is the pointwise equality of the x₀ and u₀ actions. Opening u₀⁻¹*x₀ and cancelling u₀⁻¹*u₀ recovers the product fixed-point row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint327 bridge for the checkpoint326 c₀ primitive action equality: the new datum says that the product action u₀⁻¹*x₀ fixes the point. Open the product action, apply u₀, and cancel u₀*u₀⁻¹.

                                                                                                                                                                                                                                                                                                                                        Checkpoint322 bridge for c₀=[d₀,z₀]: the checkpoint321 opened-tail fixed point is recovered from the lower primitive action-coincidence row by cancelling the adjacent x₀*x₀⁻¹ action on the right.

                                                                                                                                                                                                                                                                                                                                        Checkpoint320 bridge for c₀=[d₀,z₀]: evaluate the checkpoint321 opened d₀ = u₀*x₀⁻¹ fixed-point row at the x₀-orbit point and cancel x₀⁻¹*x₀.

                                                                                                                                                                                                                                                                                                                                        Checkpoint318 bridge for c₀=[d₀,z₀]: the checkpoint317 action coincidence at the x₀-orbit point follows by applying u₀ to the smaller equality of the visible x₀⁻¹ and u₀⁻¹ preimages.

                                                                                                                                                                                                                                                                                                                                        Checkpoint317 bridge for c₀=[d₀,z₀]: the checkpoint316 primitive action coincidence is recovered from the same equality at the displayed x₀-orbit point, followed by cancellation of x₀⁻¹*x₀.

                                                                                                                                                                                                                                                                                                                                        Checkpoint312 d₀-fixes-opened-z₀ row, now theorem-level from the opened product-action atom above.

                                                                                                                                                                                                                                                                                                                                        Checkpoint311 c₀ prefix-swap row, recovered theorem-level from the checkpoint312 statement that the literal d₀ = u₀*x₀⁻¹ product action fixes the opened z₀ core.

                                                                                                                                                                                                                                                                                                                                        Checkpoint311 c₀ tail-insertion row, recovered theorem-level from the checkpoint312 pointwise assertion that the literal d₀ = u₀*x₀⁻¹ tail fixes the point before the opened z₀ prefix is reapplied.

                                                                                                                                                                                                                                                                                                                                        Checkpoint303 primitive datum for c₀=[d₀,z₀], now theorem-level from the checkpoint304 pre-cancelled u₀⁻¹ transport row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint302 primitive datum for c₀=[d₀,z₀], now theorem-level from the checkpoint303 pointwise split of the two visible d₀ actions.

                                                                                                                                                                                                                                                                                                                                        Checkpoint300 primitive datum for c₀=[d₀,z₀], now theorem-level from the checkpoint301 no-let inverse-transported row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint299 primitive datum for c₀=[d₀,z₀], now theorem-level from the checkpoint300 inverse-transported fully inlined row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint296 d₀/z₀ nested-action zero-difference atom, now theorem-level from the fully inlined d₀ = ω₂(x₀τ)x₀⁻¹ and z₀ = σ₂⁻¹x₀σ₂ pointwise row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint295 nested d₀/z₀ action balance, now theorem-level from the zero-difference pointwise balance above.

                                                                                                                                                                                                                                                                                                                                        Checkpoint294 product-action balance for c₀, now theorem-level from the nested pointwise commutation of the two visible actions.

                                                                                                                                                                                                                                                                                                                                        Checkpoint293 pointwise commutation of the visible d₀ and z₀ actions, now theorem-level from the raw equality of the two product actions.

                                                                                                                                                                                                                                                                                                                                        Checkpoint292 raw commutator action for c₀, now theorem-level from the smaller pointwise commutation of the two visible actions.

                                                                                                                                                                                                                                                                                                                                        theorem Q2Presentation.Induction.sec7_frattiniTrivial_elementaryMStageCandidateWildRowManuscriptC0CommutatorCanonicalPrimitiveTowerActionD0Z0CommutatorTrivialApplyPointwiseData {p : FramedPair} {h : ¬ScalarTerminal p} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} {hR : Nat.card ↥(kernelFrattini K) = 1} {child : Sec7FrattiniTrivialElementaryChildData p} (src : Sec7FrattiniTrivialElementaryMStageCandidateLowerSourceData h chief K hR child) (m : towerM K) :
                                                                                                                                                                                                                                                                                                                                        have sigma2 := powOmega2 src.sigma; have d0 := powOmega2 (src.x₀ * src.tau) * src.x₀⁻¹; have z0 := sigma2⁻¹ * src.x₀ * sigma2; have A := ↑((towerActM K) d0); have B := ↑((towerActM K) z0); have Ai := ↑((towerActM K) d0⁻¹); have Bi := ↑((towerActM K) z0⁻¹); (Ai * Bi * A * B) m = m

                                                                                                                                                                                                                                                                                                                                        Checkpoint291 c₀ commutator-action pointwise row, now theorem-level from the raw fourfold towerActM commutator application.

                                                                                                                                                                                                                                                                                                                                        Former checkpoint290 c₀ commutator-action operator statement, now theorem-level from the pointwise fixed-vector statement.

                                                                                                                                                                                                                                                                                                                                        Checkpoint289 residual for c₀=[d₀,z₀], now theorem-level from the lower commutator-action-trivial atom.

                                                                                                                                                                                                                                                                                                                                        Checkpoint288 c₀ deviation-commutation residual, now theorem-level from the narrower checkpoint289 action-commutation residual.

                                                                                                                                                                                                                                                                                                                                        Checkpoint286 c₀=[d₀,z₀] raw-subtraction residual, now theorem-level from the checkpoint287 operator-commutation statement above.

                                                                                                                                                                                                                                                                                                                                        The proof applies the operator commutation to m and uses the local deviation helper sec7_end_dev_comp_apply twice, avoiding the broad noncommutative simplification that caused the checkpoint287 bridge attempt to time out.

                                                                                                                                                                                                                                                                                                                                        Checkpoint284 c₀ raw-subtraction residual, now theorem-level from the checkpoint285 concrete tower-action subtraction balance.

                                                                                                                                                                                                                                                                                                                                        Checkpoint282 lower atom for c₀=[d₀,z₀], now theorem-level from the checkpoint283 raw-subtraction primitive deviation-commutation form.

                                                                                                                                                                                                                                                                                                                                        Checkpoint281 lower atom for c₀=[d₀,z₀], now theorem-level from the checkpoint282 expanded pointwise deviation-commutation form.

                                                                                                                                                                                                                                                                                                                                        Checkpoint279 lower atom for c₀=[d₀,z₀], now theorem-level from the checkpoint281 pointwise deviation-commutation form.

                                                                                                                                                                                                                                                                                                                                        Checkpoint278 primitive d₀/z₀ action-commutation atom, now theorem-level from the smaller primitive deviation-commutation row.

                                                                                                                                                                                                                                                                                                                                        Checkpoint277 expanded primitive d₀/z₀ action commutation, now theorem-level from the canonical product-form commutation atom.

                                                                                                                                                                                                                                                                                                                                        Checkpoint276 primitive d₀/z₀ action-commutation application atom, now theorem-level from the fully expanded d₀ and z₀ lower-quotient actions.

                                                                                                                                                                                                                                                                                                                                        Checkpoint275 primitive d₀/z₀ action-commutation row, now theorem-level from the lower application-level commutation coordinate equality.

                                                                                                                                                                                                                                                                                                                                        Checkpoint274 pointwise primitive deviation-commutation atom for c₀, now theorem-level from the smaller primitive action-commutation coordinate datum.

                                                                                                                                                                                                                                                                                                                                        Former checkpoint273 primitive endomorphism-level commutator atom for c₀, now theorem-level from the pointwise primitive deviation-commutation row above.

                                                                                                                                                                                                                                                                                                                                        Smaller manuscript leaf for u₁⁻¹: the inverse ω₂-norm row is the sum of its two canonical τ and x₁ pieces.

                                                                                                                                                                                                                                                                                                                                        This is now supplied by the lower checkpoint270 two-piece ω₂-norm datum, rather than being reconstructed from the checkpoint269 x₁-only specialization.

                                                                                                                                                                                                                                                                                                                                        Smaller manuscript leaf for x₁^σ: the three canonical conjugation rows collapse to the S⁻¹-twisted x₁ row.

                                                                                                                                                                                                                                                                                                                                        The former checkpoint266 atom is now theorem-level from the three-factor product rule and the explicit action-product collapse atom.

                                                                                                                                                                                                                                                                                                                                        Smaller manuscript leaf for c₀=[d₀,z₀]: the four canonical commutator rows cancel.

                                                                                                                                                                                                                                                                                                                                        The former checkpoint266 atom is now theorem-level: the row sum is identified with the external-prefix commutator product rule, and the remaining datum is the explicit four-action product identity for d₀⁻¹ z₀⁻¹ d₀ z₀.

                                                                                                                                                                                                                                                                                                                                        Former cancelled canonical-row input, now theorem-level from the strictly lower canonical product-rule atom and the four theorem-level manuscript term carriers.

                                                                                                                                                                                                                                                                                                                                        The proof uses only:

                                                                                                                                                                                                                                                                                                                                        • the canonical factor-term shadows (h₀=0, u₁⁻¹=P(T-1)+P(X₁-1), x₁^σ=S⁻¹(X₁-1), c₀=0);
                                                                                                                                                                                                                                                                                                                                        • the new non-circular product-rule atom above; and
                                                                                                                                                                                                                                                                                                                                        • the source datum's actual wild-relator equality to cancel ρ(wildRelator)-1.

                                                                                                                                                                                                                                                                                                                                        It does not call sec7_frattiniTrivial_elementaryMStageCandidateRelatorShadowData or any theorem downstream of the canonical manuscript-row chain.

                                                                                                                                                                                                                                                                                                                                        Former fundamental wild-row input, now theorem-level from the collapsed Fox expansion of the actual manuscript relator plus the lower wild-relator equality.

                                                                                                                                                                                                                                                                                                                                        Former finite-word factor-table leaf, now theorem-level from five smaller manuscript facts: the four factor rows in the order h₀, u₁⁻¹, x₁^σ, c₀, and the raw Fox product-rule sum for the actual wild relator.

                                                                                                                                                                                                                                                                                                                                        Former Route247 literal row, now theorem-level from the lower manuscript factor-table ledger. The proof only substitutes the four factor shadows into the raw Fox product rule, preserving the manuscript order h₀, u₁⁻¹, x₁^σ, c₀.

                                                                                                                                                                                                                                                                                                                                        Former Route245 product-rule/Fox core, now theorem-level from the literal lem:h0shadow / lem:fullwordledger row.

                                                                                                                                                                                                                                                                                                                                        The proof performs no word expansion: it rewrites the four selected factor records by their shadow fields and then applies the literal full-word ledger above.

                                                                                                                                                                                                                                                                                                                                        Raw four-factor Fox sum for the candidate wild relator. The four terms correspond respectively to h₀, u₁⁻¹, x₁^σ, and c₀=[d₀,z₀] in Q2Word.wildRelator.

                                                                                                                                                                                                                                                                                                                                        The factor-evaluation shadows are now fields of the raw packet, so the former aggregate factor-evaluation axiom becomes theorem-level by projection.

                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                          Evaluation of the four raw wild-row factor terms from lem:h0shadow and lem:fullwordledger. This contains no relator-triviality assertion; it only identifies what each factor contributes to the row of d¹ ∘ d⁰.

                                                                                                                                                                                                                                                                                                                                          • h0_shadow : raw.h0Term = 0

                                                                                                                                                                                                                                                                                                                                            h₀ has the first-order shadow of x₀², hence zero in characteristic two.

                                                                                                                                                                                                                                                                                                                                          • u1_inv_shadow : raw.u1InvTerm = src.P * (src.T - 1) + src.P * (src.X₁ - 1)

                                                                                                                                                                                                                                                                                                                                            The u₁⁻¹ term contributes the two norm pieces.

                                                                                                                                                                                                                                                                                                                                          • x1_conj_shadow : raw.x1ConjTerm = src.Sinv * (src.X₁ - 1)

                                                                                                                                                                                                                                                                                                                                            The conjugate x₁^σ term contributes S⁻¹ on the x₁ coordinate.

                                                                                                                                                                                                                                                                                                                                          • c0_shadow : raw.c0Term = 0

                                                                                                                                                                                                                                                                                                                                            The commutator c₀=[d₀,z₀] has no first-order contribution.

                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                            Former Route244 raw four-factor candidate wild-row ledger, now theorem-level from the smaller formal product-rule atom plus the four explicit factor-shadow packets.

                                                                                                                                                                                                                                                                                                                                            The new residual records only the Fox product-rule sum for selected factor terms. The h₀, u₁⁻¹, x₁^σ, and c₀ evaluations are supplied here by the literal factor structures, so the old raw ledger is no longer an axiom.

                                                                                                                                                                                                                                                                                                                                            The literal evaluated four-factor wild-row ledger, before the final additive normalization.

                                                                                                                                                                                                                                                                                                                                            The four summands are the already-evaluated contributions of h₀, u₁⁻¹, x₁^σ, and c₀ in Q2Word.wildRelator. The following theorem normalizes this statement to the old additive row, so the old Route242 additive-ledger atom no longer appears directly.

                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                              Former Route243 literal factor-ordered candidate wild-row ledger, now theorem-level from the raw four-factor ledger. The proof performs only factor-shadow rewriting, preserving the manuscript order h₀, u₁⁻¹, x₁^σ, c₀ before the later additive normalization.

                                                                                                                                                                                                                                                                                                                                              The literal additive wild-row identity after the four factor shadows have been evaluated.

                                                                                                                                                                                                                                                                                                                                              This Route242 atom is smaller than the old product-rule packet: it no longer quantifies over arbitrary factor records. It is the manuscript row identity from the wild relator (lem:h0shadow / lem:fullwordledger) with the four contributions already written in the concrete endomorphism algebra of M = towerM K.

                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                Former Route242 additive-ledger residual, now theorem-level from the literal factor ledger by additive normalization in the endomorphism group.

                                                                                                                                                                                                                                                                                                                                                Former Route239 wild-row fundamental atom, now theorem-level. The proof combines the raw four-factor Fox sum with the factor evaluations; only additive regrouping and left-distributivity of composition over addition remain to be checked in Lean.

                                                                                                                                                                                                                                                                                                                                                Former source-specific lower candidate marking atom, now theorem-level.

                                                                                                                                                                                                                                                                                                                                                Given an admissible marking of towerC K, the candidate finite-quotient semantics constructs the epimorphism Γ_A ↠ towerC K; the fields recording the four generator values and the two candidate relators are then just the corresponding components of admissibility.

                                                                                                                                                                                                                                                                                                                                                Former source-specific finite-word shadow atom, now theorem-level.

                                                                                                                                                                                                                                                                                                                                                The new residual supplies the wild Fox identity with the norm term still present. The norm term vanishes by the already-proved telescoping identity src.norm_shadow, so the old final shadow follows by a two-line linear calculation.

                                                                                                                                                                                                                                                                                                                                                Former candidate-side word-operator constructor, now theorem-level.

                                                                                                                                                                                                                                                                                                                                                The operators are assembled from the source-specific lower marking and the concrete towerActM K action. The inverse, tame, and norm shadows are proved from general representation lemmas; the wild shadow is supplied only as the specialized finite-word ledger from the lower candidate relator.

                                                                                                                                                                                                                                                                                                                                                Full-row-rank form of the candidate Fox--Jacobian input.

                                                                                                                                                                                                                                                                                                                                                This is the candidate deformation-duality consequence actually used to obtain dim Z¹ = 2 dim M: the evaluated two-relator map d¹ : M⁴ → M² is onto. The rank-nullity conversion to the old finrank packet is theorem-level below.

                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                  Range-top form of the candidate Fox--Jacobian full-row-rank input.

                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                    Right-inverse form of the candidate Fox--Jacobian full-row-rank input.

                                                                                                                                                                                                                                                                                                                                                    This is a more constructive deformation-duality datum than range = ⊤: it records a linear section of the evaluated two-relator Jacobian d¹ : M⁴ → M². The range-top statement is recovered theorem-level by applying the section to an arbitrary target vector.

                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                      Coordinate-section form of the candidate Fox--Jacobian full-row-rank input.

                                                                                                                                                                                                                                                                                                                                                      This splits the right inverse into two manuscript row sections: one lifting the tame-row coordinate (m,0) and one lifting the wild-row coordinate (0,m). The single right inverse to d¹ is assembled theorem-level by adding these two lifts.

                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                        Tame-coordinate section of the evaluated candidate Fox--Jacobian.

                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                          Wild-coordinate section of the evaluated candidate Fox--Jacobian.

                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                            Carrier map for the tame-coordinate section of the candidate Fox--Jacobian.

                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                              Specification for a chosen tame-coordinate section of the candidate Fox--Jacobian.

                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                Carrier map for the wild-coordinate section of the candidate Fox--Jacobian.

                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                  Specification for a chosen wild-coordinate section of the candidate Fox--Jacobian.

                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                    New strictly weaker candidate Fox--Jacobian residual: full-row surjectivity.

                                                                                                                                                                                                                                                                                                                                                                    This is the manuscript-shaped deformation-duality fact needed by the M-stage cardinality calculation. It does not choose coordinate section maps. The old coordinate map/spec APIs below are reconstructed theorem-level from this single surjectivity statement using projectivity of vector spaces over ZMod 2.

                                                                                                                                                                                                                                                                                                                                                                    Former candidate deformation-duality range-top atom, now theorem-level from the weaker full-row-surjectivity residual.

                                                                                                                                                                                                                                                                                                                                                                    Former candidate Z¹ finrank residual, now theorem-level from full row rank of d¹ : M⁴ → M² and rank-nullity.

                                                                                                                                                                                                                                                                                                                                                                    The literal candidate cocycle subgroup is finite because it is a submodule of (towerM K)^4, and towerM K is already a finite Section 7 module.

                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                      Former candidate cocycle-group constructor, now theorem-level. The old group packet is assembled from the lower word-operator datum; no cardinality data is used here.

                                                                                                                                                                                                                                                                                                                                                                      Finite 𝔽₂-vector spaces have cardinality 2^(finrank), specialised to the candidate word-complex cocycle subgroup.

                                                                                                                                                                                                                                                                                                                                                                      Former candidate cocycle-cardinality constructor, now theorem-level. The old cardinality packet is assembled from the lower finrank formula and the standard finite-vector-space cardinality identity over 𝔽₂.

                                                                                                                                                                                                                                                                                                                                                                      Local coefficient representation atom before choosing the cocycle group finiteness proof.

                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                        Finiteness of the literal local continuous Z¹ group for the selected local module.

                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                          Lower local source-interface datum for the elementary M-stage coefficient module.

                                                                                                                                                                                                                                                                                                                                                                          The old coefficient-representation residual directly supplied a local finite-discrete representation A, an abstract linear equivalence A.V ≃ towerM K, and equivariance of that equivalence. The manuscript input is narrower: the local action on the elementary module factors through the finite lower quotient C = Y/K and matches the already-built concrete tower action. Once this locally constant quotient map is supplied, the representation itself is constructed theorem-level below with underlying space exactly towerM K and the identity coefficient equivalence.

                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                            Former local coefficient-representation residual, now theorem-level from the narrower local source quotient.

                                                                                                                                                                                                                                                                                                                                                                            The constructed representation has underlying vector space towerM K, action g ↦ towerActM K (source g), and identity coefficient equivalence. Thus the remaining semantic content is only the existence of the smooth surjective quotient map from G_{ℚ₂} to the lower finite quotient carrying the prescribed tower action.

                                                                                                                                                                                                                                                                                                                                                                            The continuous local Z¹ group is finite once the local Tate/Euler package is available. This is the finiteness part of the same local-cohomology argument proved in Local.q2_local_Z1_dim, exposed here so the Section 7 elementary stage no longer needs a separate non-local finiteness atom.

                                                                                                                                                                                                                                                                                                                                                                            The finite type structure on the local continuous Z¹ group, derived from the finite-dimensional 𝔽₂-vector-space structure.

                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                              Former local cocycle-group finiteness input, now theorem-level from the local Tate/Euler finiteness package already present in Local.Cohomology.

                                                                                                                                                                                                                                                                                                                                                                              Former local cocycle-group residual, now theorem-level from the coefficient representation and the separate continuous-cocycle finiteness atom.

                                                                                                                                                                                                                                                                                                                                                                              Local Tate/Euler formula split from the coefficient-dimension identification.

                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                Lower local Tate/Euler cardinality residual.

                                                                                                                                                                                                                                                                                                                                                                                The coefficient-dimension part of the previous residual is not mathematical content: the local coefficient packet already carries a linear equivalence loc.A.V ≃ₗ towerM K, and sec7MStageDim K is definitionally the finrank of towerM K. This packet is now assembled theorem-level from Local.q2_local_Z1_dim plus the narrower invariant-vanishing residual below.

                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                  Narrow residual replacing the former local Euler-cardinality axiom.

                                                                                                                                                                                                                                                                                                                                                                                  Local.q2_local_Z1_dim gives dim Z¹(A) = 2 * dim A + dim H⁰(A∨). The only remaining semantic input needed for the elementary M-stage exponent is that the selected local dual coefficient module has no invariants. This is the manuscript's invariant-vanishing content for the local source interface (prop:localduality, eq:localobdual, cor:sourceinterface) and is strictly narrower than asking directly for the final cardinality formula.

                                                                                                                                                                                                                                                                                                                                                                                  • dual_Hcont0_finrank : Module.finrank (ZMod 2) ↥loc.A.dual.Hcont0 = 0

                                                                                                                                                                                                                                                                                                                                                                                    The local dual invariant subspace (A∨)^{G_{ℚ₂}} = H⁰(A∨) has dimension zero.

                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                    Local dual-invariant vanishing for the selected elementary M-stage local coefficient representation.

                                                                                                                                                                                                                                                                                                                                                                                    Checkpoint368 removes the former theorem-level axiom here. The proof transports a local invariant functional on A∨ along loc.module_equiv to a towerActM-invariant functional on the concrete module towerM K; towerDualInv_zero then kills it. The only semantic input needed is now part of the local coefficient/source-interface packet: the local action factors onto towerC K and is equivariant with the concrete tower action.

                                                                                                                                                                                                                                                                                                                                                                                    Finite 𝔽₂-vector spaces have cardinality 2^(finrank), specialised to the local continuous cocycle subgroup.

                                                                                                                                                                                                                                                                                                                                                                                    Local Tate/Euler cardinality, now theorem-level from the local cocycle-dimension formula and dual-invariant vanishing.

                                                                                                                                                                                                                                                                                                                                                                                    Former local Tate/Euler residual, now theorem-level from the lower cardinality-only residual plus the existing coefficient linear equivalence.

                                                                                                                                                                                                                                                                                                                                                                                    Former local cocycle-cardinality residual, now theorem-level from local Tate/Euler and the coefficient-dimension identification with M = towerM K.

                                                                                                                                                                                                                                                                                                                                                                                    Former common M-stage cocycle-multiplicity residual, now theorem-level. The old packet is assembled from four sourcewise atoms: candidate constructor, candidate cardinality, local constructor, and local cardinality. This removes the common candidate/local cocycle multiplicity packet as an axiom and exposes the two source interfaces separately, both for the literal module M = towerM K.

                                                                                                                                                                                                                                                                                                                                                                                    Former M-stage multiplicity residual, now theorem-level from the literal cocycle multiplicity packet. The old interface is recovered with dimM = dim_{𝔽₂}(towerM K) and liftMultiplicity = |Z¹_{Γ_A,ρ}(M)|; the local group has the same cardinality by the same lower packet.

                                                                                                                                                                                                                                                                                                                                                                                    The canonical elementary M-stage multiplicity datum: dimM is literally the concrete module dimension sec7MStageDim K, and the lift multiplicity is literally 2 ^ (2 * sec7MStageDim K). Using this definitional packet (instead of an opaque Nonempty-obtained one) lets the downstream count theorems discharge the dimension side condition mult.dimM = sec7MStageDim K by rfl.

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

                                                                                                                                                                                                                                                                                                                                                                                      Candidate lift-index equivalence for the elementary M-stage.

                                                                                                                                                                                                                                                                                                                                                                                      Instead of only asserting equality of cardinalities, this records the actual finite candidate lift index together with a bijection from the boundary-framed candidate surjection set counted by framedCountA. The old cardinal realization is recovered by cardinality of this equivalence.

                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                        Product/fibre form of the candidate elementary lift index: a lower-child index and a finite cocycle-fibre index whose product indexes all candidate framed lifts.

                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                          Canonical lower-index/fibre form of the candidate elementary lift index.

                                                                                                                                                                                                                                                                                                                                                                                          Compared with the checkpoint-255 fibre packet, the lower index is not an arbitrary auxiliary BaseA; it is the actual lower-child boundary-framed surjection set. Thus the only non-canonical finite index left is the elementary cocycle fibre.

                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                            Fin-fibre form of the candidate elementary lift index.

                                                                                                                                                                                                                                                                                                                                                                                            The elementary cocycle fibre is no longer an arbitrary finite type with the right cardinality; it is the canonical Fin liftMultiplicity.

                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                              def Q2Presentation.Induction.sec7SigmaConstEquivProd (α : Type u_1) (β : Type u_2) :
                                                                                                                                                                                                                                                                                                                                                                                              (_ : α) × β ≃ α × β

                                                                                                                                                                                                                                                                                                                                                                                              Convert a sigma type with constant fibre to a product. Kept local to this file to avoid depending on a particular mathlib equivalence name.

                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                Core equivalence for the candidate elementary lift index.

                                                                                                                                                                                                                                                                                                                                                                                                The finite lower-child instance in the checkpoint-257 packet is theorem-level from the general finiteness of candidate boundary-framed surjection sets. The remaining input is only the manuscript product bijection with the canonical Fin liftMultiplicity fibre.

                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                  Sigma-fibre form of the candidate elementary lift index.

                                                                                                                                                                                                                                                                                                                                                                                                  This is below the product-form checkpoint-258 atom: the elementary lifts are indexed as a canonical Fin liftMultiplicity fibre over each lower-child candidate source, matching the manuscript affine-lifting torsor description before it is flattened to a product.

                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                    Cardinality-only sigma-fibre form of the candidate elementary lift index.

                                                                                                                                                                                                                                                                                                                                                                                                    This is strictly weaker than the previous sigma-fibre equivalence residual: it records only that the candidate framed lifts at p and the canonical lower-child Fin-fibre sigma index have the same finite cardinality. The equivalence used by the existing public API is then chosen theorem-level from finite cardinality equality.

                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                      Fibrewise projection form of the candidate elementary lift index.

                                                                                                                                                                                                                                                                                                                                                                                                      This is a more local manuscript-shaped datum than the total sigma-cardinality statement: it supplies the actual projection from a candidate lift at the current target to its lower-child source, and records that each individual fibre has the common elementary lift multiplicity. The total cardinality statement is recovered below by the standard sigmaFiberEquiv decomposition, so the old cardinal residual is no longer assumed directly.

                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                        Cocycle-fibre form of the candidate elementary lift projection.

                                                                                                                                                                                                                                                                                                                                                                                                        This is a lower, manuscript-shaped replacement for the fibre-cardinality residual: instead of asserting the cardinality of every fibre directly, it identifies every fibre of the lower-child projection with the literal candidate word-complex cocycle group Z¹_{Γ_A,ρ}(M) = Lifting.Z1 Sinv T P. The separate cardinality datum below records that this common cocycle torsor has the chosen elementary lift multiplicity, and the previous fibre-cardinality packet is recovered theorem-level from these two ingredients.

                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                          Cardinality comparison for the literal candidate cocycle fibre selected by the projection/cocycle-fibre equivalence datum.

                                                                                                                                                                                                                                                                                                                                                                                                          This is separated from the fibre-equivalence datum so that the old uniform fibre-cardinality packet is rebuilt from two finer ingredients: the torsor identification of each fibre and the common cocycle-cardinality calculation.

                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                            Checkpoint350 split of the candidate projection/cocycle-fibre residual #

                                                                                                                                                                                                                                                                                                                                                                                                            The checkpoint349 residual sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionCocycleFiberEquivData packaged the whole candidate-side elementary-lift torsor in one axiom: the lower-child projection, the candidate cocycle group, and a fibre equivalence. The structures below separate the manuscript construction into its component maps and inverse laws.

                                                                                                                                                                                                                                                                                                                                                                                                            Finite target-level postcomposition map from the current framed target to the lower child.

                                                                                                                                                                                                                                                                                                                                                                                                            This is the first projection-front atom below the old raw projection packet: it contains only the finite quotient homomorphism Y → C, not a map out of Γ_A and not a boundary-framed source construction.

                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                              Surjectivity of the finite target-level postcomposition map.

                                                                                                                                                                                                                                                                                                                                                                                                              Separated from the carrier map so that the old SurjContHom projection is recovered from two strictly finite target-side facts: the homomorphism and its surjectivity.

                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                Boundary-frame compatibility of the finite target-level postcomposition map.

                                                                                                                                                                                                                                                                                                                                                                                                                This is the lower-child boundary equation at the finite target level: whenever a point of Y has the top boundary value β(b), its image in C has the inherited lower boundary value β_C(b). It is independent of the candidate source Γ_A and of any particular lift.

                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                  Raw projection map from a current candidate lift to a lower-child candidate surjection.

                                                                                                                                                                                                                                                                                                                                                                                                                  Compared with checkpoint350, this packet now carries only the finite postcomposition provenance used to build the raw map: a target homomorphism Y → C, its surjectivity, and the statement that the raw projection evaluates by postcomposition. The boundary landing condition remains in the separate ...ProjectionBoundaryLandingData packet and is recovered below from the finite postcomposition boundary datum.

                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                    Boundary landing condition for the raw lower projection.

                                                                                                                                                                                                                                                                                                                                                                                                                    This is the part of the manuscript construction saying that the projected lower map still satisfies the inherited boundary frame.

                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                      The lift multiplicity used by the elementary stage is the candidate word-complex Euler multiplicity for this cocycle fibre. Together with the already separated CandidateCocycleCardinalityData, this replaces the former direct cocycle-cardinality residual.

                                                                                                                                                                                                                                                                                                                                                                                                                      • liftMultiplicity_eq_candidate_dim : mult.liftMultiplicity = 2 ^ (2 * sec7MStageDim K)

                                                                                                                                                                                                                                                                                                                                                                                                                        The chosen elementary lift multiplicity is the candidate 2^(2 dim M) value.

                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                        The finite quotient/postcomposition homomorphism Y → C is now part of the child-data interface, where it is constructed from the literal quotient map Y → Y/K.

                                                                                                                                                                                                                                                                                                                                                                                                                        Checkpoint353 split of the candidate projection cocycle/fibre residuals #

                                                                                                                                                                                                                                                                                                                                                                                                                        The checkpoint352 frontier still treated the affine fibre/cocycle equivalence as four map/inverse-law atoms plus one multiplicity-normalization atom. The next structures split those atoms one step further:

                                                                                                                                                                                                                                                                                                                                                                                                                        Raw affine-difference coordinates for a current candidate lift over a fixed lower source. This is below the old fibre-to-cocycle map because it lands only in the ambient four-coordinate word-complex module, before imposing the d¹=0 cocycle equation.

                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                          Cocycle-membership for the raw affine-difference coordinates. This is the literal word-complex equation saying that the extracted difference lies in Lifting.Z1 cand.Sinv cand.T cand.P.

                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                            Raw inverse-lift constructor: add a literal candidate cocycle to a fixed lower-child source and obtain a current candidate lift. The proof that this lift lies over the chosen lower source is separated below.

                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                              Value-level left inverse law. Since Lifting.Z1 is a subtype of the ambient four-coordinate module, this removes the proof-irrelevant cocycle-membership component from the old left-inverse residual.

                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                Dimension normalization below the old multiplicity residual. The multiplicity packet already says liftMultiplicity = 2^(2*mult.dimM); this datum identifies that chosen stage dimension with the literal concrete Section 7 module dimension.

                                                                                                                                                                                                                                                                                                                                                                                                                                • dimM_eq_sec7 : mult.dimM = sec7MStageDim K

                                                                                                                                                                                                                                                                                                                                                                                                                                  The M-stage dimension used in the multiplicity packet is the concrete dimension of towerM K.

                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                  Checkpoint354 coordinate/value lowering of the projection cocycle-fibre atoms #

                                                                                                                                                                                                                                                                                                                                                                                                                                  The checkpoint353 residuals already separated the candidate projection fibre into raw ambient differences, cocycle membership, current-lift construction, projection landing, proof-irrelevant inverse laws, and dimension normalization. The next layer below keeps the same public theorem API but makes three of those residuals more literal:

                                                                                                                                                                                                                                                                                                                                                                                                                                  Coordinate extraction below the raw affine-difference map.

                                                                                                                                                                                                                                                                                                                                                                                                                                  This is the literal four-generator coordinate form of the candidate lift-fibre difference: for a current lift over a lower source, it records separately the additive differences in M = towerM K on σ, τ, x₀, and x₁. The previous product-valued raw difference map is recovered theorem-level by bundling these four coordinates.

                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                    Checkpoint355: coordinate-by-coordinate raw affine differences #

                                                                                                                                                                                                                                                                                                                                                                                                                                    The checkpoint354 coordinate residual is split into the four marked-generator coordinate functions. The old bundled coordinate datum is rebuilt theorem-level below.

                                                                                                                                                                                                                                                                                                                                                                                                                                    Pointwise residual below the σ raw affine-difference coordinate.

                                                                                                                                                                                                                                                                                                                                                                                                                                    Instead of assuming a whole coordinate-extraction function at once, this atom supplies the single σ coordinate for one lower source and one current lift in that projection fibre. The public coordinate-function packet is rebuilt theorem-level by choice over these pointwise coordinates.

                                                                                                                                                                                                                                                                                                                                                                                                                                    • rawSigma : towerM K

                                                                                                                                                                                                                                                                                                                                                                                                                                      The pointwise σ additive affine-difference coordinate.

                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                      Lower residual below the pointwise Sigma Frattini-quotient coordinate: a representative in the concrete kernel K before passing to K/Φ(K).

                                                                                                                                                                                                                                                                                                                                                                                                                                      • rawSigmaKernelRepresentative : ↥K.Ksub

                                                                                                                                                                                                                                                                                                                                                                                                                                        The raw kernel representative whose Frattini-quotient class is the σ affine-difference coordinate.

                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                        Pointwise residual below the τ raw affine-difference coordinate.

                                                                                                                                                                                                                                                                                                                                                                                                                                        Instead of assuming a whole coordinate-extraction function at once, this atom supplies the single τ coordinate for one lower source and one current lift in that projection fibre. The public coordinate-function packet is rebuilt theorem-level by choice over these pointwise coordinates.

                                                                                                                                                                                                                                                                                                                                                                                                                                        • rawTau : towerM K

                                                                                                                                                                                                                                                                                                                                                                                                                                          The pointwise τ additive affine-difference coordinate.

                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                          Lower residual below the pointwise Tau affine-difference coordinate: the raw multiplicative Frattini-quotient value before additivizing it as an element of towerM K.

                                                                                                                                                                                                                                                                                                                                                                                                                                          • rawTauQuotient : towerMgrp K

                                                                                                                                                                                                                                                                                                                                                                                                                                            The raw multiplicative quotient coordinate, prior to the Additive wrapper.

                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                            Lower residual below the pointwise Tau Frattini-quotient coordinate: a representative in the concrete kernel K before passing to K/Φ(K).

                                                                                                                                                                                                                                                                                                                                                                                                                                            • rawTauKernelRepresentative : ↥K.Ksub

                                                                                                                                                                                                                                                                                                                                                                                                                                              The raw kernel representative whose Frattini-quotient class is the τ affine-difference coordinate.

                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                              Pointwise residual below the x₀ raw affine-difference coordinate.

                                                                                                                                                                                                                                                                                                                                                                                                                                              Instead of assuming a whole coordinate-extraction function at once, this atom supplies the single x₀ coordinate for one lower source and one current lift in that projection fibre. The public coordinate-function packet is rebuilt theorem-level by choice over these pointwise coordinates.

                                                                                                                                                                                                                                                                                                                                                                                                                                              • rawX0 : towerM K

                                                                                                                                                                                                                                                                                                                                                                                                                                                The pointwise x₀ additive affine-difference coordinate.

                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                Lower residual below the pointwise X0 affine-difference coordinate: the raw multiplicative Frattini-quotient value before additivizing it as an element of towerM K.

                                                                                                                                                                                                                                                                                                                                                                                                                                                • rawX0Quotient : towerMgrp K

                                                                                                                                                                                                                                                                                                                                                                                                                                                  The raw multiplicative quotient coordinate, prior to the Additive wrapper.

                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                  Lower residual below the pointwise X0 Frattini-quotient coordinate: a representative in the concrete kernel K before passing to K/Φ(K).

                                                                                                                                                                                                                                                                                                                                                                                                                                                  • rawX0KernelRepresentative : ↥K.Ksub

                                                                                                                                                                                                                                                                                                                                                                                                                                                    The raw kernel representative whose Frattini-quotient class is the x₀ affine-difference coordinate.

                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                    Pointwise residual below the x₁ raw affine-difference coordinate.

                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instead of assuming a whole coordinate-extraction function at once, this atom supplies the single x₁ coordinate for one lower source and one current lift in that projection fibre. The public coordinate-function packet is rebuilt theorem-level by choice over these pointwise coordinates.

                                                                                                                                                                                                                                                                                                                                                                                                                                                    • rawX1 : towerM K

                                                                                                                                                                                                                                                                                                                                                                                                                                                      The pointwise x₁ additive affine-difference coordinate.

                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                      Lower residual below the pointwise X1 affine-difference coordinate: the raw multiplicative Frattini-quotient value before additivizing it as an element of towerM K.

                                                                                                                                                                                                                                                                                                                                                                                                                                                      • rawX1Quotient : towerMgrp K

                                                                                                                                                                                                                                                                                                                                                                                                                                                        The raw multiplicative quotient coordinate, prior to the Additive wrapper.

                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                        Lower residual below the pointwise X1 Frattini-quotient coordinate: a representative in the concrete kernel K before passing to K/Φ(K).

                                                                                                                                                                                                                                                                                                                                                                                                                                                        • rawX1KernelRepresentative : ↥K.Ksub

                                                                                                                                                                                                                                                                                                                                                                                                                                                          The raw kernel representative whose Frattini-quotient class is the x₁ affine-difference coordinate.

                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                          Literal d¹ = 0 equation below the raw affine-difference cocycle-membership proof. This states the word-complex condition directly in the ambient four-coordinate module, before it is repackaged as membership in the kernel submodule Lifting.Z1.

                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                            Pointwise residual below the tame-row half of the literal d¹ = 0 equation.

                                                                                                                                                                                                                                                                                                                                                                                                                                                            It proves the selected row of Lifting.d1 vanishes for one raw affine-difference value; the former fibrewise row-zero packet is recovered theorem-level by assembling these pointwise proofs.

                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                              Carrier for the tame-row term packet: the two tame Fox-row summands are the literal operators applied to the raw affine-difference coordinates. This carrier is closed theorem-level by choosing the displayed summands themselves; the remaining atom below is only the cancellation of those named summands.

                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                Scalar-dual row-sum residual below tame-row pair equality: every dual functional annihilates the sum of the two named tame Fox-row summands. This is the exact linear functional form of the remaining tame cancellation statement.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Source-level scalar equality below tame-row dual-sum vanishing: for one dual functional, the two displayed tame Fox-row summands have the same scalar value. This is strictly below the aggregate row-sum atom because the old statement is recovered by assembling these one-functional equalities and using characteristic two in ZMod 2.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Pointwise residual below the wild-row half of the literal d¹ = 0 equation.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                    It proves the selected row of Lifting.d1 vanishes for one raw affine-difference value; the former fibrewise row-zero packet is recovered theorem-level by assembling these pointwise proofs.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Carrier for the wild-row term packet: the two wild Fox-row summands are the literal operators applied to the raw affine-difference coordinates. This carrier is closed theorem-level by choosing the displayed summands themselves; the remaining atom below is only the cancellation of those named summands.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Underlying current candidate epimorphism below the cocycle-to-current-lift map.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                        This is only the raw candidate map Γ_A ↠ Y produced by adding a cocycle to a lower source. The boundary-framed condition is deliberately separated into the next datum.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Pointwise residual below the raw current-lift homomorphism constructor.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                          For one lower source and one candidate cocycle, this supplies the underlying continuous homomorphism Γ_A → Y. The former function-valued constructor is rebuilt theorem-level by choosing these pointwise homomorphisms.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Former current-lift epimorphism residual, now theorem-level directly from the pointwise current-target epimorphism constructor.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Checkpoint360 note: the previous proof rebuilt this packet by first forgetting the pointwise epimorphism to a raw homomorphism and then using a second residual to recover surjectivity of that raw homomorphism. That second residual is unnecessary for this public packet: the existing pointwise constructor already supplies a Profinite.SurjContHom, so the epimorphism-valued lift can be chosen directly.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Carrier below the raw generator-boundary equation: name the actual boundary value of the constructed current lift and the expected top boundary value. The carrier itself is definitional; the only residual content is the equality between these two named values.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Underlying lower-epimorphism form of the projection law.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                              This removes the proof-irrelevant boundary-frame component from the statement that a lift constructed from a cocycle lies over its chosen lower source.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Lower residual below the projection generator equation: explicitly named finite-target values for the projected lift and the chosen lower source.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Carrier below the finite postcomposition projection equation: name the current lift's generator value, its image under the finite quotient map Y → C, and the chosen lower-source value. This carrier is definitional; only equality of the last two named values remains as a residual.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Still-lower finite postcomposition atom: the quotient map applied to the named current lift value is the named lower-source value. The artificial projected value is recovered from the carrier.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Source-level finite postcomposition equality at one generator: applying the quotient map to the constructed current lift's generator value gives the chosen lower-source value. This removes the artificial current/lower carrier values.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Former finite postcomposition multiplicative-defect residual, now theorem-level from the source-level postcomposition equality.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Carrier below the Sigma coordinate equality in the left-inverse law: name the extracted coordinate and the input coordinate. The carrier is definitional; only equality of these two named towerM K values remains below.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Source-level one-functional residual below the Sigma left-inverse additive-error packet. It removes the artificial carrier values and states the scalar vanishing directly on the extracted cocycle coordinate and the input cocycle coordinate.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Carrier below the Tau coordinate equality in the left-inverse law: name the extracted coordinate and the input coordinate. The carrier is definitional; only equality of these two named towerM K values remains below.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Source-level one-functional residual below the Tau left-inverse additive-error packet. It removes the artificial carrier values and states the scalar vanishing directly on the extracted cocycle coordinate and the input cocycle coordinate.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              • source_dual_difference_zero : φ ((↑(toMap.toCocycle ρ (lift.ofCocycle ρ z))).2.1 - (↑z).2.1) = 0
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Carrier below the X0 coordinate equality in the left-inverse law: name the extracted coordinate and the input coordinate. The carrier is definitional; only equality of these two named towerM K values remains below.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Source-level one-functional residual below the X0 left-inverse additive-error packet. It removes the artificial carrier values and states the scalar vanishing directly on the extracted cocycle coordinate and the input cocycle coordinate.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  • source_dual_difference_zero : φ ((↑(toMap.toCocycle ρ (lift.ofCocycle ρ z))).2.2.1 - (↑z).2.2.1) = 0
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Carrier below the X1 coordinate equality in the left-inverse law: name the extracted coordinate and the input coordinate. The carrier is definitional; only equality of these two named towerM K values remains below.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Source-level one-functional residual below the X1 left-inverse additive-error packet. It removes the artificial carrier values and states the scalar vanishing directly on the extracted cocycle coordinate and the input cocycle coordinate.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      • source_dual_difference_zero : φ ((↑(toMap.toCocycle ρ (lift.ofCocycle ρ z))).2.2.2 - (↑z).2.2.2) = 0
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Lower residual below the right-inverse generator equation: explicitly named finite target values for the rebuilt and original current lift.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Carrier below the generator equality in the right-inverse law: name the rebuilt current-lift generator value and the original current-lift generator value. The carrier is definitional; only equality of those named values remains below.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Still-lower right-inverse generator atom: the multiplicative difference between the named rebuilt and original finite-target values is trivial.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Kernel-Frattini residual below the right-inverse generator difference-one statement. It records that the rebuilt/original generator defect lies in the Frattini kernel R; under the active elementary hypothesis Nat.card R = 1, this defect is forced to be trivial theorem-level.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Internal Frattini representative below the right-inverse generator defect. Instead of asking directly for ambient membership in kernelFrattini K = map K.subtype (Φ K), this records an explicit element of the abstract kernel Frattini subgroup whose image is the rebuilt/original defect.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Lower residual: produce an internal Frattini representative for the right-inverse generator defect.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Former ambient kernelFrattini membership residual, now theorem-level from an internal Φ(K) representative.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Former right-inverse generator difference-one residual, now theorem-level from membership of the defect in the trivial Frattini kernel R.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Former equality-only right-inverse generator atom, now theorem-level from triviality of the rebuilt/original multiplicative difference.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Former candidate lift-index realization input, now theorem-level from the separated projection map, landing proof, fibre-to-cocycle map, inverse lift map, and two inverse laws.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Former cocycle-cardinality residual, now theorem-level from the candidate cocycle cardinality formula and the canonical dimension normalization mult.dimM = sec7MStageDim K (discharged by rfl at the canonical multiplicity packet sec7MStageCanonicalMultiplicityData).

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Former fibrewise projection/cardinality residual, now theorem-level from the literal cocycle-fibre equivalence and the common candidate cocycle cardinality.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Former product-form candidate lift-index atom, now theorem-level from the sigma-fibre index and the canonical constant-fibre sigma/product equivalence.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Former canonical Fin-fibre lift-index atom, now theorem-level from the total product bijection plus general finiteness of candidate boundary-framed surjection sets.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Former candidate lower-index/fibre packet, now theorem-level from the canonical product decomposition over the actual lower-child candidate surjection set.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Former candidate lift-index equivalence residual, now theorem-level from the manuscript product decomposition: lower lift index times elementary cocycle fibre.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Product/fibre form of the local elementary lift index.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Local lower-projection/fibre-cardinality form of the elementary M-stage lift index.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    This is the local analogue of the candidate projection packet: a framed local lift at p has a lower-child shadow, and every fibre over a lower local lift has the common cardinality liftMultiplicity = |Z¹|. The product bijection used by eq:Mstage is recovered theorem-level from this fibre-cardinality statement.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Cardinality-only sigma-fibre form of the local lift index.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Sigma-fibre bijective form of the local lift index.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Local lift-index source input, lowered to a projection with constant fibre cardinal.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          The datum is stated at the canonical dimension normalization mult.dimM = sec7MStageDim K (checkpoint-F1 repair): without that side condition the statement would over-quantify over arbitrary multiplicity packets, which is the same over-strong shape as the corrected §7 kernel findings in PROGRESS.md.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Former local M-stage lift-index input, now theorem-level from the sigma-fibre projection/cardinality statement and the canonical constant-fibre sigma/product equivalence.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          G_{ℚ₂} is topologically finitely generated — a literature-shaped local input. EXACT-CITABLE: NSW (7.4.1) Theorem (2nd ed., p. 401), verbatim-verified against the electronic edition (2026-07-09 citability audit, audit/CITABILITY_AUDIT_20260708.md §D3): "Let k be a p-adic local field and let n = [k : ℚ_p]. Then the absolute Galois group G = G(k̄|k) of k is generated by n + 2 elements" — no parity restriction, so for ℚ₂ THREE topological generators suffice, strictly stronger than this bare tfg Prop. NOT load-bearing here: Jannsen–Wingberg (NSW 7.5.14) is stated for p ≠ 2 only, and Diekert (Crelle 350 (1984)) requires k(μ₄)|k unramified — false for ℚ₂ (NSW p. 417: "The structure of G_ℚ₂ is not known"); NSW 7.4.1 alone carries the axiom. The former circular reference to the manuscript's own thm:main remains struck (2026-07-08 keep audit). Recorded in the same spirit as labute_GQ2_maxPro2_marked; consumed only to give finiteness of local boundary-framed surjection sets, replacing the former (over-strong) local fibre-cardinality route.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Every local boundary-framed surjection set is finite, from topological finite generation of G_{ℚ₂} (mirror of centralCover_candidateBoundaryFramedSurj_finite).

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Former M-stage source-index residual, now theorem-level. The paired source-index packet is assembled from independent candidate and local lift-index realization atoms.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Additive exact-image partition form of the candidate eq:Mstage formula.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          This is the manuscript subtraction before solving for the final difference: candidate lifts over the lower quotient split into the desired exact-image lifts plus the proper exact-image contributions. The old Nat.sub formula is recovered below by arithmetic.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Finite disjoint-union form of the candidate exact-image partition. The left side is the desired exact-image index plus proper-image indices; the right side is the lower-child index times the elementary lift fibre.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Canonical lower-child form of the candidate exact-image partition.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              The right-hand lower index is no longer an arbitrary finite type LowerA; it is the actual lower-child candidate boundary-framed surjection set. The remaining arbitrary finite index ProperA represents the disjoint union of proper exact-image children.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Fin-indexed form of the candidate exact-image partition.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                The proper-image summand is no longer an arbitrary finite type with the right cardinality; it is the canonical finite set Fin (Σ proper child counts). The lower-child summand is still the actual lower-child candidate boundary-framed surjection set.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Lower-child cardinality half of the canonical candidate exact-image partition.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    For any lower child, the finite cardinal of the candidate boundary-framed source set is the natural cardinal attached to framedCountA.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Former lower-child cardinality input for the candidate exact-image partition, now closed from the definition of framedCountA and the existing finiteness theorem for candidate boundary-framed source sets.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Sigma-fibre form of the canonical candidate exact-image partition.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    The right side keeps the canonical elementary lift fibre visible before flattening it to the product Fin liftMultiplicity × lowerChildSource.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Cardinality form of the canonical candidate exact-image partition.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      This is strictly weaker than choosing the partition equivalence: it records only that the finite disjoint-union index and the canonical constant sigma-fibre index have the same cardinality. The equivalence is recovered theorem-level below using finite-cardinality choice, as in the existing exact-image lift-partition cardinality interface.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Former canonical candidate exact-image partition atom, now theorem-level from the separate lower-cardinality identity, the partition bijection, and general finiteness of candidate boundary-framed surjection sets.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Finite disjoint-union form of the local exact-image partition.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Lower-child cardinality half of the local exact-image partition.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          This is the local analogue of the candidate lower-cardinality theorem, but it is kept as a semantic residual because the final local source side does not currently expose a general finiteness theorem for all boundaryFramedSurj boundaryPackage_GQ2 sets.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Sigma-fibre cardinality form of the local exact-image partition.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            The proper-image summand is the canonical finite set whose cardinality is the sum of the proper-child local counts; the lower-child summand is the actual local lower-child boundary-framed surjection set.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Product-form canonical local exact-image partition over the actual lower-child local source set.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Local lower-child finite/cardinality input for the elementary exact-image partition.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                The local projection/fibre packet already contains the only nontrivial finiteness input needed here: finiteness of the lower local boundary-framed source set. Once that Fintype instance is available, the cardinality equality is just the definition framedCountQ q = #boundaryFramedSurj boundaryPackage_GQ2 q.1 q.2 followed by Cardinal.mk_toNat_eq_card.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Fused eq:Mstage partition packet (soundness repair #15). Existence-form over the manuscript-constructed elementary child: replaces the two former ∀-child partition axioms, which were falsifiable at junk properChildren/lowerChild instantiations (PROGRESS.md). Asserts lem:elementarystage's two count identities exactly at a manuscript child with its canonical multiplicity and realized source indexes.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Former M-stage normalized-count residual, now theorem-level. The public packet is assembled from the three manuscript mechanisms in lem:elementarystage / eq:Mstage: common lift multiplicity, source lift-index realization, and exact-image subtraction.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Split residual (R = 1, elementary stage), now assembled theorem-level from the two halves. The child-geometry half is supplied by sec7_frattiniTrivial_elementaryChildData; the remaining source-count half is the separate normalized-count residual above.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Former smaller residual, now assembled theorem-level. The previous core packet is recovered from the split elementary-stage packet by converting the vacuous zero-obstruction fibres to the full lift index.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Lowered residual (R = 1, elementary stage). The previous elementary-stage packet is now a theorem assembled from the smaller core packet. The formerly residual all-character partial identities are discharged by Subsingleton.elim on Module.Dual (ZMod 2) PUnit.

                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                The old branch statement, now proved from the lowered elementary-stage residual.