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 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 < Ymapping ontoC; - 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.
- lowerChild : FramedPair
The lower quotient child
C = Y/K. Strict decrease of the lower quotient child.
- properChildren : List FramedPair
The proper exact-image children in the elementary-stage subtraction.
- proper_small (c : FramedPair) : c ∈ self.properChildren → framedMeasure c < framedMeasure p
Strict decrease of every proper exact-image child.
Source-independent elementary partial-count recipe.
- XA : Type
Candidate-source elementary lift index.
- XQ : Type
Local-source elementary lift index.
Candidate elementary lift identity; the obstruction is identically zero and
z_R = 1.Local elementary lift identity; the obstruction is identically zero and
z_R = 1.- partialA (χ : Module.Dual (ZMod 2) PUnit.{1}) : Nat.card { x : self.XA // χ (sec7ZeroObstruction self.XA x) = 0 } = self.partialN χ (List.map (⇑Cardinal.toNat) (List.map framedCountA (self.lowerChild :: self.properChildren)))
Candidate elementary partial-count realization.
- partialQ (χ : Module.Dual (ZMod 2) PUnit.{1}) : Nat.card { x : self.XQ // χ (sec7ZeroObstruction self.XQ x) = 0 } = self.partialN χ (List.map (⇑Cardinal.toNat) (List.map framedCountQ (self.lowerChild :: self.properChildren)))
Local elementary partial-count realization.
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.
- lowerChild : FramedPair
The lower quotient child
C = Y/K. Strict decrease of the lower quotient child.
- properChildren : List FramedPair
The proper exact-image children in the elementary-stage subtraction.
- proper_small (c : FramedPair) : c ∈ self.properChildren → framedMeasure c < framedMeasure p
Strict decrease of every proper exact-image child.
Source-independent elementary partial-count recipe.
- XA : Type
Candidate-source elementary lift index.
- XQ : Type
Local-source elementary lift index.
Candidate elementary lift identity; the obstruction is identically zero and
z_R = 1.Local elementary lift identity; the obstruction is identically zero and
z_R = 1.- partialA_zero : Nat.card { x : self.XA // 0 (sec7ZeroObstruction self.XA x) = 0 } = self.partialN 0 (List.map (⇑Cardinal.toNat) (List.map framedCountA (self.lowerChild :: self.properChildren)))
Candidate elementary partial-count realization at the unique dual character.
- partialQ_zero : Nat.card { x : self.XQ // 0 (sec7ZeroObstruction self.XQ x) = 0 } = self.partialN 0 (List.map (⇑Cardinal.toNat) (List.map framedCountQ (self.lowerChild :: self.properChildren)))
Local elementary partial-count realization at the unique dual character.
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.
- lowerChild : FramedPair
The lower quotient child
C = Y/K. The finite target-level projection
Y → Cused for candidate postcomposition.- lowerPostMap_surj : Function.Surjective ⇑self.lowerPostMap
The finite target-level projection
Y → Cis onto. - lowerPostMap_boundary (y : p.fst.Y) (b : ↑Boundary.toProfinite.toTop) : p.fst.qYMap y = (ProfiniteGrp.Hom.hom p.snd.beta) b → self.lowerChild.fst.qYMap (self.lowerPostMap y) = (ProfiniteGrp.Hom.hom self.lowerChild.snd.beta) b
The finite projection carries the top boundary frame to the inherited lower frame.
Strict decrease of the lower quotient child.
- properChildren : List FramedPair
The proper exact-image children in the elementary-stage subtraction.
- proper_small (c : FramedPair) : c ∈ self.properChildren → framedMeasure c < framedMeasure p
Strict decrease of every proper exact-image child.
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 child C = Y/K as a framed pair.
Equations
Instances For
The quotient map Y -> C = Y/K.
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
- Q2Presentation.Induction.sec7ElementaryExactImageChild p J hJ = ⟨p.fst.exactImageTarget J hJ, p.fst.exactImageFrame J hJ p.snd⟩
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:
Kis killed by the decoration, so the lower child is the literal quotientC = Y/K;- the proper subtraction terms are actual subgroups
J < Ymapping ontoC; - 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 with2 |J ∩ K| ≤ |K|.
It contains no source-specific lift-count identities.
lem:decorationblockin the elementary branch: the boundary decoration killsK.The elementary layer
M = Kis nontrivial.- lower_measure_mul_Kcard : framedMeasure (sec7ElementaryLowerChild K ⋯) * Nat.card ↥K.Ksub = framedMeasure p
Lower-target cardinal identity
|L_Y| = |K| |L_C|, written in measure form. - properImages : Type
Finite index of proper exact-image subgroups in the
M-stage subtraction. - finProperImages : Fintype self.properImages
- subgroup : self.properImages → Subgroup p.fst.Y
The subgroup
J < B = Y. - subgroup_surj (i : self.properImages) : Function.Surjective ⇑(p.fst.piY.comp (self.subgroup i).subtype)
Each proper image still projects onto the fixed tame quotient
H. Manuscript condition
J < B = Y.- maps_onto_lower (i : self.properImages) : Function.Surjective ⇑((sec7ElementaryLowerMap K ⋯).comp (self.subgroup i).subtype)
Manuscript condition
J -> C = Y/Kis onto. - kernelPartCard : self.properImages → ℕ
The cardinal
|J ∩ K|in the exact sequence forJ ∩ L_Y. Properness gives
2 |J ∩ K| ≤ |K|.- child_measure_eq (i : self.properImages) : framedMeasure (sec7ElementaryExactImageChild p (self.subgroup i) ⋯) = self.kernelPartCard i * framedMeasure (sec7ElementaryLowerChild K ⋯)
Manuscript
|J ∩ L_Y| = |J ∩ K| |L_C|, written as a framed-measure identity.
Instances For
The proper exact-image children as a concrete finite list.
Equations
- D.properChildren = List.map (fun (i : D.properImages) => Q2Presentation.Induction.sec7ElementaryExactImageChild p (D.subgroup i) ⋯) Finset.univ.toList
Instances For
Strict decrease of the lower quotient child C = Y/K.
The eq:Mdescent strict-decrease estimate for every proper exact-image child.
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|.
lem:decorationblockin the elementary branch: the boundary decoration killsK.The elementary layer
M = Kis nontrivial.- lower_measure_mul_Kcard : framedMeasure (sec7ElementaryLowerChild K ⋯) * Nat.card ↥K.Ksub = framedMeasure p
Lower-target cardinal identity
|L_Y| = |K| |L_C|, written in measure form.
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|.
lem:decorationblockin the elementary branch: the boundary decoration killsK.- lower_measure_mul_Kcard : framedMeasure (sec7ElementaryLowerChild K ⋯) * Nat.card ↥K.Ksub = framedMeasure p
Lower-target cardinal identity
|L_Y| = |K| |L_C|, written in measure form.
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|.
- properImages : Type
Finite index of proper exact-image subgroups in the
M-stage subtraction. - finProperImages : Fintype self.properImages
- subgroup : self.properImages → Subgroup p.fst.Y
The subgroup
J < B = Y. - subgroup_surj (i : self.properImages) : Function.Surjective ⇑(p.fst.piY.comp (self.subgroup i).subtype)
Each proper image still projects onto the fixed tame quotient
H. Manuscript condition
J < B = Y.- maps_onto_lower (i : self.properImages) : Function.Surjective ⇑((sec7ElementaryLowerMap K ⋯).comp (self.subgroup i).subtype)
Manuscript condition
J -> C = Y/Kis onto. - kernelPartCard : self.properImages → ℕ
The cardinal
|J ∩ K|in the exact sequence forJ ∩ L_Y. Properness gives
2 |J ∩ K| ≤ |K|.- child_measure_eq (i : self.properImages) : framedMeasure (sec7ElementaryExactImageChild p (self.subgroup i) ⋯) = self.kernelPartCard i * framedMeasure (sec7ElementaryLowerChild K ⋯)
Manuscript
|J ∩ L_Y| = |J ∩ K| |L_C|, written as a framed-measure identity.
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.
- properImages : Type
Finite index of proper exact-image subgroups in the
M-stage subtraction. - finProperImages : Fintype self.properImages
- subgroup : self.properImages → Subgroup p.fst.Y
The subgroup
J < B = Y. - subgroup_surj (i : self.properImages) : Function.Surjective ⇑(p.fst.piY.comp (self.subgroup i).subtype)
Each proper image still projects onto the fixed tame quotient
H. Manuscript condition
J < B = Y.- maps_onto_lower (i : self.properImages) : Function.Surjective ⇑((sec7ElementaryLowerMap K ⋯).comp (self.subgroup i).subtype)
Manuscript condition
J -> C = Y/Kis onto.
Instances For
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|.
- kernelPartCard : family.properImages → ℕ
The cardinal
|J ∩ K|in the exact sequence forJ ∩ L_Y. Properness gives
2 |J ∩ K| ≤ |K|.- child_measure_eq (i : family.properImages) : framedMeasure (sec7ElementaryExactImageChild p (family.subgroup i) ⋯) = self.kernelPartCard i * framedMeasure (sec7ElementaryLowerChild K ⋯)
Manuscript
|J ∩ L_Y| = |J ∩ K| |L_C|, written as a framed-measure identity.
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.
- kernelPartCard : Sec7FrattiniTrivialElementaryProperExactImageSubgroups lower → ℕ
The cardinal
|J ∩ K|for the canonical exact-image subgroupJ. - kernelPart_bound (i : Sec7FrattiniTrivialElementaryProperExactImageSubgroups lower) : 2 * self.kernelPartCard i ≤ Nat.card ↥K.Ksub
Properness gives
2 |J ∩ K| ≤ |K|. - child_measure_eq (i : Sec7FrattiniTrivialElementaryProperExactImageSubgroups lower) : framedMeasure (sec7ElementaryExactImageChild p ↑i ⋯) = self.kernelPartCard i * framedMeasure (sec7ElementaryLowerChild K ⋯)
Manuscript
|J ∩ L_Y| = |J ∩ K| |L_C|, for the canonical exact-image index.
Instances For
Embed a chosen family member into the canonical exact-image subtype.
Equations
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.
lem:decorationblockin the elementary branch: the boundary decoration killsK.
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|.
- lower_measure_mul_Kcard : framedMeasure (sec7ElementaryLowerChild K ⋯) * Nat.card ↥K.Ksub = framedMeasure p
Lower-target cardinal identity
|L_Y| = |K| |L_C|, written in measure form.
Instances For
Decoration and lower marked-kernel exact sequence for the R = 1 child #
The restriction of the elementary decoration to the selected kernel K.
Equations
Instances For
Any decoration into an elementary multiplicative vector group kills Φ(K).
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
On a represented kernel element, the descended linear map recovers thetaY.
The descended decoration is invariant for the quotient conjugation action.
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.
The marked-kernel map induced by
Y → Y/K.- lowerMarkedMap_surj : Function.Surjective ⇑self.lowerMarkedMap
The induced marked-kernel map is onto
L_C. Its kernel is the selected 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
- Q2Presentation.Induction.sec7ElementaryLowerMarkedMap K hθ = { toFun := fun (y : ↥p.fst.LY) => ⟨(QuotientGroup.mk' K.Ksub) ↑y, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
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.
- kernelPart : Sec7FrattiniTrivialElementaryProperExactImageSubgroups lower → Subgroup ↥K.Ksub
The subgroup playing the role of
J ∩ Kfor a canonical exact image. - restrictedMap (i : Sec7FrattiniTrivialElementaryProperExactImageSubgroups lower) : ↥(sec7ElementaryExactImageChild p ↑i ⋯).fst.LY →* ↥(sec7ElementaryLowerChild K ⋯).fst.LY
The map
J ∩ L_Y → L_Cinduced byY → C. - restrictedMap_surj (i : Sec7FrattiniTrivialElementaryProperExactImageSubgroups lower) : Function.Surjective ⇑(self.restrictedMap i)
The restricted map is onto the lower marked kernel.
- restrictedKernelEquiv (i : Sec7FrattiniTrivialElementaryProperExactImageSubgroups lower) : ↥(self.restrictedMap i).ker ≃* ↥(self.kernelPart i)
Its kernel is the selected
J ∩ Ksubgroup. - kernelPart_bound (i : Sec7FrattiniTrivialElementaryProperExactImageSubgroups lower) : 2 * Nat.card ↥(self.kernelPart i) ≤ Nat.card ↥K.Ksub
Properness of
J < Ygives the manuscript bound2 |J ∩ K| ≤ |K|.
Instances For
Restricted exact sequences for canonical proper exact images #
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 literal kernel part J ∩ K, viewed as a subgroup of K.
Equations
- Q2Presentation.Induction.sec7ProperImageKernelPart lower i = (↑i).subgroupOf K.Ksub
Instances For
If J < Y maps onto Y/K, then J ∩ K is a proper subgroup of K.
The proper-subgroup cardinal estimate 2 |J ∩ K| ≤ |K|.
The underlying element of the proper-image marked kernel J ∩ L_Y, read in Y.
Equations
- Q2Presentation.Induction.sec7ProperImageRestrictedDomainVal x = id (fun (x : ↥(p.fst.LY.subgroupOf ↑i)) => ↑((p.fst.subgroupOfInclToLY ↑i) x)) x
Instances For
The underlying element of J ∩ L_Y really lies in L_Y.
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.
Source-independent elementary partial-count recipe.
- XA : Type
Candidate-source elementary lift index.
- XQ : Type
Local-source elementary lift index.
Candidate elementary lift identity, with the vacuous zero-obstruction fibre simplified to the full lift index.
Local elementary lift identity, with the vacuous zero-obstruction fibre simplified to the full lift index.
- partialA_zero_card : Nat.card self.XA = self.partialN 0 (List.map (⇑Cardinal.toNat) (List.map framedCountA (D.lowerChild :: D.properChildren)))
Candidate zero-character partial-count identity, normalized to the full lift index.
- partialQ_zero_card : Nat.card self.XQ = self.partialN 0 (List.map (⇑Cardinal.toNat) (List.map framedCountQ (D.lowerChild :: D.properChildren)))
Local zero-character partial-count identity, normalized to the full lift index.
Instances For
A split residual packet: child geometry plus normalized source-count data.
- child : Sec7FrattiniTrivialElementaryChildData p
The lower/proper exact-image child data.
- counts : Sec7FrattiniTrivialElementaryNormalizedCountData self.child
The normalized elementary count data for those children.
Instances For
The elementary-stage child list attached to the split child packet.
Equations
- D.children = D.lowerChild :: D.properChildren
Instances For
Strict decrease for the split child packet.
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
Assemble the old core residual from the split elementary-stage packet.
Equations
- D.toCoreData = D.counts.toCoreData
Instances For
The elementary-stage child list: the lower quotient child followed by the proper-image subtraction children.
Equations
- D.children = D.lowerChild :: D.properChildren
Instances For
Strict decrease for the assembled elementary-stage child list.
The dual of the zero obstruction space has one element.
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 elementary-stage child list attached to the core packet.
Equations
- D.children = D.lowerChild :: D.properChildren
Instances For
Strict decrease for the core elementary-stage child list.
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
Direct Fourier-branch assembly from the smaller core packet.
Equations
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
- Q2Presentation.Induction.sec7MStageFunctional zM [] = 0
- Q2Presentation.Induction.sec7MStageFunctional zM (lower :: proper) = zM * lower - proper.sum
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.
- dimM : ℕ
The dimension of the elementary layer
Mover𝔽₂. - liftMultiplicity : ℕ
The common lift multiplicity
|Z¹_{Γ,ρ}(M)| = 2^(2 dim M). The manuscript multiplicity formula.
- XA : Type
Candidate-source elementary lift index.
- XQ : Type
Local-source elementary lift index.
Candidate elementary lift identity, normalized to the full lift index.
Local elementary lift identity, normalized to the full lift index.
- partialA_mstage : Nat.card self.XA = sec7MStageFunctional self.liftMultiplicity (List.map (⇑Cardinal.toNat) (List.map framedCountA (D.lowerChild :: D.properChildren)))
Candidate
eq:Mstage: lower quotient contribution minus proper exact-image terms. - partialQ_mstage : Nat.card self.XQ = sec7MStageFunctional self.liftMultiplicity (List.map (⇑Cardinal.toNat) (List.map framedCountQ (D.lowerChild :: D.properChildren)))
Local
eq:Mstage: lower quotient contribution minus proper exact-image terms.
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
Mover𝔽₂. - liftMultiplicity : ℕ
The common lift multiplicity
|Z¹_{Γ,ρ}(M)| = 2^(2 dim M). 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.
- XQ : Type
Local-source elementary lift index.
Candidate elementary lift identity, normalized to the full lift index.
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.
- partialA_mstage : Nat.card src.XA = sec7MStageFunctional mult.liftMultiplicity (List.map (⇑Cardinal.toNat) (List.map framedCountA (D.lowerChild :: D.properChildren)))
Candidate
eq:Mstage: lower quotient contribution minus proper exact-image terms. - partialQ_mstage : Nat.card src.XQ = sec7MStageFunctional mult.liftMultiplicity (List.map (⇑Cardinal.toNat) (List.map framedCountQ (D.lowerChild :: D.properChildren)))
Local
eq:Mstage: lower quotient contribution minus proper exact-image terms.
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.
- ZA : Type
Candidate
Z¹_{Γ_A,ρ}(M)additive group. - addZA : AddCommGroup self.ZA
- ZQ : Type
Local
Z¹_{G_{ℚ₂},ρ}(M)additive group. - addZQ : AddCommGroup self.ZQ
Candidate Euler/duality cardinality formula.
Local Euler/Tate cardinality formula.
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.
- Sinv : Module.End (ZMod 2) (towerM K)
The candidate operator
ρ(σ)⁻¹onM = towerM K. - T : Module.End (ZMod 2) (towerM K)
The candidate operator
ρ(τ)onM = towerM K. - P : Module.End (ZMod 2) (towerM K)
- finZA : Fintype ↥(Lifting.Z1 self.Sinv self.T self.P)
Instances For
Candidate-side cardinality formula for the actual word-complex cocycle group.
Candidate Euler/Fox--Heisenberg cardinality formula.
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 toM = 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 finiteC = Y/Kaction 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.
Finiteness of the literal local continuous cocycle group
A.Z1.
Instances For
Local-source cardinality formula for the actual continuous local cocycle group.
Local Tate/Euler cardinality formula.
Instances For
Candidate-source elementary lift-index realization, separated from the local side.
- XA : Type
Candidate-source elementary
M-lift index. 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. 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.
- partialA_mstage : Nat.card src.XA = sec7MStageFunctional mult.liftMultiplicity (List.map (⇑Cardinal.toNat) (List.map framedCountA (D.lowerChild :: D.properChildren)))
Candidate
eq:Mstage: lower quotient contribution minus proper exact-image terms.
Instances For
Local eq:Mstage exact-image subtraction, separated from the candidate side.
- partialQ_mstage : Nat.card src.XQ = sec7MStageFunctional mult.liftMultiplicity (List.map (⇑Cardinal.toNat) (List.map framedCountQ (D.lowerChild :: D.properChildren)))
Local
eq:Mstage: lower quotient contribution minus proper exact-image terms.
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
ρ(σ)onM = towerM K. - Sinv : Module.End (ZMod 2) (towerM K)
The candidate operator
ρ(σ)⁻¹onM = towerM K. - T : Module.End (ZMod 2) (towerM K)
The candidate operator
ρ(τ)onM = towerM K. - X₀ : Module.End (ZMod 2) (towerM K)
The candidate operator
ρ(x₀)onM = towerM K. - X₁ : Module.End (ZMod 2) (towerM K)
The candidate operator
ρ(x₁)onM = towerM K. - P : Module.End (ZMod 2) (towerM K)
Sinvis the left inverse of the evaluatedσ-operator.The tame row shadow of the candidate word complex.
The norm row shadow
P·(T-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 𝔽₂.
- candidate_finrank : Module.finrank (ZMod 2) ↥(Lifting.Z1 cand.Sinv cand.T cand.P) = 2 * sec7MStageDim K
Candidate Fox--Heisenberg/Euler dimension formula.
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
- Q2Presentation.Induction.sec7MStageCandidateActionEnd K = { toFun := fun (c : Q2Presentation.Induction.towerC K) => ↑((Q2Presentation.Induction.towerActM K) c), map_one' := ⋯, map_mul' := ⋯ }
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.
- source : Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (towerC K)))
The candidate lower-source epimorphism
Γ_A ↠ C = Y/K. - sigma : towerC K
The value of the lower candidate marking on
σ. - tau : towerC K
The value of the lower candidate marking on
τ. - x₀ : towerC K
The value of the lower candidate marking on
x₀. - x₁ : towerC K
The value of the lower candidate marking on
x₁. Evaluation of the source map on the universal candidate generator
σ.Evaluation of the source map on the universal candidate generator
τ.Evaluation of the source map on the universal candidate generator
x₀.Evaluation of the source map on the universal candidate generator
x₁.The tame candidate relator in the lower quotient,
σ⁻¹ τ σ = τ².- wild_rel : (Q2Word.wildRelator.eval fun (a : Gen) => match a with | Gen.sigma => self.sigma | Gen.tau => self.tau | Gen.x0 => self.x₀ | Gen.x1 => self.x₁) = 1
The full candidate wild relator in the lower quotient.
The next structure records the finite-word/Fox calculation that turns this relator, via the evaluated action on
M, into the wild linear shadow.
Instances For
The lower marking Gen → towerC K attached to the source datum.
Equations
- src.marking Q2Presentation.Gen.sigma = src.sigma
- src.marking Q2Presentation.Gen.tau = src.tau
- src.marking Q2Presentation.Gen.x0 = src.x₀
- src.marking Q2Presentation.Gen.x1 = src.x₁
Instances For
The evaluated σ-operator on M = towerM K.
Equations
- src.S = (Q2Presentation.Induction.sec7MStageCandidateActionEnd K) src.sigma
Instances For
The evaluated σ⁻¹-operator on M = towerM K.
Equations
Instances For
The evaluated τ-operator on M = towerM K.
Equations
- src.T = (Q2Presentation.Induction.sec7MStageCandidateActionEnd K) src.tau
Instances For
The evaluated x₀-operator on M = towerM K.
Equations
- src.X₀ = (Q2Presentation.Induction.sec7MStageCandidateActionEnd K) src.x₀
Instances For
The evaluated x₁-operator on M = towerM K.
Equations
- src.X₁ = (Q2Presentation.Induction.sec7MStageCandidateActionEnd K) src.x₁
Instances For
The norm operator P = 1 + T + ⋯ of the evaluated τ-orbit.
Equations
Instances For
The inverse shadow follows from the source action, not from an arbitrary choice.
The tame shadow follows by applying the lower action to the candidate tame relator.
The norm shadow is the standard telescoping identity for the norm of τ.
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).
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 inO₂(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.
The finite lower candidate marking of
C = towerC K.The marked images generate
C.The tame candidate relator holds in
C.The wild candidate relator holds in
C.The lower image of
x₀lies inO₂(C); stored here so the later core projections do not quantify over an arbitrary unrelated presented marking.The lower image of
x₁lies inO₂(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.
The finite lower candidate marking of
C = towerC K.The candidate lower map whose generator values define
q.- surj : Function.Surjective ⇑(ProfiniteGrp.Hom.hom self.hom)
The lower candidate map has exact image all of
C = towerC K. The marking is the image of the universal candidate generators under
hom.
Instances For
The generation half of the finite lower presented marking.
The marked images generate
C.
Instances For
The tame-relator half of the finite lower presented marking.
The tame candidate relator holds in
C.
Instances For
The wild-relator half of the finite lower presented marking.
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.
The candidate lower homomorphism to
C = towerC K.- surj : Function.Surjective ⇑(ProfiniteGrp.Hom.hom self.hom)
The lower candidate map has exact image all of
C = towerC K.
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.
The decoration-kernel hypothesis used to form the lower child
C = Y/K.- f : boundaryFramedSurj boundaryPackage_GammaA (sec7ElementaryLowerTarget K ⋯) (sec7ElementaryLowerFrame K ⋯)
A candidate boundary-framed surjection to the inherited lower child.
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.
- q : Marking (sec7ElementaryLowerTarget K ⋯).Y
The finite candidate marking of the literal lower quotient
C = Y/K. - admissible : Admissible self.q
The marking satisfies the candidate finite-quotient presentation.
- boundary_gen (a : Gen) : (sec7ElementaryLowerTarget K ⋯).qYMap (self.q a) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))
The marking is compatible with the inherited boundary frame on the four universal generators.
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.
- q : Marking (sec7ElementaryLowerTarget K ⋯).Y
The finite candidate marking of the literal lower quotient
C = Y/K. The actual candidate lower-boundary homomorphism whose generator values define
q.- surj : Function.Surjective ⇑(ProfiniteGrp.Hom.hom self.hom)
The source map has exact image all of the lower quotient.
The marking is exactly the image of the universal candidate generators.
- admissible : Admissible self.q
The marking satisfies the finite candidate presentation.
- pi_boundary_gen (a : Gen) : (sec7ElementaryLowerTarget K ⋯).piY ((ProfiniteGrp.Hom.hom self.hom) (gammaGen a)) = ((ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))).1
The tame quotient coordinate of the inherited-boundary generator equation.
- theta_boundary_gen (a : Gen) : (sec7ElementaryLowerTarget K ⋯).thetaY ((ProfiniteGrp.Hom.hom self.hom) (gammaGen a)) = ((ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))).2
The elementary-decoration coordinate of the inherited-boundary generator equation.
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.
- boundary_gen (a : Gen) : (sec7ElementaryLowerTarget K ⋯).qYMap (mark.q a) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))
Compatibility with the inherited boundary frame on the four universal generators.
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.
- q : Marking (sec7ElementaryLowerTarget K ⋯).Y
The finite candidate marking of the lower quotient
C = Y/K. The actual candidate lower-boundary homomorphism whose generator values define
q.- surj : Function.Surjective ⇑(ProfiniteGrp.Hom.hom self.hom)
The source map has exact image all of the lower quotient.
The carrier marking is exactly the image of the universal candidate generators.
- pi_boundary_gen (a : Gen) : (sec7ElementaryLowerTarget K ⋯).piY ((ProfiniteGrp.Hom.hom self.hom) (gammaGen a)) = ((ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))).1
The tame quotient coordinate of the inherited-boundary generator equation.
- theta_boundary_gen (a : Gen) : (sec7ElementaryLowerTarget K ⋯).thetaY ((ProfiniteGrp.Hom.hom self.hom) (gammaGen a)) = ((ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))).2
The elementary-decoration coordinate of the inherited-boundary generator equation.
Instances For
The generation component of admissibility for the lower-boundary marking.
The marked images generate
C.
Instances For
The tame-relator component of admissibility for the lower-boundary marking.
The tame candidate relator holds in the lower quotient.
Instances For
The wild-relator component of admissibility for the lower-boundary marking.
The wild candidate relator holds in the lower quotient.
Instances For
The x₀ two-core component of admissibility for the lower-boundary marking.
The lower image of
x₀lies inO₂(C).
Instances For
The x₁ two-core component of admissibility for the lower-boundary marking.
The lower image of
x₁lies inO₂(C).
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.
The candidate lower-boundary homomorphism to the literal lower quotient.
- surj : Function.Surjective ⇑(ProfiniteGrp.Hom.hom self.hom)
The lower-boundary map has exact image all of
C = Y/K. - pi_boundary_gen (a : Gen) : (sec7ElementaryLowerTarget K ⋯).piY ((ProfiniteGrp.Hom.hom self.hom) (gammaGen a)) = ((ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))).1
The tame quotient coordinate of the inherited-boundary generator equation.
- theta_boundary_gen (a : Gen) : (sec7ElementaryLowerTarget K ⋯).thetaY ((ProfiniteGrp.Hom.hom self.hom) (gammaGen a)) = ((ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))).2
The elementary-decoration coordinate of the inherited-boundary generator equation.
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.
The candidate lower-boundary homomorphism to the literal lower quotient.
- surj : Function.Surjective ⇑(ProfiniteGrp.Hom.hom self.hom)
The lower-boundary map has exact image all of
C = Y/K. - boundary_gen (a : Gen) : (sec7ElementaryLowerTarget K ⋯).qYMap ((ProfiniteGrp.Hom.hom self.hom) (gammaGen a)) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))
Compatibility with the inherited boundary frame on the four universal generators.
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.
- q : Marking (sec7ElementaryLowerTarget K ⋯).Y
The finite candidate marking of the literal lower quotient
C = Y/K. The actual candidate lower-boundary homomorphism whose generator values define
q.- surj : Function.Surjective ⇑(ProfiniteGrp.Hom.hom self.hom)
The source map has exact image all of the lower quotient.
The carrier marking is exactly the image of the universal candidate generators.
- boundary_gen (a : Gen) : (sec7ElementaryLowerTarget K ⋯).qYMap (self.q a) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))
Compatibility with the inherited boundary frame on the four universal generators.
Instances For
The generation component of the finite lower-boundary marking.
Instances For
The tame-relator component of the finite lower-boundary marking.
Instances For
The wild-relator component of the finite lower-boundary marking.
Instances For
The x₀ ∈ O₂(C) component of the finite lower-boundary marking.
Instances For
The x₁ ∈ O₂(C) component of the finite lower-boundary marking.
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.
The candidate lower-boundary homomorphism to the literal lower quotient.
- surj : Function.Surjective ⇑(ProfiniteGrp.Hom.hom self.hom)
The lower-boundary map has exact image all of
C = Y/K. - boundary_all (γ : ↑GammaA.toProfinite.toTop) : (sec7ElementaryLowerTarget K ⋯).qYMap ((ProfiniteGrp.Hom.hom self.hom) γ) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) γ)
Full inherited-boundary equation, not merely its four generator specializations.
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.
- source : boundaryFramedSurj boundaryPackage_GammaA (sec7ElementaryLowerTarget K ⋯) (sec7ElementaryLowerFrame K ⋯)
The actual lower-child candidate boundary-framed surjection.
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.
- source : boundaryFramedSurj boundaryPackage_GammaA (sec7ElementaryLowerTarget K ⋯) (sec7ElementaryLowerFrame K ⋯)
The actual inherited lower-child boundary-framed candidate surjection.
- q : Marking (sec7ElementaryLowerTarget K ⋯).Y
The finite candidate marking of the inherited lower quotient.
The marking is the image of the universal generators under
source.- admissible : Admissible self.q
The marking satisfies the candidate finite-quotient presentation.
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.
- boundary_gen (a : Gen) : (sec7ElementaryLowerTarget K ⋯).qYMap (mark.q a) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))
Compatibility with the inherited boundary frame on the four universal generators.
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.
- source : boundaryFramedSurj boundaryPackage_GammaA (sec7ElementaryLowerTarget K ⋯) (sec7ElementaryLowerFrame K ⋯)
The actual inherited lower-child boundary-framed candidate surjection.
- q : Marking (sec7ElementaryLowerTarget K ⋯).Y
The finite candidate marking of the inherited lower quotient.
The marking is the image of the universal generators under
source.- admissible : Admissible self.q
The source epimorphism makes this marking admissible.
Instances For
Generation clause for the split finite admissible quotient.
Instances For
Tame-relator clause for the split finite admissible quotient.
Instances For
Wild-relator clause for the split finite admissible quotient.
Instances For
x₀ ∈ O₂(C) clause for the split finite admissible quotient.
Instances For
x₁ ∈ O₂(C) clause for the split finite admissible quotient.
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.
The finite candidate marking of the concrete tower quotient
C = towerC K.- admissible : Admissible self.q
The marking is admissible, so
Γ_A ↠ towerC Kis supplied byGammaA_epi_equiv_admissiblerather than by this datum. - pi_boundary_gen (a : Gen) : (sec7ElementaryLowerTarget K ⋯).piY (self.q a) = ((ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))).1
Tame-quotient coordinate of the inherited boundary equation on generators.
- theta_boundary_gen (a : Gen) : (sec7ElementaryLowerTarget K ⋯).thetaY (self.q a) = ((ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))).2
Elementary-decoration coordinate of the inherited boundary equation on generators.
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.
The finite candidate marking of the concrete tower quotient
C = towerC K.- admissible : Admissible self.q
The marking is admissible; the epimorphism from
Γ_Ais still reconstructed byGammaA_epi_equiv_admissible, not assumed here. - pi_tame_gen (a : Gen) : (sec7ElementaryLowerTarget K ⋯).piY (self.q a) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).alpha) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.tameMap) (gammaGen a))
Tame coordinate, stated directly through the tame boundary factor
α. - theta_pro2_gen (a : Gen) : (sec7ElementaryLowerTarget K ⋯).thetaY (self.q a) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.pro2Map) (gammaGen a))
Elementary-decoration coordinate, stated directly through the pro-
2boundary factorψ.
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.
The finite candidate marking of the concrete tower quotient
C = towerC K.- admissible : Admissible self.q
The marking is admissible; the epimorphism from
Γ_Ais reconstructed byGammaA_epi_equiv_admissible. - pi_tame_sigma : (sec7ElementaryLowerTarget K ⋯).piY (self.q Gen.sigma) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).alpha) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.tameMap) (gammaGen Gen.sigma))
Tame coordinate on
σ. - pi_tame_tau : (sec7ElementaryLowerTarget K ⋯).piY (self.q Gen.tau) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).alpha) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.tameMap) (gammaGen Gen.tau))
Tame coordinate on
τ. - pi_tame_x0 : (sec7ElementaryLowerTarget K ⋯).piY (self.q Gen.x0) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).alpha) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.tameMap) (gammaGen Gen.x0))
Tame coordinate on
x₀. - pi_tame_x1 : (sec7ElementaryLowerTarget K ⋯).piY (self.q Gen.x1) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).alpha) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.tameMap) (gammaGen Gen.x1))
Tame coordinate on
x₁. - theta_pro2_sigma : (sec7ElementaryLowerTarget K ⋯).thetaY (self.q Gen.sigma) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.pro2Map) (gammaGen Gen.sigma))
Pro-
2decoration coordinate onσ. - theta_pro2_tau : (sec7ElementaryLowerTarget K ⋯).thetaY (self.q Gen.tau) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.pro2Map) (gammaGen Gen.tau))
Pro-
2decoration coordinate onτ. - theta_pro2_x0 : (sec7ElementaryLowerTarget K ⋯).thetaY (self.q Gen.x0) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.pro2Map) (gammaGen Gen.x0))
Pro-
2decoration coordinate onx₀. - theta_pro2_x1 : (sec7ElementaryLowerTarget K ⋯).thetaY (self.q Gen.x1) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.pro2Map) (gammaGen Gen.x1))
Pro-
2decoration coordinate onx₁.
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.
The finite candidate marking of the concrete tower quotient
C = towerC K.- admissible : Admissible self.q
The marking is admissible; the epimorphism from
Γ_Ais reconstructed byGammaA_epi_equiv_admissible. - pi_tame_sigma : (sec7ElementaryLowerTarget K ⋯).piY (self.q Gen.sigma) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).alpha) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.tameMap) (gammaGen Gen.sigma))
Tame coordinate on
σ. - pi_tame_tau : (sec7ElementaryLowerTarget K ⋯).piY (self.q Gen.tau) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).alpha) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.tameMap) (gammaGen Gen.tau))
Tame coordinate on
τ. - pi_tame_x0 : (sec7ElementaryLowerTarget K ⋯).piY (self.q Gen.x0) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).alpha) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.tameMap) (gammaGen Gen.x0))
Tame coordinate on
x₀. - pi_tame_x1 : (sec7ElementaryLowerTarget K ⋯).piY (self.q Gen.x1) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).alpha) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.tameMap) (gammaGen Gen.x1))
Tame coordinate on
x₁. - theta_pro2_sigma : (sec7ElementaryLowerTarget K ⋯).thetaY (self.q Gen.sigma) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.pro2Map) (gammaGen Gen.sigma))
Pro-
2decoration coordinate onσ. - theta_pro2_x0 : (sec7ElementaryLowerTarget K ⋯).thetaY (self.q Gen.x0) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.pro2Map) (gammaGen Gen.x0))
Pro-
2decoration coordinate onx₀. - theta_pro2_x1 : (sec7ElementaryLowerTarget K ⋯).thetaY (self.q Gen.x1) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.pro2Map) (gammaGen Gen.x1))
Pro-
2decoration coordinate onx₁.
Instances For
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.
The finite candidate marking of the concrete tower quotient
C = towerC K.- admissible : Admissible self.q
The marking is admissible; the epimorphism from
Γ_Ais reconstructed byGammaA_epi_equiv_admissible. - pi_tame_sigma : (sec7ElementaryLowerTarget K ⋯).piY (self.q Gen.sigma) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).alpha) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.tameMap) (gammaGen Gen.sigma))
Tame coordinate on
σ. - pi_tame_tau : (sec7ElementaryLowerTarget K ⋯).piY (self.q Gen.tau) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).alpha) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.tameMap) (gammaGen Gen.tau))
Tame coordinate on
τ. Lower-kernel membership for the
x₀image.Lower-kernel membership for the
x₁image.- theta_pro2_sigma : (sec7ElementaryLowerTarget K ⋯).thetaY (self.q Gen.sigma) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.pro2Map) (gammaGen Gen.sigma))
Pro-
2decoration coordinate onσ. - theta_pro2_x0 : (sec7ElementaryLowerTarget K ⋯).thetaY (self.q Gen.x0) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.pro2Map) (gammaGen Gen.x0))
Pro-
2decoration coordinate onx₀. - theta_pro2_x1 : (sec7ElementaryLowerTarget K ⋯).thetaY (self.q Gen.x1) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.pro2Map) (gammaGen Gen.x1))
Pro-
2decoration coordinate onx₁.
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.
The finite candidate marking of the concrete tower quotient
C = towerC K.- admissible : Admissible self.q
The marking is admissible; the epimorphism from
Γ_Ais reconstructed byGammaA_epi_equiv_admissible. - pi_tame_sigma_concrete : (sec7ElementaryLowerTarget K ⋯).piY (self.q Gen.sigma) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).alpha) tameSigma
Tame coordinate on
σ, stated against the concrete tame generator. - pi_tame_tau_concrete : (sec7ElementaryLowerTarget K ⋯).piY (self.q Gen.tau) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).alpha) tameTau
Tame coordinate on
τ, stated against the concrete tame generator. Lower-kernel membership for the
x₀image.Lower-kernel membership for the
x₁image.- theta_pro2_sigma_concrete : (sec7ElementaryLowerTarget K ⋯).thetaY (self.q Gen.sigma) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) piSigma
Pro-
2decoration coordinate onσ, stated against the concrete pro-2generator. - theta_pro2_x0_concrete : (sec7ElementaryLowerTarget K ⋯).thetaY (self.q Gen.x0) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) piX0
Pro-
2decoration coordinate onx₀, stated against the concrete pro-2generator. - theta_pro2_x1_concrete : (sec7ElementaryLowerTarget K ⋯).thetaY (self.q Gen.x1) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) piX1
Pro-
2decoration coordinate onx₁, stated against the concrete pro-2generator.
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).
The finite candidate marking of the concrete tower quotient
C = towerC K.The presentation part of admissibility: generation and the two candidate relators.
- pi_tame_sigma_concrete : (sec7ElementaryLowerTarget K ⋯).piY (self.q Gen.sigma) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).alpha) tameSigma
Tame coordinate on
σ, stated against the concrete tame generator. - pi_tame_tau_concrete : (sec7ElementaryLowerTarget K ⋯).piY (self.q Gen.tau) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).alpha) tameTau
Tame coordinate on
τ, stated against the concrete tame generator. Lower-kernel membership for the
x₀image.Lower-kernel membership for the
x₁image.- theta_pro2_sigma_concrete : (sec7ElementaryLowerTarget K ⋯).thetaY (self.q Gen.sigma) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) piSigma
Pro-
2decoration coordinate onσ, stated against the concrete pro-2generator. - theta_pro2_x0_concrete : (sec7ElementaryLowerTarget K ⋯).thetaY (self.q Gen.x0) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) piX0
Pro-
2decoration coordinate onx₀, stated against the concrete pro-2generator. - theta_pro2_x1_concrete : (sec7ElementaryLowerTarget K ⋯).thetaY (self.q Gen.x1) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) piX1
Pro-
2decoration coordinate onx₁, stated against the concrete pro-2generator.
Instances For
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.
- source : Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (towerC K)))
The actual candidate source epimorphism to the concrete tower quotient
C = towerC K. - pi_tame_sigma_concrete : (sec7ElementaryLowerTarget K ⋯).piY ((ProfiniteGrp.Hom.hom self.source.hom) (gammaGen Gen.sigma)) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).alpha) tameSigma
Tame coordinate on
σ, stated against the concrete tame generator. - pi_tame_tau_concrete : (sec7ElementaryLowerTarget K ⋯).piY ((ProfiniteGrp.Hom.hom self.source.hom) (gammaGen Gen.tau)) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).alpha) tameTau
Tame coordinate on
τ, stated against the concrete tame generator. - x0_mem_lower_LY : (ProfiniteGrp.Hom.hom self.source.hom) (gammaGen Gen.x0) ∈ (sec7ElementaryLowerTarget K ⋯).LY
Lower-kernel membership for the
x₀image. - x1_mem_lower_LY : (ProfiniteGrp.Hom.hom self.source.hom) (gammaGen Gen.x1) ∈ (sec7ElementaryLowerTarget K ⋯).LY
Lower-kernel membership for the
x₁image. - theta_pro2_sigma_concrete : (sec7ElementaryLowerTarget K ⋯).thetaY ((ProfiniteGrp.Hom.hom self.source.hom) (gammaGen Gen.sigma)) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) piSigma
Pro-
2decoration coordinate onσ, stated against the concrete pro-2generator. - theta_pro2_x0_concrete : (sec7ElementaryLowerTarget K ⋯).thetaY ((ProfiniteGrp.Hom.hom self.source.hom) (gammaGen Gen.x0)) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) piX0
Pro-
2decoration coordinate onx₀, stated against the concrete pro-2generator. - theta_pro2_x1_concrete : (sec7ElementaryLowerTarget K ⋯).thetaY ((ProfiniteGrp.Hom.hom self.source.hom) (gammaGen Gen.x1)) = (ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).psi) piX1
Pro-
2decoration coordinate onx₁, stated against the concrete pro-2generator.
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.
The previous tame/pro-2 factor packet is theorem-level from the literal generator
rows.
The checkpoint-336 tower-marking packet is now theorem-level from the still lower
tame/pro-2 factor compatibility datum above.
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 finite marking-carrier primitive, now theorem-level from the actual lower-child boundary-framed candidate surjection.
Former generation primitive for the split finite admissible quotient, now recovered from
GammaA_epi_equiv_admissible applied to the carrier's actual source epimorphism.
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 x₀ ∈ O₂(C) primitive for the split finite admissible quotient, now recovered
from GammaA_epi_equiv_admissible applied to the carrier's actual source epimorphism.
Former x₁ ∈ O₂(C) 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.
Tame-quotient coordinate of inherited-boundary compatibility on the four generators.
- pi_boundary_gen (a : Gen) : (sec7ElementaryLowerTarget K ⋯).piY (mark.q a) = ((ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))).1
Instances For
Elementary-decoration coordinate of inherited-boundary compatibility on the four generators.
- theta_boundary_gen (a : Gen) : (sec7ElementaryLowerTarget K ⋯).thetaY (mark.q a) = ((ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))).2
Instances For
Former tame-quotient coordinate primitive, now obtained by projecting the full
boundary-framed equation carried by mark.source.
Former elementary-decoration coordinate primitive, now obtained by projecting the full
boundary-framed equation carried by mark.source.
Former full generator-level inherited-boundary atom, now theorem-level from the two
coordinates of the boundary map qYMap = (π_Y, θ_Y).
Former full lower-boundary map datum, now theorem-level from the canonical boundary-framed surjection subtype.
Former generator-level lower finite-frame source atom, now theorem-level from a full boundary-framed candidate epimorphism to the inherited lower quotient.
Former carrier atom for the inherited lower finite frame, now theorem-level from the source-level finite frame datum.
Former generation atom for the inherited lower finite frame, now theorem-level from
GammaA_epi_equiv_admissible applied to the carrier source map.
Former tame-relator atom for the inherited lower finite frame, now theorem-level from
GammaA_epi_equiv_admissible.
Former wild-relator atom for the inherited lower finite frame, now theorem-level from
GammaA_epi_equiv_admissible.
Former x₀ ∈ O₂(C) atom for the inherited lower finite frame, now theorem-level
from GammaA_epi_equiv_admissible.
Former x₁ ∈ O₂(C) atom for the inherited lower finite frame, now theorem-level
from GammaA_epi_equiv_admissible.
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 lower-source carrier input, now theorem-level from the actual lower-boundary source map.
Former generation input for the lower-boundary finite marking, now theorem-level from candidate finite-quotient semantics applied to the carrier source map.
Former tame-relator input for the lower-boundary finite marking, now theorem-level from candidate finite-quotient semantics.
Former wild-relator input for the lower-boundary finite marking, now theorem-level from candidate finite-quotient semantics.
Former x₀ ∈ O₂(C) input for the lower-boundary finite marking, now theorem-level
from candidate finite-quotient semantics.
Former x₁ ∈ O₂(C) input for the lower-boundary finite marking, now theorem-level
from candidate finite-quotient semantics.
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.
- pi_boundary_gen (a : Gen) : (sec7ElementaryLowerTarget K ⋯).piY (mark.q a) = ((ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))).1
Compatibility of the
Hcoordinate on the four universal generators.
Instances For
The elementary-decoration coordinate of the inherited-boundary generator equation.
- theta_boundary_gen (a : Gen) : (sec7ElementaryLowerTarget K ⋯).thetaY (mark.q a) = ((ProfiniteGrp.Hom.hom (sec7ElementaryLowerFrame K ⋯).beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))).2
Compatibility of the decoration coordinate on the four universal generators.
Instances For
Former H-coordinate boundary input for the lower source, now theorem-level from
the source map stored in the admissible-marking packet.
Former decoration-coordinate boundary input for the lower source, now theorem-level from the source map stored in the admissible-marking packet.
Former lower-boundary generator-compatibility atom, now theorem-level from the two
literal coordinates of the combined map q_Y=(π_Y,θ_Y).
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 epimorphism encoded by the lower finite marking.
Equations
- Q2Presentation.Induction.sec7CandidateLowerFiniteEpiOfMarking mark = { hom := mark.hom, surj := ⋯ }
Instances For
The finite lower marking attached to a source map is admissible, by the candidate finite-quotient semantics.
Route245 residual closed theorem-level: the finite lower marking generates
C = towerC K.
Route245 residual closed theorem-level: the tame relator holds for the finite lower marking.
Route245 residual closed theorem-level: the wild relator holds for the finite lower marking.
The x₀-core half of the finite wild-core datum.
The lower image of
x₀lies inO₂(C).
Instances For
The x₁-core half of the finite wild-core datum.
The lower image of
x₁lies inO₂(C).
Instances For
Route245 residual closed theorem-level: the lower image of x₀ lies in O₂(C).
Route245 residual closed theorem-level: the lower image of x₁ lies in O₂(C).
Former Route244 presented-marking residual, now theorem-level from four smaller finite quotient atoms: the bare marking, generation, tame relator, and wild relator.
Former Route244 finite wild-core residual, now theorem-level from the two separate
x₀ and x₁ finite O₂(C) membership atoms.
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.
The wild row shadow obtained from the candidate wild relator by the finite-word ledger (
lem:h0shadowandlem: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:h0shadowandlem: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:
- an admissible lower marking of
C = towerC K; - the finite-word/Fox wild-row fundamental identity.
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:
- existence of the lower marking is separated from generation, relators, and the
O₂(C)wild-core conditions (prop:epi-semantics/ admissible finite quotients); - the wild-row calculation is separated into a raw four-factor Fox sum and the
factor-by-factor ledger for
h₀,u₁⁻¹,x₁^σ, andc₀(lem:h0shadow,lem:fullwordledger).
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.
The candidate lower homomorphism to
C = towerC K.- surj : Function.Surjective ⇑(ProfiniteGrp.Hom.hom self.hom)
The lower candidate map has exact image
C.
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.
The underlying candidate lower homomorphism.
- surj : Function.Surjective ⇑(ProfiniteGrp.Hom.hom self.hom)
The lower candidate map has exact image
C. The four-generator lower marking
Γ_A -> Cat the finite-quotient level.The marking is the image of the universal candidate generators.
Instances For
The lower marking generates the lower quotient C. This is the generation part
of admissibility, recovered from candidate finite-quotient semantics.
The marked images of
σ,τ,x₀,x₁generateC.
Instances For
The two candidate relators on the lower marking of C.
The tame relation
τ^σ = τ².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.
The underlying candidate lower homomorphism to
C = towerC K.- surj : Function.Surjective ⇑(ProfiniteGrp.Hom.hom self.hom)
The carrier is chosen from an admissible finite marking, hence is onto
C.
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.
- surj : Function.Surjective ⇑(ProfiniteGrp.Hom.hom carrier.hom)
The carrier map has exact image all of
C = towerC K.
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.
Former Route241 residual, now theorem-level from carrier plus exact-image data.
Former Route240 residual, now theorem-level from the lower homomorphism datum.
Build the epimorphism encoded by a lower marking.
Equations
- Q2Presentation.Induction.sec7CandidateLowerEpiOfMarking mark = { hom := mark.hom, surj := ⋯ }
Instances For
The admissibility of the marking attached to an exact lower candidate image.
Former Route240 residual, now theorem-level from exact-image semantics.
Former Route240 residual, now theorem-level from exact-image semantics.
Former Route240 residual, now theorem-level from exact-image semantics.
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₀. h₀has the first-order shadow ofx₀², 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₁⁻¹. The
u₁⁻¹term contributes the two norm pieces.
Instances For
The x₁^σ factor contribution in the candidate wild-row ledger.
- term : Module.End (ZMod 2) (towerM K)
First-order contribution of
x₁^σ. The conjugate
x₁^σterm contributesS⁻¹on thex₁coordinate.
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₀]. 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.
- relator_factor_sum : Q2Word.wildRelator.eval src.marking = 1 → h0.term + u1.term + x1.term + c0.term = 0
The raw Fox fundamental sum attached to the actual lower wild relator.
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.
- literal_factor_sum : Q2Word.wildRelator.eval src.marking = 1 → 0 + (src.P * (src.T - 1) + src.P * (src.X₁ - 1)) + src.Sinv * (src.X₁ - 1) + 0 = 0
The literal factor-ordered row from
lem:fullwordledger.
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.
- h0Term : Module.End (ZMod 2) (towerM K)
First-order contribution of
h₀. - u1InvTerm : Module.End (ZMod 2) (towerM K)
First-order contribution of
u₁⁻¹. - x1ConjTerm : Module.End (ZMod 2) (towerM K)
First-order contribution of
x₁^σ. - c0Term : Module.End (ZMod 2) (towerM K)
First-order contribution of
c₀=[d₀,z₀]. - relator_factor_sum : Q2Word.wildRelator.eval src.marking = 1 → self.h0Term + self.u1InvTerm + self.x1ConjTerm + self.c0Term = 0
The raw Fox product-rule sum for the actual lower wild relator.
h₀has the first-order shadow ofx₀², hence zero in characteristic two.The
u₁⁻¹term contributes the two norm pieces.The conjugate
x₁^σterm contributesS⁻¹on thex₁coordinate.The commutator
c₀=[d₀,z₀]has no first-order contribution.
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₀. 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₁⁻¹. The inverse norm term contributes
P(T-1) + P(X₁-1).
Instances For
The x₁^σ row of the manuscript finite-word ledger.
- x1ConjTerm : Module.End (ZMod 2) (towerM K)
First-order contribution of
x₁^σ. The conjugate contributes
S⁻¹(X₁-1)on thex₁coordinate.
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₀]. 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.
- relator_factor_sum : Q2Word.wildRelator.eval src.marking = 1 → h0.h0Term + u1.u1InvTerm + x1.x1ConjTerm + c0.c0Term = 0
The raw Fox product-rule sum for the actual lower wild relator.
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₀. The chosen
h₀term has the zero shadow fromlem:h0shadow.
Instances For
The shadow half of the h₀ row (lem:h0shadow): the chosen h₀ term is zero.
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₁⁻¹. 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).
The inverse norm term contributes
P(T-1) + P(X₁-1).
Instances For
The term-carrier half of the x₁^σ row.
- x1ConjTerm : Module.End (ZMod 2) (towerM K)
First-order contribution of
x₁^σ. The conjugate contributes
S⁻¹(X₁-1)on thex₁coordinate.
Instances For
The shadow half of the x₁^σ row: conjugation by σ contributes S⁻¹.
The conjugate contributes
S⁻¹(X₁-1)on thex₁coordinate.
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₀]. The commutator factor has no first-order contribution.
Instances For
The shadow half of the commutator row: c₀ has no first-order contribution.
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.
- expansion : Q2Word.wildRelator.eval src.marking = 1 → h0.h0Term + u1.u1InvTerm + x1.x1ConjTerm + c0.c0Term = (sec7MStageCandidateActionEnd K) (Q2Word.wildRelator.eval src.marking) - 1
The Fox product-rule expansion before using the relator equality.
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.
- literal_expansion : Q2Word.wildRelator.eval src.marking = 1 → 0 + (src.P * (src.T - 1) + src.P * (src.X₁ - 1)) + src.Sinv * (src.X₁ - 1) + 0 = (sec7MStageCandidateActionEnd K) (Q2Word.wildRelator.eval src.marking) - 1
The literal Fox product-rule expansion before using the relator cancellation.
Instances For
The h₀ term carrier is now chosen directly as its manuscript zero contribution.
The h₀ shadow is theorem-level from the chosen term carrier.
The u₁⁻¹ term carrier is now the literal inverse-norm contribution from the
manuscript word ledger.
The u₁⁻¹ shadow is theorem-level from the chosen term carrier.
The x₁^σ term carrier is now the literal conjugation contribution from the
manuscript word ledger.
The x₁^σ shadow is theorem-level from the chosen term carrier.
The commutator term carrier c₀=[d₀,z₀] is now chosen as its zero first-order
contribution.
The commutator zero shadow is theorem-level from the chosen term carrier.
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.
- collapsed_expansion : Q2Word.wildRelator.eval src.marking = 1 → src.P * (src.T - 1) + (src.P + src.Sinv) * (src.X₁ - 1) = (sec7MStageCandidateActionEnd K) (Q2Word.wildRelator.eval src.marking) - 1
The collapsed Fox derivative row before the final relator cancellation.
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.
- normBlock : Module.End (ZMod 2) (towerM K)
The norm part of the collapsed Fox row.
- x1Block : Module.End (ZMod 2) (towerM K)
The remaining
x₁part of the collapsed Fox row. The norm block is the manuscript operator
P(T-1).The
x₁block is the manuscript operator(P+S⁻¹)(X₁-1).- block_expansion : Q2Word.wildRelator.eval src.marking = 1 → self.normBlock + self.x1Block = (sec7MStageCandidateActionEnd K) (Q2Word.wildRelator.eval src.marking) - 1
The block sum is the Fox derivative of the evaluated wild relator.
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₀.
- term_product_rule : Q2Word.wildRelator.eval src.marking = 1 → h0.h0Term + u1.u1InvTerm + x1.x1ConjTerm + c0.c0Term = (sec7MStageCandidateActionEnd K) (Q2Word.wildRelator.eval src.marking) - 1
The raw Fox product-rule expansion before substituting the four term shadows.
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.
- canonical_term_product_rule : Q2Word.wildRelator.eval src.marking = 1 → 0 + (src.P * (src.T - 1) + src.P * (src.X₁ - 1)) + src.Sinv * (src.X₁ - 1) + 0 = (sec7MStageCandidateActionEnd K) (Q2Word.wildRelator.eval src.marking) - 1
The raw Fox product-rule expansion for the canonical four manuscript terms.
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 actual h₀ factor of the manuscript wild word, evaluated in the lower candidate
quotient C = towerC K.
Equations
Instances For
The actual u₁⁻¹ factor of the manuscript wild word, evaluated in the lower
candidate quotient.
Equations
Instances For
The actual x₁^σ factor of the manuscript wild word, evaluated in the lower
candidate quotient.
Equations
Instances For
The actual c₀ factor of the manuscript wild word, evaluated in the lower candidate
quotient.
Equations
Instances For
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.
- h0_prefix_shadow : h0.h0Term = (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0Factor src) - 1
The
h₀term is the first prefix contribution of the product rule.
Instances For
Prefix-shadow datum for the u₁⁻¹ manuscript factor.
- u1_prefix_shadow : u1.u1InvTerm = (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0Factor src) * ((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptU1InvFactor src) - 1)
The
u₁⁻¹term is the second prefix contribution of the product rule.
Instances For
Prefix-shadow datum for the x₁^σ manuscript factor.
- x1_prefix_shadow : x1.x1ConjTerm = (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0Factor src * sec7MStageCandidateWildRowManuscriptU1InvFactor src) * ((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptX1ConjFactor src) - 1)
The
x₁^σterm is the third prefix contribution of the product rule.
Instances For
Prefix-shadow datum for the c₀ manuscript factor.
- c0_prefix_shadow : c0.c0Term = (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0Factor src * sec7MStageCandidateWildRowManuscriptU1InvFactor src * sec7MStageCandidateWildRowManuscriptX1ConjFactor src) * ((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptC0Factor src) - 1)
The
c₀term is the fourth prefix contribution of the product rule.
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.
- h0_prefix_action : (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0Factor src) = 1
The evaluated
h₀factor has trivial action onM.
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.
- u1_inv_factor_fox : (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptU1InvFactor src) - 1 = src.P * (src.T - 1) + src.P * (src.X₁ - 1)
The inverse
ω₂-norm factor contributes the two norm pieces oflem:fullwordledger.
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₀.
- x1_conj_prefix_fox : (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0Factor src * sec7MStageCandidateWildRowManuscriptU1InvFactor src) * ((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptX1ConjFactor src) - 1) = src.Sinv * (src.X₁ - 1)
The third prefix contribution is the
S⁻¹-twistedx₁row.
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.
- c0_prefix_fox : (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0Factor src * sec7MStageCandidateWildRowManuscriptU1InvFactor src * sec7MStageCandidateWildRowManuscriptX1ConjFactor src) * ((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptC0Factor src) - 1) = 0
The fourth prefix contribution, coming from the commutator factor
c₀, vanishes.
Instances For
Checkpoint264: lower the four factor/Fox atoms to internal word/Fox ledgers #
First internal factor of h₀ = x₀^{g₀} x₀ d_g d₀ d₀² h_c.
Equations
Instances For
Second internal factor of h₀.
Equations
Instances For
Third internal factor of h₀.
Equations
Instances For
Fourth internal factor of h₀.
Equations
Instances For
Fifth internal factor of h₀, namely d₀².
Equations
Instances For
Sixth internal factor of h₀.
Equations
Instances For
The internal six-factor Fox sum of h₀.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The algebraic product-rule bridge from the internal six-factor h₀ ledger to
ρ(h₀)-1.
The non-inverted u₁ factor.
Equations
Instances For
Internal first factor of x₁^σ = σ⁻¹ x₁ σ.
Equations
Instances For
Internal middle factor of x₁^σ = σ⁻¹ x₁ σ.
Equations
Instances For
Internal final factor of x₁^σ = σ⁻¹ x₁ σ.
Equations
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
Product-rule bridge from the internal conjugation ledger to the lumped third-prefix contribution.
Internal d₀ factor of c₀=[d₀,z₀].
Equations
Instances For
Internal d₀⁻¹ factor of c₀=[d₀,z₀].
Equations
Instances For
Internal z₀ factor of c₀=[d₀,z₀].
Equations
Instances For
Internal z₀⁻¹ factor of c₀=[d₀,z₀].
Equations
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
Product-rule bridge from the internal commutator ledger to the lumped fourth-prefix contribution.
Lower internal manuscript atom for h₀: the six-factor Fox sum of
x₀^{g₀} x₀ d_g d₀ d₀² h_c vanishes.
The internal
h₀Fox ledger, before collapsing it to the action equalityρ(h₀)=1.
Instances For
Lower internal manuscript atom for u₁⁻¹: the inverse rule has been separated
from the ω₂-norm Fox calculation for u₁=(x₁τ)^{ω₂}.
- u1_inv_omega_norm_fox : -((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptU1InvFactor src) * ((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptU1Factor src) - 1)) = src.P * (src.T - 1) + src.P * (src.X₁ - 1)
The
ω₂-norm Fox row for the non-invertedu₁, transported through the inverse-factor rule.
Instances For
Lower internal manuscript atom for x₁^σ: expand the conjugate
σ⁻¹ x₁ σ before collapsing it to the third-prefix row.
- x1_conj_internal_fox : sec7MStageCandidateWildRowManuscriptX1ConjInternalPrefixSum src = src.Sinv * (src.X₁ - 1)
The internal conjugation ledger is the manuscript
S⁻¹-twistedx₁row.
Instances For
Lower internal manuscript atom for c₀=[d₀,z₀]: expand the commutator before
collapsing it to a zero fourth-prefix contribution.
The internal commutator Fox ledger vanishes.
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.
- h0ConjX0G0Row : Module.End (ZMod 2) (towerM K)
The row from the factor
x₀^{g₀}. - h0X0Row : Module.End (ZMod 2) (towerM K)
The row from the factor
x₀. - h0DgRow : Module.End (ZMod 2) (towerM K)
The row from the factor
d_g. - h0D0Row : Module.End (ZMod 2) (towerM K)
The row from the factor
d₀. - h0D0SqRow : Module.End (ZMod 2) (towerM K)
The row from the factor
d₀². - h0HcRow : Module.End (ZMod 2) (towerM K)
The row from the factor
h_c. - h0_conjX0G0_row : self.h0ConjX0G0Row = (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0ConjX0G0Factor src) - 1
Fox row for
x₀^{g₀}. - h0_x0_row : self.h0X0Row = (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0ConjX0G0Factor src) * ((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0X0Factor src) - 1)
Fox row for the following
x₀, including the prefixx₀^{g₀}. - h0_dg_row : self.h0DgRow = (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0ConjX0G0Factor src * sec7MStageCandidateWildRowManuscriptH0X0Factor src) * ((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0DgFactor src) - 1)
Fox row for
d_g, including the prefixx₀^{g₀}x₀. - h0_d0_row : self.h0D0Row = (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0ConjX0G0Factor src * sec7MStageCandidateWildRowManuscriptH0X0Factor src * sec7MStageCandidateWildRowManuscriptH0DgFactor src) * ((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0D0Factor src) - 1)
Fox row for the first
d₀. - h0_d0Sq_row : self.h0D0SqRow = (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0ConjX0G0Factor src * sec7MStageCandidateWildRowManuscriptH0X0Factor src * sec7MStageCandidateWildRowManuscriptH0DgFactor src * sec7MStageCandidateWildRowManuscriptH0D0Factor src) * ((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0D0SqFactor src) - 1)
Fox row for the
d₀²factor. - h0_hc_row : self.h0HcRow = (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0ConjX0G0Factor src * sec7MStageCandidateWildRowManuscriptH0X0Factor src * sec7MStageCandidateWildRowManuscriptH0DgFactor src * sec7MStageCandidateWildRowManuscriptH0D0Factor src * sec7MStageCandidateWildRowManuscriptH0D0SqFactor src) * ((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0HcFactor src) - 1)
Fox row for the final
h_cfactor. - h0_expanded_rows_sum_zero : self.h0ConjX0G0Row + self.h0X0Row + self.h0DgRow + self.h0D0Row + self.h0D0SqRow + self.h0HcRow = 0
The six
h₀rows cancel, which is the literal first-order content oflem:h0shadowin the elementary row.
Instances For
Row-level finite-word data for the inverse ω₂-norm factor u₁⁻¹.
- u1TauRow : Module.End (ZMod 2) (towerM K)
The
τ-variation piece of theω₂-norm row. - u1X1Row : Module.End (ZMod 2) (towerM K)
The
x₁-variation piece of theω₂-norm row. The
τpiece is the manuscript operatorP(T-1).The
x₁piece is the manuscript operatorP(X₁-1).- u1_inv_omega_norm_rows : -((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptU1InvFactor src) * ((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptU1Factor src) - 1)) = self.u1TauRow + self.u1X1Row
The inverse-factor rule transports the non-inverted
ω₂-norm Fox row tou₁⁻¹.
Instances For
Row-level finite-word data for the conjugate x₁^σ=σ⁻¹x₁σ.
- x1SigmaInvRow : Module.End (ZMod 2) (towerM K)
The row from the internal factor
σ⁻¹. - x1BareRow : Module.End (ZMod 2) (towerM K)
The row from the internal factor
x₁. - x1SigmaRow : Module.End (ZMod 2) (towerM K)
The row from the internal factor
σ. - x1_sigmaInv_row : self.x1SigmaInvRow = (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0Factor src * sec7MStageCandidateWildRowManuscriptU1InvFactor src) * ((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptSigmaInvFactor src) - 1)
Fox row for the leading
σ⁻¹in the conjugate. - x1_bare_row : self.x1BareRow = (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0Factor src * sec7MStageCandidateWildRowManuscriptU1InvFactor src * sec7MStageCandidateWildRowManuscriptSigmaInvFactor src) * ((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptX1BareFactor src) - 1)
Fox row for the middle
x₁, including theh₀u₁⁻¹σ⁻¹prefix. - x1_sigma_row : self.x1SigmaRow = (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0Factor src * sec7MStageCandidateWildRowManuscriptU1InvFactor src * sec7MStageCandidateWildRowManuscriptSigmaInvFactor src * sec7MStageCandidateWildRowManuscriptX1BareFactor src) * ((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptSigmaFactor src) - 1)
Fox row for the closing
σ. The three conjugation rows collapse to the manuscript
S⁻¹-twistedx₁row.
Instances For
Row-level finite-word data for the commutator c₀=[d₀,z₀].
- c0D0InvRow : Module.End (ZMod 2) (towerM K)
The row from the factor
d₀⁻¹. - c0Z0InvRow : Module.End (ZMod 2) (towerM K)
The row from the factor
z₀⁻¹. - c0D0Row : Module.End (ZMod 2) (towerM K)
The row from the factor
d₀. - c0Z0Row : Module.End (ZMod 2) (towerM K)
The row from the factor
z₀. - c0_d0Inv_row : self.c0D0InvRow = (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0Factor src * sec7MStageCandidateWildRowManuscriptU1InvFactor src * sec7MStageCandidateWildRowManuscriptX1ConjFactor src) * ((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptD0InvFactor src) - 1)
Fox row for
d₀⁻¹, with the external prefixh₀u₁⁻¹x₁^σ. - c0_z0Inv_row : self.c0Z0InvRow = (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0Factor src * sec7MStageCandidateWildRowManuscriptU1InvFactor src * sec7MStageCandidateWildRowManuscriptX1ConjFactor src * sec7MStageCandidateWildRowManuscriptD0InvFactor src) * ((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptZ0InvFactor src) - 1)
Fox row for
z₀⁻¹. - c0_d0_row : self.c0D0Row = (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0Factor src * sec7MStageCandidateWildRowManuscriptU1InvFactor src * sec7MStageCandidateWildRowManuscriptX1ConjFactor src * sec7MStageCandidateWildRowManuscriptD0InvFactor src * sec7MStageCandidateWildRowManuscriptZ0InvFactor src) * ((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptD0Factor src) - 1)
Fox row for
d₀. - c0_z0_row : self.c0Z0Row = (sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptH0Factor src * sec7MStageCandidateWildRowManuscriptU1InvFactor src * sec7MStageCandidateWildRowManuscriptX1ConjFactor src * sec7MStageCandidateWildRowManuscriptD0InvFactor src * sec7MStageCandidateWildRowManuscriptZ0InvFactor src * sec7MStageCandidateWildRowManuscriptD0Factor src) * ((sec7MStageCandidateActionEnd K) (sec7MStageCandidateWildRowManuscriptZ0Factor src) - 1)
Fox row for
z₀. The four commutator rows cancel, expressing the zero first-order row of
[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 τ-piece in the inverse ω₂-norm row for u₁⁻¹.
Equations
Instances For
Canonical x₁-piece in the inverse ω₂-norm row for u₁⁻¹.
Equations
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.
Checkpoint330 bridge for the checkpoint329 h₀ head primitive preimage 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.
Checkpoint311 nested-head row, recovered theorem-level from the checkpoint312 fully nested head row by unfolding the remaining action-list tail.
Checkpoint310 list-head row, recovered theorem-level from the checkpoint311 fully nested head row.
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₀⁻¹.
Checkpoint332 bridge recovering the checkpoint331 h₀ tail row from the
lower stripped inverse-preimage difference-zero primitive.
Checkpoint331 bridge closing the checkpoint330 h₀ tail difference-zero
residual from the lower x₀-reapplied row.
Checkpoint330 bridge for the checkpoint329 h₀ tail primitive preimage row.
Checkpoint329 bridge for the checkpoint328 h₀ tail atom.
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.
Checkpoint325 bridge for the h₀ tail: apply x₀ to the lower inverse
preimage row and cancel x₀*x₀⁻¹.
Checkpoint324 bridge for the h₀ tail: reapply the visible
u₀ · x₀⁻¹ prefix to the new precore-preimage row.
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₀.
Checkpoint315 h₀ tail atom, now theorem-level from the checkpoint316
fully stripped tail-preimage core.
Checkpoint314 h₀ tail atom, now theorem-level from the checkpoint315
x₀⁻¹-prefix-stripped preimage core.
Checkpoint312 opened h₀ tail row, now theorem-level from the smaller inverse
preimage core above.
Checkpoint311 nested tail-to-z₀⁻¹ row, recovered theorem-level from the
checkpoint312 row after cancelling the common outer g⁻¹ action.
Checkpoint310 tail-to-z₀⁻¹ list row, recovered theorem-level from the
checkpoint311 fully nested tail row.
Checkpoint309 datum for h₀, now theorem-level from two smaller
checkpoint310 rows: first the six-factor head is replaced at a common tail, and
then the remaining tail is rewritten to the fully opened z₀⁻¹ tail.
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.
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.
Checkpoint301 primitive datum for h₀, now theorem-level from the
checkpoint302 nested-action commutator row.
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.
Checkpoint295 lower atom for h₀, now theorem-level from the still more
literal zero-deviation seven-action atom above.
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.
Checkpoint293 product-action fixed-point atom for h₀, now theorem-level
from the literal nested six-factor action datum.
Checkpoint292 raw h₀ six-factor Fox row, now theorem-level from the smaller
product-fixed-point datum and the formal six-factor product rule.
Checkpoint291 h₀ pointwise endomorphism row, now theorem-level from the
raw towerActM six-factor pointwise row.
Former checkpoint290 h₀ operator row, now theorem-level from the pointwise
applied six-factor row.
Checkpoint289 lower atom for h₀, now theorem-level from the still-lower
six-factor Fox row.
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).
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.
Checkpoint282 lower atom for h₀, now theorem-level from the checkpoint283
raw nested primitive-action value.
Checkpoint281 lower atom for h₀, now theorem-level from the checkpoint282
primitive fixed-point statement.
Checkpoint279 lower atom for h₀, now theorem-level from the checkpoint281
raw pointwise displacement form.
Checkpoint278 primitive nested h₀ action atom, now theorem-level from the
smaller six-factor deviation identity.
Checkpoint277 primitive six-factor nested-application atom, now theorem-level from the still more literal d₀-expanded nested action atom.
Checkpoint276 primitive six-factor fixed-point atom for h₀, now theorem-level
from the still more literal nested application of the six primitive actions.
Checkpoint275 primitive h₀ deviation row, now theorem-level from the lower
fixed-point action product atom.
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.
Former checkpoint273 primitive endomorphism-row atom for h₀, now theorem-level
from the pointwise primitive row above.
Former checkpoint272 raw-evaluation six-row atom for h₀, now theorem-level from
the direct primitive lower-quotient action statement above.
Former checkpoint271 named six-factor row atom, now theorem-level from the lower
raw GExpr.eval six-factor row statement.
Former checkpoint270 h₀ head/tail block-row atom, now theorem-level from the
six concrete canonical factor rows and the already-proved six-factor product rule.
Former checkpoint269 h₀ head-tail action-product atom, now theorem-level
from the lower block-row identity.
Former checkpoint268 h₀ six-action product, now theorem-level from the
head/tail action identity.
The h₀ action is trivial, theorem-level from the composable head/tail action
identity.
Checkpoint332 lower primitive for u₁⁻¹: keep only the final recursive
norm-step difference core as a closed zero. The checkpoint331 value at
succ (pred |τ|) is recovered by unfolding one step of
sec7TauReplicateOpenedNormSumAux and solving the displayed additive equation.
Checkpoint332 bridge recovering the checkpoint331 u₁⁻¹ recursive-norm
value from the lower final-step closed-zero primitive.
Checkpoint331 bridge closing the checkpoint330 u₁⁻¹ final-step closed-zero
residual by unfolding the lower recursive norm value.
Checkpoint330 bridge for the checkpoint329 u₁⁻¹ difference-core primitive.
Checkpoint329 bridge for the checkpoint328 u₁⁻¹ closed-zero atom.
Checkpoint328 bridge for the checkpoint327 u₁⁻¹ norm atom: the new datum
is the closed residual after subtracting the auxiliary and final summand. Moving
those terms back gives the displayed final recursive step.
Checkpoint327 bridge for the checkpoint326 u₁⁻¹ norm atom: fold the
single unfolded final recursive summand back into sec7TauReplicateOpenedNormSumAux.
Checkpoint326 bridge for the checkpoint325 u₁⁻¹ residual: unfold the
last recursive summand and cancel by additive algebra.
Checkpoint325 bridge for u₁⁻¹: solve the lower closed zero row for the
last base summand using the elementary ZMod 2 cancellation Y+Y=0.
Checkpoint324 bridge for u₁⁻¹: the checkpoint323 pair-sum row follows
from the isolated-last-summand row by elementary additive algebra.
Checkpoint323 bridge for u₁⁻¹: isolate the final base summand from the
lower two-summand recursive norm row.
Checkpoint322 bridge for u₁⁻¹: the checkpoint321 isolated base-value row
is recovered from the lower positive last-summand row by the characteristic-two
identity Y = -Y on the tower module.
Checkpoint320 bridge for u₁⁻¹: move the isolated last base summand back
across the equality to recover the opened subtraction-zero row.
Checkpoint319 bridge for u₁⁻¹: regroup the checkpoint320 opened last
summand back as subtraction of the displayed final difference.
Checkpoint318 bridge for u₁⁻¹: the checkpoint317 final-step equality is
recovered from the residual form that isolates the last recursive summand after
subtracting the accumulated auxiliary norm prefix.
Checkpoint317 bridge for u₁⁻¹: the checkpoint316 auxiliary row is
recovered by folding the final recursive step of the norm-sum auxiliary at
orderOf τ.
Checkpoint315 u₁⁻¹ base-subtracted row, now theorem-level from the
checkpoint316 auxiliary recursive norm-sum row.
Checkpoint314 u₁⁻¹ value-before-base-sub row, now theorem-level from the
checkpoint315 base-subtracted norm row.
Checkpoint312 opened replicated-list norm row, now theorem-level from the recursive norm-sum datum and the finite-range summation lemma.
Checkpoint311 closed-map-sub norm row, recovered theorem-level from the checkpoint312 row where every replicate-list summand has been opened by linearity.
Checkpoint310 opened replicated-list row for u₁⁻¹, recovered theorem-level
from the checkpoint311 closed-map_sub norm row.
Checkpoint309 u₁⁻¹ datum, now theorem-level from the still more literal
checkpoint310 row where every τ-iterate is an explicit replicated action list.
Checkpoint308 u₁⁻¹ norm row, now theorem-level from the literal summand row
where the named raw-difference helper has been opened as subtraction.
Checkpoint303 primitive datum for u₁⁻¹, now theorem-level from the
checkpoint304 base-deviation norm-summand formula.
Checkpoint302 primitive datum for u₁⁻¹, now theorem-level from the
checkpoint303 pointwise-summand norm formula.
Checkpoint301 primitive datum for u₁⁻¹, now theorem-level from the
checkpoint302 literal norm-sum row.
Checkpoint300 primitive datum for u₁⁻¹, now theorem-level from the
checkpoint301 unfolded-norm value formula.
Checkpoint299 primitive datum for u₁⁻¹, now theorem-level from the
checkpoint300 inverse-value formula.
Checkpoint298 primitive atom for u₁⁻¹, now theorem-level from the
checkpoint299 base-difference balance.
Checkpoint297 primitive atom for u₁⁻¹, now theorem-level from the
four-term checkpoint298 balance.
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).
Checkpoint295 positive inverse-factor deviation for u₁⁻¹, now theorem-level
from the raw value statement above.
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.
Former checkpoint272 raw-evaluation u₁⁻¹ atom, now theorem-level from the direct
primitive lower-quotient action statement above.
Former checkpoint271 Q2Word.u1 raw-evaluation atom, now theorem-level from the
primitive x₁τ expansion of u₁.
Former checkpoint270 u₁⁻¹ action atom, now theorem-level from the raw
GExpr.eval norm-row identity.
Former checkpoint269 u₁⁻¹ x₁-only action atom, now theorem-level from
the lower two-piece ω₂-norm row and src.norm_shadow.
Former checkpoint268 u₁⁻¹ residual, now theorem-level from the non-inverted
ω₂-norm action atom and the inverse-factor identity.
Former checkpoint267 u₁⁻¹ action-sub-one leaf, now theorem-level from the
single residual x₁ action row and the proved norm shadow P(T-1)=0.
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.
Checkpoint332 lower primitive for x₁^σ: keep only the final recursive
norm-step difference core as a closed zero. The checkpoint331 untransported
norm value is recovered by the single recursive unfold.
Checkpoint332 bridge recovering the checkpoint331 x₁^σ recursive-norm
value from the lower final-step closed-zero primitive.
Checkpoint331 bridge closing the checkpoint330 x₁^σ final-step closed-zero
residual by unfolding the lower recursive norm value.
Checkpoint330 bridge for the checkpoint329 x₁^σ difference-core primitive.
Checkpoint329 bridge for the checkpoint328 x₁^σ closed-zero norm atom.
Checkpoint328 bridge for the checkpoint327 P x₁ to σ⁻¹ norm atom: the
new datum is the final-step residual in closed-zero form; additive algebra moves
it back to the displayed recursive summand equality.
Checkpoint327 bridge for the checkpoint326 P x₁ to σ⁻¹ norm atom:
fold the unfolded last recursive summand back into the auxiliary norm sum.
Checkpoint326 bridge for the checkpoint325 P x₁ to σ⁻¹ residual:
unfold the last recursive summand and cancel by additive algebra.
Checkpoint325 bridge for the P x₁ to σ⁻¹ norm comparison: recover the
checkpoint324 isolated last-summand equality from the lower closed zero row.
Checkpoint324 bridge for the P x₁ to σ⁻¹ comparison: the checkpoint323
pair-sum row follows from the isolated-last-summand row.
Checkpoint323 bridge for the P x₁ to σ⁻¹ norm row: isolate the final
base summand from the lower two-summand recursive norm row.
Checkpoint322 bridge for the P x₁ to σ⁻¹ norm row: convert the lower
positive isolated base summand into the checkpoint321 negated isolated base
summand using characteristic two.
Checkpoint320 bridge for the x₁^σ norm row: move the isolated last base
summand back across the equality.
Checkpoint319 bridge for the P x₁ to σ⁻¹ norm comparison: regroup the
checkpoint320 opened last summand back as subtraction of the displayed final
difference.
Checkpoint318 bridge for the P x₁ to σ⁻¹ row: the checkpoint317
final-step equality is recovered from the residual form isolating the last
recursive summand after subtracting the auxiliary norm prefix.
Checkpoint317 bridge for the P x₁ to σ⁻¹ row: the checkpoint316
auxiliary row is recovered by folding the final recursive step of the same
opened norm-sum auxiliary.
Checkpoint315 P x₁ to σ⁻¹ base-subtracted row, now theorem-level from
the checkpoint316 auxiliary recursive norm-sum row.
Checkpoint314 P x₁ to σ⁻¹ value-before-base-sub row, now theorem-level
from the checkpoint315 transported-base-subtracted row.
Checkpoint312 opened replicated-list P x₁/σ⁻¹ row, now theorem-level from
the recursive norm-sum datum.
Checkpoint311 closed-map-sub x₁^σ norm row, recovered theorem-level from
its checkpoint312 summand-opened form.
Checkpoint310 opened replicated-list row for the P x₁ to σ⁻¹ comparison,
recovered theorem-level from the checkpoint311 closed-map_sub row.
Checkpoint309 P x₁/σ⁻¹ datum, now theorem-level from the checkpoint310
row where every iterated τ action is an explicit replicated action list.
Checkpoint308 x₁^σ norm-summand row, now theorem-level from the literal
subtraction form of the same iterated-action summands and target difference.
Checkpoint303 primitive datum for the P/σ⁻¹ part of x₁^σ, now
theorem-level from the checkpoint304 norm-summand difference row.
Checkpoint302 primitive datum for the P/σ⁻¹ part of x₁^σ, now
theorem-level from the checkpoint303 pointwise-summand norm row.
Checkpoint301 primitive datum for the P/σ⁻¹ part of x₁^σ, now
theorem-level from the checkpoint302 literal norm-sum row.
Checkpoint300 primitive datum for the P/σ⁻¹ part of x₁^σ, now
theorem-level from the checkpoint301 unfolded norm/transport row.
Checkpoint299 primitive datum for the P/σ⁻¹ part of x₁^σ, now
theorem-level from the checkpoint300 point-value formula.
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.
Checkpoint332 lower primitive for the transported-square raw corner: keep the isolated single-corner additive difference as a closed zero, before solving it back to the checkpoint331 corner equality.
Checkpoint332 bridge recovering the checkpoint331 transported-square single-corner equality from the lower difference-zero primitive.
Checkpoint331 bridge closing the checkpoint330 transported-square single-corner difference-zero residual from the lower corner equality.
Checkpoint330 bridge for the checkpoint329 transported-square single-corner difference.
Checkpoint329 bridge for the checkpoint328 transported-square corner.
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.
Checkpoint327 bridge for the checkpoint326 transported-square isolated corner: solve the lower closed-zero two-corner row in characteristic two.
Checkpoint326 bridge for the checkpoint325 transported-square four-corner
row: rewrite by the isolated corner equality and use Y+Y=0.
Checkpoint325 bridge for the transported-square row: solve the lower raw four-corner zero row for the isolated first corner.
Checkpoint324 bridge for the transported-square row: add back the remaining corners to the single-corner isolated row and cancel duplicated characteristic-two summands.
Checkpoint323 bridge for the transported-square row: the raw four-corner zero-sum follows from the isolated three-corner equality because the tower module has characteristic two.
Checkpoint322 bridge for the transported-square row: turn the lower raw four-term zero-sum row into the checkpoint321 two-corner balance in the characteristic-two tower module.
Checkpoint320 bridge for the transported-square row: add the two duplicated char-two corners back to the checkpoint321 two-corner balance.
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.
Checkpoint318 bridge for the transported-square row: the checkpoint317
named-difference balance follows from the same equality with the two
sec7TowerActDifference terms opened to literal tower-action differences.
Checkpoint317 bridge for the transported-square row: the checkpoint316 additive balance follows from the same row stated as a difference balance.
Checkpoint315 transported-square subtracted difference core, now theorem-level from the checkpoint316 additive-balance row.
Checkpoint314 transported-square single-action value core, now theorem-level from the checkpoint315 subtracted difference core.
Checkpoint312 transported-square opened equality, now theorem-level from the single-action-difference core above.
Checkpoint311 closed-map-sub transported-square row, recovered theorem-level from the checkpoint312 expression with both transported differences opened.
Checkpoint310 fully opened transported-square equality, recovered theorem-level
from the checkpoint311 closed-map_sub equality.
Checkpoint309 transported-square datum, now theorem-level from the smaller
checkpoint310 equality form before the final sub_eq_zero wrapping.
Checkpoint308 transported-square row, now theorem-level from the fully opened subtraction form of both transported deviation differences.
Checkpoint303 primitive datum for the transported-square part of
x₁^σ, now theorem-level from the checkpoint304 second-difference row.
Checkpoint302 primitive datum for the transported-square part of x₁^σ, now
theorem-level from the checkpoint303 fully distributed pointwise value row.
Checkpoint301 primitive datum for the transported-square part of x₁^σ, now
theorem-level from the checkpoint302 distributed-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 checkpoint272 raw-evaluation σ⁻¹,x₁,σ transport-defect atom, now
theorem-level from the direct primitive lower-quotient action statement 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.
Former checkpoint268 prefix-transport atom, now theorem-level from the h₀ action
identity and the smaller u₁⁻¹ transport atom.
Former checkpoint267 x₁^σ action-product leaf, now theorem-level from the
bare conjugation identity and the smaller u₁⁻¹ prefix-transport atom.
The collapsed prefix contribution of x₁^σ, theorem-level from the explicit
three-action product.
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.
Checkpoint332 bridge recovering the checkpoint331 c₀ primitive action
coincidence from the lower relative-action difference-zero primitive.
Checkpoint331 bridge closing the checkpoint330 c₀ relative-action
fixed-core difference-zero residual from primitive x₀/u₀ action coincidence.
Checkpoint330 bridge for the checkpoint329 c₀ relative-action fixed row.
Checkpoint329 bridge for the checkpoint328 c₀ primitive action equality.
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₀⁻¹.
Checkpoint326 bridge for the checkpoint325 c₀ inverse-preimage atom:
evaluate the lower primitive action agreement at u₀⁻¹ m and cancel.
Checkpoint325 bridge for c₀=[d₀,z₀]: recover the checkpoint324
base-preimage row from the lower equality of inverse preimages.
Checkpoint324 bridge for c₀=[d₀,z₀]: apply u₀ · x₀⁻¹ to the new
base-preimage row and cancel the adjacent inverse tower actions.
Checkpoint323 bridge for c₀=[d₀,z₀]: compare the lower primitive u₀
cancellation row with the already proved x₀*x₀⁻¹ cancellation row.
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₀.
Checkpoint319 bridge for c₀=[d₀,z₀]: apply u₀⁻¹ to the primitive
base action coincidence and cancel u₀⁻¹*u₀ on the left.
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₀.
Checkpoint315 c₀ opened d₀ fixed-point row, now theorem-level from
the checkpoint316 primitive-action coincidence row.
Checkpoint314 c₀ prefix-swap product-opened row, now theorem-level from
the checkpoint315 opened d₀ fixed-point row.
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.
Checkpoint310 prefix-swap row for c₀, recovered theorem-level from the
checkpoint311 nested common-z₀ row.
Checkpoint313 lower atom for the c₀ tail: the assertion that
d₀ = u₀*x₀⁻¹ fixes the point is stated with the product action opened.
Checkpoint312 d₀ tail-fixes-point row, now theorem-level from the opened
product-action tail atom above.
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.
Checkpoint310 tail-insertion list row for c₀, recovered theorem-level from
the checkpoint311 fully nested tail row.
Checkpoint309 c₀ datum, now theorem-level from two smaller checkpoint310
rows: a prefix swap at the common z₀ core and a tail insertion under the new
u₀⁻¹ prefix.
Checkpoint308 c₀ list datum, now theorem-level from the row after the
visible initial x₀⁻¹,x₀ pair on the right-hand side has already been cancelled.
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.
Checkpoint301 primitive datum for c₀=[d₀,z₀], now theorem-level from the
checkpoint302 nested-z₀ commutation row.
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.
Checkpoint298 primitive atom for c₀=[d₀,z₀], now theorem-level from the
checkpoint299 pointwise conjugation row.
Checkpoint297 primitive atom for c₀=[d₀,z₀], now theorem-level from the
fully inlined pointwise commutation checkpoint298 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.
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.
Former checkpoint272 raw-evaluation d₀/z₀ commutator-deviation atom, now
theorem-level from the direct primitive lower-quotient action statement above.
Former checkpoint271 raw d₀/z₀ commutation atom, now theorem-level from the
primitive raw-evaluation x₀,τ,σ expansion.
Former checkpoint270 deviation-commutation atom, now theorem-level from the raw
d₀/z₀ word-evaluation commutation identity.
Former checkpoint269 d₀/z₀ action-commutation atom, now theorem-level from
the lower deviation-commutation identity.
Former checkpoint268 conjugation-invariance atom for c₀, now theorem-level from
commutation of the d₀ and z₀ actions.
Former checkpoint267 c₀ commutator action-product leaf, now theorem-level from
the explicit commutation of the d₀ and z₀ actions.
The c₀ action is trivial, theorem-level from the explicit four-action product.
Smaller manuscript leaf for h₀: the six canonical factor rows cancel.
The former checkpoint266 atom is now theorem-level: the row sum is identified with
ρ(h₀)-1 by the six-factor product rule, and ρ(h₀)=1 is recovered from the explicit
six-action product atom 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₀.
Checkpoint265 row-data leaf for h₀, now theorem-level from the canonical
row-sum leaf.
Checkpoint265 row-data leaf for u₁⁻¹, now theorem-level from canonical
ω₂-norm row pieces.
Checkpoint265 row-data leaf for x₁^σ, now theorem-level from canonical
conjugation rows.
Checkpoint265 row-data leaf for c₀, now theorem-level from canonical
commutator rows.
Former checkpoint264 h₀ internal Fox leaf, now theorem-level from the six
factor-row ledger.
Former checkpoint264 u₁⁻¹ inverse norm leaf, now theorem-level from the two
norm-piece rows.
Former checkpoint264 x₁^σ internal Fox leaf, now theorem-level from the three
conjugation rows.
Former checkpoint264 c₀ internal commutator Fox leaf, now theorem-level from
the four commutator rows.
Former direct h₀ action atom, now theorem-level from the internal six-factor
Fox ledger plus the pure product rule for h₀.
Former direct u₁⁻¹ factor-Fox atom, now theorem-level from an inverse-rule
bridge and the lower ω₂-norm row.
Former direct third-prefix atom, now theorem-level from the internal conjugation ledger and its product-rule bridge.
Former direct fourth-prefix zero atom, now theorem-level from the internal commutator ledger and its product-rule bridge.
Former direct prefix-shadow atom for h₀, now theorem-level from the lower
zero-degree factor-action atom plus the already theorem-level h₀ term shadow.
Former direct prefix-shadow atom for u₁⁻¹, now theorem-level from the lower
inverse-norm factor Fox atom, the h₀ action atom, and the term shadow.
Former direct prefix-shadow atom for x₁^σ, now theorem-level from the lower
third-prefix Fox atom and the term shadow.
Former direct prefix-shadow atom for c₀, now theorem-level from the lower
fourth-prefix zero Fox atom and the term shadow.
Former non-circular product-rule core, now theorem-level from the pure four-factor product rule plus the four lower prefix-shadow atoms.
This proof does not use Sec7FrattiniTrivialElementaryMStageCandidateRelatorShadowData
or any theorem downstream of the canonical manuscript-row chain.
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 canonical finite-word product-rule atom, now theorem-level from the cancelled
canonical row and the fact that the action of a trivial relator is 1.
Former carrier-dependent four-factor product-rule atom, now theorem-level from the canonical product rule and the four manuscript term-shadow equalities.
Former collapsed two-block Fox-derivative atom, now theorem-level from the raw four-factor product rule and the four manuscript term shadows.
Former collapsed Fox-derivative core atom, now theorem-level from the two manuscript operator blocks and their product-rule expansion.
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 collapsed Fox-derivative expansion input, now theorem-level from the manuscript fundamental row plus triviality of the evaluated wild relator in the lower quotient.
Former literal Fox derivative expansion input, now theorem-level from the collapsed manuscript row and the linear distributivity identity.
Former Route250 Fox-derivative expansion atom, now theorem-level from the literal substituted finite-word expansion and the four already evaluated factor shadows.
Former Route249 h₀ factor row, now theorem-level from the term carrier and the
separate lem:h0shadow zero shadow.
Former Route249 u₁⁻¹ factor row, now theorem-level from a term carrier and its
norm-projector shadow.
Former Route249 x₁^σ factor row, now theorem-level from a term carrier and its
conjugation shadow.
Former Route249 commutator row c₀=[d₀,z₀], now theorem-level from a term carrier
and the separate zero-shadow statement.
The evaluated wild relator acts trivially on M once the relator value is 1.
Former Route249 raw product-rule row, now theorem-level from the Fox derivative
expansion plus the theorem-level cancellation ρ(wildRelator)-1=0.
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.
- h0Term : Module.End (ZMod 2) (towerM K)
First-order contribution of
h₀. - u1InvTerm : Module.End (ZMod 2) (towerM K)
First-order contribution of
u₁⁻¹. - x1ConjTerm : Module.End (ZMod 2) (towerM K)
First-order contribution of
x₁^σ. - c0Term : Module.End (ZMod 2) (towerM K)
First-order contribution of
c₀=[d₀,z₀]. - relator_factor_sum : Q2Word.wildRelator.eval src.marking = 1 → self.h0Term + self.u1InvTerm + self.x1ConjTerm + self.c0Term = 0
The raw Fox fundamental sum attached to the actual lower wild relator.
h₀has the first-order shadow ofx₀², hence zero in characteristic two.The
u₁⁻¹term contributes the two norm pieces.The conjugate
x₁^σterm contributesS⁻¹on thex₁coordinate.The commutator
c₀=[d₀,z₀]has no first-order contribution.
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⁰.
h₀has the first-order shadow ofx₀², hence zero in characteristic two.The
u₁⁻¹term contributes the two norm pieces.The conjugate
x₁^σterm contributesS⁻¹on thex₁coordinate.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.
- literal_factor_sum : Q2Word.wildRelator.eval src.marking = 1 → 0 + (src.P * (src.T - 1) + src.P * (src.X₁ - 1)) + src.Sinv * (src.X₁ - 1) + 0 = 0
The evaluated wild row in literal factor order.
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.
- additive_wild_row : Q2Word.wildRelator.eval src.marking = 1 → src.P * (src.T - 1) + src.P * (src.X₁ - 1) + src.Sinv * (src.X₁ - 1) = 0
The evaluated candidate wild row before cancelling the norm term.
Instances For
Former Route242 additive-ledger residual, now theorem-level from the literal factor ledger by additive normalization in the endomorphism group.
Former Route241 residual, now theorem-level: the h₀ shadow is the zero term.
Former Route241 residual, now theorem-level: the u₁⁻¹ term is its explicit ledger
contribution.
Former Route241 residual, now theorem-level: the x₁^σ term is its explicit
S⁻¹-twisted x₁ contribution.
Former Route241 residual, now theorem-level: the commutator factor c₀ has zero
first-order contribution.
Former Route241 product-rule residual, now theorem-level from the smaller Route245 formal product-rule atom.
Former Route240 residual, now theorem-level from the separated wild-row factors and product-rule datum.
Former Route240 residual, now theorem-level by projection from the raw factor packet.
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.
- d1_surjective : Function.Surjective ⇑(Lifting.d1 cand.Sinv cand.T cand.P)
The evaluated candidate Fox--Jacobian has full row rank.
Instances For
Range-top form of the candidate Fox--Jacobian full-row-rank input.
The evaluated candidate Fox--Jacobian has range all of
M².
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.
A linear right inverse to the evaluated candidate Fox--Jacobian.
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.
A section of
d¹over the tame row.A section of
d¹over the wild row.- tameRightInv_spec (m : towerM K) : (Lifting.d1 cand.Sinv cand.T cand.P) (self.tameRightInv m) = (m, 0)
The tame-row section maps to
(m,0). - wildRightInv_spec (m : towerM K) : (Lifting.d1 cand.Sinv cand.T cand.P) (self.wildRightInv m) = (0, m)
The wild-row section maps to
(0,m).
Instances For
Tame-coordinate section of the evaluated candidate Fox--Jacobian.
A section of
d¹over the tame row.- tameRightInv_spec (m : towerM K) : (Lifting.d1 cand.Sinv cand.T cand.P) (self.tameRightInv m) = (m, 0)
The tame-row section maps to
(m,0).
Instances For
Wild-coordinate section of the evaluated candidate Fox--Jacobian.
A section of
d¹over the wild row.- wildRightInv_spec (m : towerM K) : (Lifting.d1 cand.Sinv cand.T cand.P) (self.wildRightInv m) = (0, m)
The wild-row section maps to
(0,m).
Instances For
Carrier map for the tame-coordinate section of the candidate Fox--Jacobian.
- tameRightInv_spec_core (m : towerM K) : (Lifting.d1 cand.Sinv cand.T cand.P) (self.tameRightInv m) = (m, 0)
The chosen carrier is a genuine section over the tame coordinate. Keeping this proof in the map datum lets the old map/spec API be recovered theorem-level from the weaker full-row-surjectivity residual below.
Instances For
Specification for a chosen tame-coordinate section of the candidate Fox--Jacobian.
- tameRightInv_spec (m : towerM K) : (Lifting.d1 cand.Sinv cand.T cand.P) (sec.tameRightInv m) = (m, 0)
Instances For
Carrier map for the wild-coordinate section of the candidate Fox--Jacobian.
- wildRightInv_spec_core (m : towerM K) : (Lifting.d1 cand.Sinv cand.T cand.P) (self.wildRightInv m) = (0, m)
The chosen carrier is a genuine section over the wild coordinate. Keeping this proof in the map datum lets the old map/spec API be recovered theorem-level from the weaker full-row-surjectivity residual below.
Instances For
Specification for a chosen wild-coordinate section of the candidate Fox--Jacobian.
- wildRightInv_spec (m : towerM K) : (Lifting.d1 cand.Sinv cand.T cand.P) (sec.wildRightInv m) = (0, m)
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 carrier map for the tame coordinate, now theorem-level from full-row surjectivity rather than a chosen coordinate section residual.
Former specification for the tame coordinate, now theorem-level from the strengthened map datum above.
Former carrier map for the wild coordinate, now theorem-level from full-row surjectivity rather than a chosen coordinate section residual.
Former specification for the wild coordinate, now theorem-level from the strengthened map datum above.
Former tame-coordinate section atom, now theorem-level from a chosen map and its pointwise section specification.
Former wild-coordinate section atom, now theorem-level from a chosen map and its pointwise section specification.
Former two-coordinate Fox--Jacobian section atom, now theorem-level from its tame and wild row sections.
Former single right-inverse datum, now theorem-level from the two coordinate sections.
Former candidate deformation-duality range-top atom, now theorem-level from the weaker full-row-surjectivity residual.
Former candidate Fox--Jacobian surjectivity residual, now theorem-level from the single row-surjectivity datum.
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
- Q2Presentation.Induction.sec7CandidateZ1Fintype ops = Fintype.ofFinite ↥(Q2Presentation.Lifting.Z1 ops.Sinv ops.T ops.P)
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.
The local finite discrete
G_{ℚ₂}-module corresponding toM.Identification of its underlying vector space with the concrete Section 7 module.
The local source quotient through which this representation factors.
This records the missing semantic source-interface input: after applying
module_equiv, the localG_{ℚ₂}action is transported to the concretetowerActM Kaction of the finite lower quotientC = towerC K.- source_surjective : Function.Surjective ⇑self.source
The local source quotient map is onto the selected finite lower quotient.
- 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 coefficient identification with the concrete tower action.
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.
The local source quotient map onto the finite lower quotient
C = Y/K.- source_surjective : Function.Surjective ⇑self.source
The quotient map realizes the whole lower quotient.
- source_smooth : IsLocallyConstant fun (g : ↑GQ2Profinite.toProfinite.toTop) => self.source g
Continuity/smoothness of the finite quotient map.
Instances For
Local source-interface input for the elementary M-stage, in quotient-map form.
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.
Local Tate/Euler count in terms of the local coefficient dimension.
The chosen coefficient module has the concrete Section 7 dimension.
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.
Local Tate/Euler count in terms of the local coefficient dimension.
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.
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.
- XA : Type
Candidate-source elementary
M-lift index. Boundary-framed candidate surjections are indexed by the elementary lift index.
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.
- BaseA : Type
Candidate lower-child lift index.
- FiberA : Type
Candidate elementary cocycle fibre index.
- lower_equiv : boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd ≃ self.BaseA
The lower-child boundary-framed surjection set is indexed by
BaseA. The elementary fibre cardinality is the common lift multiplicity.
All candidate framed lifts at
pare indexed by lower lift plus cocycle fibre.
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.
- finLowerA : Fintype (boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd)
The actual lower-child candidate surjection set is finite in this stage.
- FiberA : Type
Candidate elementary cocycle fibre index.
The elementary fibre cardinality is the common lift multiplicity.
- total_equiv : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd ≃ boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd × self.FiberA
All candidate framed lifts at
pare lower-child lifts times the 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.
- finLowerA : Fintype (boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd)
The actual lower-child candidate surjection set is finite in this stage.
- total_equiv : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd ≃ boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd × Fin mult.liftMultiplicity
All candidate framed lifts at
pare lower-child lifts times the canonical finite elementary cocycle fibre.
Instances For
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.
- total_equiv : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd ≃ boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd × Fin mult.liftMultiplicity
All candidate framed lifts at
pare lower-child lifts times the canonical finite elementary cocycle 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.
- total_sigma_equiv : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd ≃ (_ : boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd) × Fin mult.liftMultiplicity
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.
- total_sigma_card : Nat.card (boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd) = Nat.card ((_ : boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd) × Fin mult.liftMultiplicity)
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.
- liftProjection : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd → boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd
Projection from a current candidate lift to the lower-child source over which it lies.
- liftProjection_fiber_card (ρ : boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd) : Nat.card { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // self.liftProjection f = ρ } = mult.liftMultiplicity
Every fibre of the projection has the common elementary lift multiplicity.
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.
- cand : Sec7FrattiniTrivialElementaryMStageCandidateCocycleGroupData h chief K hR child
The literal candidate word-complex cocycle group controlling the elementary fibre.
- liftProjection : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd → boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd
Projection from a current candidate lift to the lower-child source over which it lies.
- liftProjection_fiber_equiv (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) : { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // self.liftProjection f = ρ } ≃ ↥(Lifting.Z1 self.cand.Sinv self.cand.T self.cand.P)
Each projection fibre is the literal candidate cocycle torsor.
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.
The literal candidate cocycle torsor has the common elementary lift multiplicity.
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.
The finite quotient/postcomposition homomorphism
Y → Cfor the lower child.- postMap_surj : Function.Surjective ⇑self.postMap
The finite quotient/postcomposition map is onto
C. - boundary_compat (y : p.fst.Y) (b : ↑Boundary.toProfinite.toTop) : p.fst.qYMap y = (ProfiniteGrp.Hom.hom p.snd.beta) b → child.lowerChild.fst.qYMap (self.postMap y) = (ProfiniteGrp.Hom.hom child.lowerChild.snd.beta) b
The finite quotient/postcomposition map preserves the inherited boundary frame.
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.
- postMap_surj : Function.Surjective ⇑post.postMap
The finite postcomposition map is onto the lower child
C.
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.
- boundary_compat (y : p.fst.Y) (b : ↑Boundary.toProfinite.toTop) : p.fst.qYMap y = (ProfiniteGrp.Hom.hom p.snd.beta) b → child.lowerChild.fst.qYMap (post.postMap y) = (ProfiniteGrp.Hom.hom child.lowerChild.snd.beta) b
Compatibility of
q_Yand the lower boundary frame after finite postcomposition.
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.
- post : Sec7FrattiniTrivialElementaryMStageCandidateLiftIndexProjectionPostcompositionMapData h chief K hR child
The finite target-level quotient/postcomposition map
Y → C. - post_surj : Sec7FrattiniTrivialElementaryMStageCandidateLiftIndexProjectionPostcompositionSurjectivityData self.post
The postcomposition map is onto
C. - liftProjectionRaw : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd → Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of child.lowerChild.fst.Y))
Forget an elementary current lift to its lower quotient map
Γ_A ↠ C. - liftProjectionRaw_apply (f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd) (γ : ↑GammaA.toProfinite.toTop) : (ProfiniteGrp.Hom.hom (self.liftProjectionRaw f).hom) γ = self.post.postMap ((ProfiniteGrp.Hom.hom (↑f).hom) γ)
The raw projection is literally postcomposition by the finite map
Y → C.
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.
- boundary_all (f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd) (γ : ↑GammaA.toProfinite.toTop) : child.lowerChild.fst.qYMap ((ProfiniteGrp.Hom.hom (raw.liftProjectionRaw f).hom) γ) = (ProfiniteGrp.Hom.hom child.lowerChild.snd.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) γ)
The projected lower map obeys the lower-child boundary equation for every
γ : Γ_A.
Instances For
Assemble the canonical boundary-framed lower projection from the raw map and the landing proof.
Equations
Instances For
Map from each projection fibre to the literal candidate cocycle group
Lifting.Z1 cand.Sinv cand.T cand.P.
- toCocycle (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) : { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land f = ρ } → ↥(Lifting.Z1 cand.Sinv cand.T cand.P)
Extract the affine cocycle difference between a lift and its lower source.
Instances For
Inverse lift map: add a candidate cocycle to a fixed lower-child source to obtain a current candidate lift in the corresponding projection fibre.
- ofCocycle (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) : ↥(Lifting.Z1 cand.Sinv cand.T cand.P) → { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land f = ρ }
Rebuild a current lift over
ρfrom a literal candidate cocycle.
Instances For
First inverse law for the cocycle/fibre maps: extracting the cocycle from the lift constructed from that cocycle returns the original cocycle.
- to_of (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (z : ↥(Lifting.Z1 cand.Sinv cand.T cand.P)) : toMap.toCocycle ρ (lift.ofCocycle ρ z) = z
toCocycle (ofCocycle z) = z.
Instances For
Second inverse law for the cocycle/fibre maps: rebuilding from the extracted cocycle returns the original current lift in the fibre.
- of_to (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (x : { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land f = ρ }) : lift.ofCocycle ρ (toMap.toCocycle ρ x) = x
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.
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.
The finite quotient/postcomposition homomorphism Y → C is onto, recovered from
its carrier data.
The finite postcomposition map carries the top boundary frame to the inherited lower boundary frame, recovered from its carrier data.
Former raw-projection residual, now theorem-level from the finite target postcomposition map and its surjectivity.
Former boundary-landing residual, now theorem-level from the finite target-level boundary compatibility of the postcomposition map.
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:
- the map from a lift fibre to
Lifting.Z1is obtained from a raw coordinate-valued affine-difference map plus a separate cocycle-membership proof; - the inverse map is obtained from a raw current-lift constructor plus a separate proof that the constructed lift projects to the chosen lower source;
- the inverse laws are reduced to equality of underlying values of the relevant subtypes;
- the multiplicity normalization is reduced to the statement that the
M-stage dimension chosen inmultis the literal concrete dimensionsec7MStageDim K.
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.
- rawCocycleValue (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) : { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land f = ρ } → towerM K × towerM K × towerM K × towerM K
The four additive generator-coordinate differences of a current lift from its lower-child source.
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.
- rawCocycle_mem (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (x : { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land f = ρ }) : diff.rawCocycleValue ρ x ∈ Lifting.Z1 cand.Sinv cand.T cand.P
The raw affine-difference coordinates satisfy the candidate cocycle equation.
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.
- ofCocycleLift (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) : ↥(Lifting.Z1 cand.Sinv cand.T cand.P) → boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd
The current lift obtained by adding the cocycle to the lower-child source.
Instances For
Projection law for the raw inverse-lift constructor.
- ofCocycle_projection (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (z : ↥(Lifting.Z1 cand.Sinv cand.T cand.P)) : sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land (liftRaw.ofCocycleLift ρ z) = ρ
The lift produced from a cocycle projects back to the lower source used to build it.
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.
- to_of_val (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (z : ↥(Lifting.Z1 cand.Sinv cand.T cand.P)) : ↑(toMap.toCocycle ρ (lift.ofCocycle ρ z)) = ↑z
The extracted cocycle has the same underlying four coordinates as the original cocycle.
Instances For
Underlying-lift right inverse law. This removes the proof-irrelevant projection component from the old equality of fibre-subtype elements.
- of_to_val (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (x : { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land f = ρ }) : ↑(lift.ofCocycle ρ (toMap.toCocycle ρ x)) = ↑x
Rebuilding from the extracted cocycle has the same underlying current lift as the original fibre element.
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.
The
M-stage dimension used in the multiplicity packet is the concrete dimension oftowerM 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:
- raw affine differences are extracted coordinate-by-coordinate on the four marked
generators before being bundled as an ambient
A × A × A × Avalue; - cocycle membership is reduced to the literal
d¹ = 0word-complex equation; - construction of a current lift from a cocycle is split into its underlying current candidate epimorphism and the boundary-frame equation, and the projection law is reduced to equality of the underlying lower epimorphism.
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.
- rawSigma (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) : { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land f = ρ } → towerM K
The
σ-coordinate affine difference. - rawTau (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) : { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land f = ρ } → towerM K
The
τ-coordinate affine difference. - rawX0 (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) : { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land f = ρ } → towerM K
The
x₀-coordinate affine difference. - rawX1 (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) : { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land f = ρ } → towerM K
The
x₁-coordinate affine difference.
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.
The σ raw affine-difference coordinate.
- rawSigma (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) : { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land f = ρ } → towerM K
Instances For
The τ raw affine-difference coordinate.
- rawTau (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) : { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land f = ρ } → towerM K
Instances For
The x₀ raw affine-difference coordinate.
- rawX0 (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) : { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land f = ρ } → towerM K
Instances For
The x₁ raw affine-difference coordinate.
- rawX1 (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) : { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land f = ρ } → towerM K
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.
- rawSigma : towerM K
The pointwise
σadditive affine-difference coordinate.
Instances For
Lower residual below the pointwise Sigma affine-difference coordinate: the raw
multiplicative Frattini-quotient value before additivizing it as an element of
towerM K.
- rawSigmaQuotient : towerMgrp K
The raw multiplicative quotient coordinate, prior to the
Additivewrapper.
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
Lower residual: construct the concrete-kernel representative of the Sigma coordinate.
Former multiplicative Frattini-quotient Sigma coordinate residual, now theorem-level
from a concrete-kernel representative by quotienting modulo Φ(K).
Former pointwise Sigma coordinate residual, now theorem-level by additivizing the
multiplicative Frattini-quotient coordinate.
Former σ coordinate residual, now theorem-level from pointwise coordinate
values over the projection fibre.
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
Additivewrapper.
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
Lower residual: construct the concrete-kernel representative of the Tau coordinate.
Former multiplicative Frattini-quotient Tau coordinate residual, now theorem-level
from a concrete-kernel representative by quotienting modulo Φ(K).
Former pointwise Tau coordinate residual, now theorem-level by additivizing the
multiplicative Frattini-quotient coordinate.
Former τ coordinate residual, now theorem-level from pointwise coordinate
values over the projection fibre.
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.
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
Additivewrapper.
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
Lower residual: construct the concrete-kernel representative of the X0 coordinate.
Former multiplicative Frattini-quotient X0 coordinate residual, now theorem-level
from a concrete-kernel representative by quotienting modulo Φ(K).
Former pointwise X0 coordinate residual, now theorem-level by additivizing the
multiplicative Frattini-quotient coordinate.
Former x₀ coordinate residual, now theorem-level from pointwise coordinate
values over the projection fibre.
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.
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
Additivewrapper.
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
Lower residual: construct the concrete-kernel representative of the X1 coordinate.
Former multiplicative Frattini-quotient X1 coordinate residual, now theorem-level
from a concrete-kernel representative by quotienting modulo Φ(K).
Former pointwise X1 coordinate residual, now theorem-level by additivizing the
multiplicative Frattini-quotient coordinate.
Former x₁ coordinate residual, now theorem-level from pointwise coordinate
values over the projection fibre.
Former coordinate residual, now theorem-level from the four marked-generator coordinate constructors.
Former raw-difference residual, now theorem-level from the four coordinate extraction maps.
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.
- rawCocycle_d1_zero (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (x : { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land f = ρ }) : (Lifting.d1 cand.Sinv cand.T cand.P) (diff.rawCocycleValue ρ x) = 0
The extracted raw difference is killed by the evaluated candidate
d¹.
Instances For
Tame-row half of the literal d¹ = 0 equation.
- rawCocycle_d1_tame_zero (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (x : { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land f = ρ }) : ((Lifting.d1 cand.Sinv cand.T cand.P) (diff.rawCocycleValue ρ x)).1 = 0
Instances For
Wild-row half of the literal d¹ = 0 equation.
- rawCocycle_d1_wild_zero (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (x : { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land f = ρ }) : ((Lifting.d1 cand.Sinv cand.T cand.P) (diff.rawCocycleValue ρ x)).2 = 0
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
Lower residual below the tame-row pointwise d¹ = 0 statement: the explicit tame
Fox-Jacobian linear combination on the four raw affine-difference coordinates.
Instances For
Term-level residual below the tame-row formula: the two nonzero tame Fox-row summands are named before asserting that their sum vanishes.
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
The tame-row term carrier is definitional: choose the two displayed Fox-row summands.
Cancellation-only tame-row atom below the former term packet. The carrier fixes the literal summands; this residual states only that the two named terms cancel.
Instances For
Still-lower tame-row cancellation atom: in characteristic two, cancellation of the two named tame Fox-row summands is recorded as equality of the 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.
- tame_terms_dual_sum_zero (φ : Module.Dual (ZMod 2) (towerM K)) : φ (carrier.tameSigmaTerm + carrier.tameTauTerm) = 0
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
Lower residual: prove one-functional scalar equality of the named tame-row summands.
Former scalar-dual annihilation residual, now theorem-level from one-functional
scalar equalities plus characteristic-two cancellation in ZMod 2.
Former tame-row pair-equality residual, now theorem-level from scalar-dual annihilation of the row sum and the characteristic-two cancellation law.
Former cancellation-only tame-row atom, now theorem-level from equality of the two
named summands and the 𝔽₂ additive self-cancellation law.
Former tame-row term packet, now theorem-level from the definitional carrier and the cancellation-only atom.
Former tame-row pointwise residual, now theorem-level from the explicit tame Fox-Jacobian formula.
Former tame-row row-zero residual, now theorem-level from pointwise row-zero proofs.
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
Lower residual below the wild-row pointwise d¹ = 0 statement: the explicit wild
Fox-Jacobian linear combination on the four raw affine-difference coordinates.
- rawCocycle_d1_wild_formula : cand.P (diff.rawCocycleValue ρ x).2.1 + (cand.P + cand.Sinv) (diff.rawCocycleValue ρ x).2.2.2 = 0
Instances For
Term-level residual below the wild-row formula: the two nonzero wild Fox-row summands are named before asserting that their sum vanishes.
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
The wild-row term carrier is definitional: choose the two displayed Fox-row summands.
Cancellation-only wild-row atom below the former term packet. The carrier fixes the literal summands; this residual states only that the two named terms cancel.
Instances For
Still-lower wild-row cancellation atom: in characteristic two, cancellation of the two named wild Fox-row summands is recorded as equality of the summands.
Instances For
Scalar-dual row-sum residual below wild-row pair equality: every dual functional annihilates the sum of the two named wild Fox-row summands.
- wild_terms_dual_sum_zero (φ : Module.Dual (ZMod 2) (towerM K)) : φ (carrier.wildTauTerm + carrier.wildX1Term) = 0
Instances For
Source-level scalar equality below wild-row dual-sum vanishing: for one dual functional, the two displayed wild Fox-row summands have the same scalar value.
Instances For
Lower residual: prove one-functional scalar equality of the named wild-row summands.
Former scalar-dual annihilation residual, now theorem-level from one-functional
scalar equalities plus characteristic-two cancellation in ZMod 2.
Former wild-row pair-equality residual, now theorem-level from scalar-dual annihilation of the row sum and the characteristic-two cancellation law.
Former cancellation-only wild-row atom, now theorem-level from equality of the two
named summands and the 𝔽₂ additive self-cancellation law.
Former wild-row term packet, now theorem-level from the definitional carrier and the cancellation-only atom.
Former wild-row pointwise residual, now theorem-level from the explicit wild Fox-Jacobian formula.
Former wild-row row-zero residual, now theorem-level from pointwise row-zero proofs.
Former d¹=0 residual, now theorem-level from the two row equations.
Former cocycle-condition residual, now theorem-level from the literal d¹=0
word-complex equation.
Former fibre-to-cocycle residual, now theorem-level from raw affine-difference coordinates plus their cocycle-membership proof.
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.
- ofCocycleHom (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) : ↥(Lifting.Z1 cand.Sinv cand.T cand.P) → Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of p.fst.Y))
The underlying current candidate epimorphism obtained from a lower source and a cocycle.
Instances For
Boundary-frame landing for the underlying current lift constructor.
- ofCocycle_boundary (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (z : ↥(Lifting.Z1 cand.Sinv cand.T cand.P)) (γ : ↑GammaA.toProfinite.toTop) : p.fst.qYMap ((ProfiniteGrp.Hom.hom (liftHom.ofCocycleHom ρ z).hom) γ) = (ProfiniteGrp.Hom.hom p.snd.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) γ)
The underlying current candidate epimorphism has the prescribed top boundary value.
Instances For
Raw continuous homomorphism below the current-lift epimorphism constructor.
- ofCocycleRawHom (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (z : ↥(Lifting.Z1 cand.Sinv cand.T cand.P)) : GammaA ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of p.fst.Y)
Instances For
Surjectivity of the raw current-lift homomorphism, separated from the homomorphism.
- ofCocycleRaw_surj (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (z : ↥(Lifting.Z1 cand.Sinv cand.T cand.P)) : Function.Surjective ⇑(ProfiniteGrp.Hom.hom (liftHomRaw.ofCocycleRawHom ρ z))
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
Lower residual below a pointwise raw current-lift homomorphism: an actual
candidate epimorphism for the current target Y; its underlying homomorphism is the raw
map used by the cocycle lift.
- ofCocycleEpi : Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of p.fst.Y))
Instances For
Lower residual: construct the actual current-target epimorphism for one cocycle lift.
Former pointwise raw homomorphism residual, now theorem-level by forgetting the surjectivity field of the actual pointwise current epimorphism.
Former raw current-lift homomorphism residual, now theorem-level from pointwise homomorphism constructors.
Pointwise residual below surjectivity of the raw current-lift homomorphism.
- ofCocycleRaw_surj : Function.Surjective ⇑(ProfiniteGrp.Hom.hom (liftHomRaw.ofCocycleRawHom ρ z))
Instances For
Lower residual below pointwise surjectivity: an actual current-target epimorphism whose underlying homomorphism is the selected raw current-lift homomorphism.
- ofCocycleEpi : Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of p.fst.Y))
Instances For
Lower residual: identify the selected raw homomorphism with an actual epimorphism.
Former pointwise surjectivity residual, now theorem-level from the actual epimorphism and its homomorphism-identification field.
Former raw current-lift surjectivity residual, now theorem-level from pointwise surjectivity proofs.
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.
Generator-level boundary-frame landing for the current-lift constructor.
- ofCocycle_boundary_gen (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (z : ↥(Lifting.Z1 cand.Sinv cand.T cand.P)) (a : Gen) : p.fst.qYMap ((ProfiniteGrp.Hom.hom (liftHom.ofCocycleHom ρ z).hom) (gammaGen a)) = (ProfiniteGrp.Hom.hom p.snd.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))
Instances For
Pointwise generator-boundary residual for a constructed current lift.
- ofCocycle_boundary_gen : p.fst.qYMap ((ProfiniteGrp.Hom.hom (liftHom.ofCocycleHom ρ z).hom) (gammaGen a)) = (ProfiniteGrp.Hom.hom p.snd.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))
Instances For
Lower residual: the H-coordinate of the boundary-frame equation at one generator.
- ofCocycle_boundary_pi_gen : (p.fst.qYMap ((ProfiniteGrp.Hom.hom (liftHom.ofCocycleHom ρ z).hom) (gammaGen a))).1 = ((ProfiniteGrp.Hom.hom p.snd.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))).1
Instances For
Lower residual: the decoration-coordinate of the boundary-frame equation at one generator.
- ofCocycle_boundary_theta_gen : (p.fst.qYMap ((ProfiniteGrp.Hom.hom (liftHom.ofCocycleHom ρ z).hom) (gammaGen a))).2 = ((ProfiniteGrp.Hom.hom p.snd.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))).2
Instances For
Raw generator-boundary residual below the two boundary-coordinate equations.
It states the full boundary-frame equality before projecting to the H and decoration
coordinates.
- ofCocycle_boundary_raw_gen : p.fst.qYMap ((ProfiniteGrp.Hom.hom (liftHom.ofCocycleHom ρ z).hom) (gammaGen a)) = (ProfiniteGrp.Hom.hom p.snd.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))
Instances For
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.
- actualBoundary_eq : self.actualBoundary = p.fst.qYMap ((ProfiniteGrp.Hom.hom (liftHom.ofCocycleHom ρ z).hom) (gammaGen a))
- expectedBoundary_eq : self.expectedBoundary = (ProfiniteGrp.Hom.hom p.snd.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))
Instances For
The raw boundary carrier is closed by choosing the displayed actual and expected boundary values.
Equality-only raw boundary atom below the former boundary point residual.
Instances For
Lower boundary raw equality residual: equality of the H-coordinate of the named
actual and expected boundary values.
Instances For
Lower boundary raw equality residual: equality of the decoration-coordinate of the named actual and expected boundary values.
Instances For
Multiplicative-defect residual below the H-coordinate boundary equality.
- actualBoundary_pi_mul_expected_inv_eq_one : carrier.actualBoundary.1 * carrier.expectedBoundary.1⁻¹ = 1
Instances For
Source-level H-coordinate boundary equality at one generator. This removes the
artificial boundary carrier and states the equality on the actual constructed lift and the
expected boundary frame value.
- source_boundary_pi_eq : (p.fst.qYMap ((ProfiniteGrp.Hom.hom (liftHom.ofCocycleHom ρ z).hom) (gammaGen a))).1 = ((ProfiniteGrp.Hom.hom p.snd.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))).1
Instances For
Lower residual: prove the source-level H-coordinate boundary equality.
Former H-coordinate multiplicative-defect residual, now theorem-level from the
source-level boundary coordinate equality.
Former H-coordinate boundary equality residual, now theorem-level from triviality
of the corresponding multiplicative defect.
Multiplicative-defect residual below the decoration-coordinate boundary equality.
- actualBoundary_theta_mul_expected_inv_eq_one : carrier.actualBoundary.2 * carrier.expectedBoundary.2⁻¹ = 1
Instances For
Source-level decoration-coordinate boundary equality at one generator.
- source_boundary_theta_eq : (p.fst.qYMap ((ProfiniteGrp.Hom.hom (liftHom.ofCocycleHom ρ z).hom) (gammaGen a))).2 = ((ProfiniteGrp.Hom.hom p.snd.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))).2
Instances For
Lower residual: prove the source-level decoration-coordinate boundary equality.
Former decoration-coordinate multiplicative-defect residual, now theorem-level from the source-level boundary coordinate equality.
Former decoration-coordinate boundary equality residual, now theorem-level from triviality of the corresponding multiplicative defect.
Former raw boundary equality atom, now theorem-level from its two coordinate equality atoms.
Former raw generator boundary residual, now theorem-level from a closed value carrier and the equality-only boundary atom.
Lower residual: prove the decoration-coordinate of generator boundary landing.
Former pointwise boundary-generator residual, now theorem-level from its two boundary coordinates.
Former generator-level boundary residual, now theorem-level from pointwise generator boundary equations.
Former boundary residual, now theorem-level from generator-level boundary landing and
gammaGen_hom_ext.
Former raw current-lift construction residual, now theorem-level from the underlying current candidate epimorphism and its boundary-frame equation.
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.
- ofCocycle_projection_val (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (z : ↥(Lifting.Z1 cand.Sinv cand.T cand.P)) : ↑(sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land (liftRaw.ofCocycleLift ρ z)) = ↑ρ
The underlying projected lower epimorphism is the lower source used in the construction.
Instances For
Generator-level form of the projection law for a lift constructed from a cocycle.
- ofCocycle_projection_gen (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (z : ↥(Lifting.Z1 cand.Sinv cand.T cand.P)) (a : Gen) : (ProfiniteGrp.Hom.hom (↑(sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land (liftRaw.ofCocycleLift ρ z))).hom) (gammaGen a) = (ProfiniteGrp.Hom.hom (↑ρ).hom) (gammaGen a)
Instances For
Pointwise generator residual for the projection law of a constructed lift.
- ofCocycle_projection_gen : (ProfiniteGrp.Hom.hom (↑(sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land (liftRaw.ofCocycleLift ρ z))).hom) (gammaGen a) = (ProfiniteGrp.Hom.hom (↑ρ).hom) (gammaGen a)
Instances For
Lower residual below the projection generator equation: explicitly named finite-target values for the projected lift and the chosen lower source.
- projectedValue : child.lowerChild.fst.Y
- lowerValue : child.lowerChild.fst.Y
- projectedValue_eq : self.projectedValue = (ProfiniteGrp.Hom.hom (↑(sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land (liftRaw.ofCocycleLift ρ z))).hom) (gammaGen a)
Instances For
Raw postcomposition form below the projection-generator value packet: after the
constructed current lift is evaluated at a generator, the finite quotient map Y → C
returns the chosen lower-source generator value.
- postMap_ofCocycle_gen : raw.post.postMap ((ProfiniteGrp.Hom.hom (↑(liftRaw.ofCocycleLift ρ z)).hom) (gammaGen a)) = (ProfiniteGrp.Hom.hom (↑ρ).hom) (gammaGen a)
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.
- projectedValue : child.lowerChild.fst.Y
- lowerValue : child.lowerChild.fst.Y
- currentValue_eq : self.currentValue = (ProfiniteGrp.Hom.hom (↑(liftRaw.ofCocycleLift ρ z)).hom) (gammaGen a)
Instances For
The finite postcomposition carrier is closed by choosing the displayed values.
Equality-only finite postcomposition atom below the former projection point 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
Multiplicative-defect residual below the finite postcomposition current-value equality.
- postMap_current_mul_lower_inv_eq_one : raw.post.postMap carrier.currentValue * carrier.lowerValue⁻¹ = 1
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.
- source_postMap_current_eq_lower : raw.post.postMap ((ProfiniteGrp.Hom.hom (↑(liftRaw.ofCocycleLift ρ z)).hom) (gammaGen a)) = (ProfiniteGrp.Hom.hom (↑ρ).hom) (gammaGen a)
Instances For
Lower residual: prove the source-level finite postcomposition equality.
Former finite postcomposition multiplicative-defect residual, now theorem-level from the source-level postcomposition equality.
Former finite postcomposition current-value equality residual, now theorem-level from triviality of its multiplicative defect.
Former finite postcomposition equality atom, now theorem-level from the actual quotient-map equality on the named current value.
Former finite postcomposition point residual, now theorem-level from a closed carrier and an equality-only finite-target atom.
Former pointwise projection-generator residual, now theorem-level from named finite projection values.
Former projection generator residual, now theorem-level from pointwise generator projection equations.
Former underlying projection residual, now theorem-level from generator values and
gammaGen_hom_ext.
Former projection-law residual, now theorem-level from equality of the underlying lower epimorphism.
Former inverse-lift residual, now theorem-level from a raw lift constructor and its projection law.
σ-coordinate of the left inverse law on the underlying four-coordinate value.
- to_of_sigma (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (z : ↥(Lifting.Z1 cand.Sinv cand.T cand.P)) : (↑(toMap.toCocycle ρ (lift.ofCocycle ρ z))).1 = (↑z).1
Instances For
τ-coordinate of the left inverse law on the underlying four-coordinate value.
- to_of_tau (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (z : ↥(Lifting.Z1 cand.Sinv cand.T cand.P)) : (↑(toMap.toCocycle ρ (lift.ofCocycle ρ z))).2.1 = (↑z).2.1
Instances For
x₀-coordinate of the left inverse law on the underlying four-coordinate value.
- to_of_x0 (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (z : ↥(Lifting.Z1 cand.Sinv cand.T cand.P)) : (↑(toMap.toCocycle ρ (lift.ofCocycle ρ z))).2.2.1 = (↑z).2.2.1
Instances For
x₁-coordinate of the left inverse law on the underlying four-coordinate value.
- to_of_x1 (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (z : ↥(Lifting.Z1 cand.Sinv cand.T cand.P)) : (↑(toMap.toCocycle ρ (lift.ofCocycle ρ z))).2.2.2 = (↑z).2.2.2
Instances For
Pointwise σ coordinate residual for the cocycle-lift left inverse law.
Instances For
Lower residual below the Sigma left-inverse coordinate: the additive difference of
the two Sigma coordinates is zero.
Instances For
Direct coordinate-equality residual below the Sigma left-inverse sub-zero
packet; the subtractive zero statement is recovered theorem-level by sub_eq_zero.
Instances For
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
The Sigma coordinate carrier is closed by choosing the displayed extracted and
input coordinates.
Equality-only atom below the Sigma coordinate left-inverse residual.
Instances For
Scalar-evaluation residual below the Sigma coordinate equality in the left-inverse
law: every dual functional has the same value on the extracted and input coordinates.
- dual_eval_eq (φ : Module.Dual (ZMod 2) (towerM K)) : φ carrier.extractedValue = φ carrier.inputValue
Instances For
Difference-zero scalar-evaluation residual below the Sigma left-inverse dual-eval
packet: every dual functional kills the additive error between the extracted and input
coordinates.
- dual_difference_zero (φ : Module.Dual (ZMod 2) (towerM K)) : φ (carrier.extractedValue - carrier.inputValue) = 0
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
Lower residual: prove source-level scalar-dual vanishing of the Sigma coordinate
left-inverse error for one dual functional.
Former carrier-level dual-difference residual, now theorem-level from the direct source-coordinate scalar residual.
Former Sigma dual-evaluation residual, now theorem-level from scalar-dual
vanishing of the additive error.
Former equality-only Sigma left-inverse atom, now theorem-level from all dual
scalar evaluations and finite-dimensional/projective separation.
Former Sigma direct coordinate residual, now theorem-level from a closed carrier
and an equality-only coordinate atom.
Former pointwise Sigma left-inverse residual, now theorem-level from the additive
zero-difference form.
Former σ coordinate left-inverse residual, now theorem-level from pointwise
coordinate equations.
Pointwise τ coordinate residual for the cocycle-lift left inverse law.
Instances For
Lower residual below the Tau left-inverse coordinate: the additive difference of
the two Tau coordinates is zero.
Instances For
Direct coordinate-equality residual below the Tau left-inverse sub-zero
packet; the subtractive zero statement is recovered theorem-level by sub_eq_zero.
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
The Tau coordinate carrier is closed by choosing the displayed extracted and
input coordinates.
Equality-only atom below the Tau coordinate left-inverse residual.
Instances For
Scalar-evaluation residual below the Tau coordinate equality in the left-inverse
law: every dual functional has the same value on the extracted and input coordinates.
- dual_eval_eq (φ : Module.Dual (ZMod 2) (towerM K)) : φ carrier.extractedValue = φ carrier.inputValue
Instances For
Difference-zero scalar-evaluation residual below the Tau left-inverse dual-eval
packet: every dual functional kills the additive error between the extracted and input
coordinates.
- dual_difference_zero (φ : Module.Dual (ZMod 2) (towerM K)) : φ (carrier.extractedValue - carrier.inputValue) = 0
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.
Instances For
Lower residual: prove source-level scalar-dual vanishing of the Tau coordinate
left-inverse error for one dual functional.
Former carrier-level dual-difference residual, now theorem-level from the direct source-coordinate scalar residual.
Former Tau dual-evaluation residual, now theorem-level from scalar-dual
vanishing of the additive error.
Former equality-only Tau left-inverse atom, now theorem-level from all dual
scalar evaluations and finite-dimensional/projective separation.
Former Tau direct coordinate residual, now theorem-level from a closed carrier
and an equality-only coordinate atom.
Former pointwise Tau left-inverse residual, now theorem-level from the additive
zero-difference form.
Former τ coordinate left-inverse residual, now theorem-level from pointwise
coordinate equations.
Pointwise x₀ coordinate residual for the cocycle-lift left inverse law.
Instances For
Lower residual below the X0 left-inverse coordinate: the additive difference of
the two X0 coordinates is zero.
Instances For
Direct coordinate-equality residual below the X0 left-inverse sub-zero
packet; the subtractive zero statement is recovered theorem-level by sub_eq_zero.
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
The X0 coordinate carrier is closed by choosing the displayed extracted and
input coordinates.
Equality-only atom below the X0 coordinate left-inverse residual.
Instances For
Scalar-evaluation residual below the X0 coordinate equality in the left-inverse
law: every dual functional has the same value on the extracted and input coordinates.
- dual_eval_eq (φ : Module.Dual (ZMod 2) (towerM K)) : φ carrier.extractedValue = φ carrier.inputValue
Instances For
Difference-zero scalar-evaluation residual below the X0 left-inverse dual-eval
packet: every dual functional kills the additive error between the extracted and input
coordinates.
- dual_difference_zero (φ : Module.Dual (ZMod 2) (towerM K)) : φ (carrier.extractedValue - carrier.inputValue) = 0
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.
Instances For
Lower residual: prove source-level scalar-dual vanishing of the X0 coordinate
left-inverse error for one dual functional.
Former carrier-level dual-difference residual, now theorem-level from the direct source-coordinate scalar residual.
Former X0 dual-evaluation residual, now theorem-level from scalar-dual
vanishing of the additive error.
Former equality-only X0 left-inverse atom, now theorem-level from all dual
scalar evaluations and finite-dimensional/projective separation.
Former X0 direct coordinate residual, now theorem-level from a closed carrier
and an equality-only coordinate atom.
Former pointwise X0 left-inverse residual, now theorem-level from the additive
zero-difference form.
Former x₀ coordinate left-inverse residual, now theorem-level from pointwise
coordinate equations.
Pointwise x₁ coordinate residual for the cocycle-lift left inverse law.
Instances For
Lower residual below the X1 left-inverse coordinate: the additive difference of
the two X1 coordinates is zero.
Instances For
Direct coordinate-equality residual below the X1 left-inverse sub-zero
packet; the subtractive zero statement is recovered theorem-level by sub_eq_zero.
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
The X1 coordinate carrier is closed by choosing the displayed extracted and
input coordinates.
Equality-only atom below the X1 coordinate left-inverse residual.
Instances For
Scalar-evaluation residual below the X1 coordinate equality in the left-inverse
law: every dual functional has the same value on the extracted and input coordinates.
- dual_eval_eq (φ : Module.Dual (ZMod 2) (towerM K)) : φ carrier.extractedValue = φ carrier.inputValue
Instances For
Difference-zero scalar-evaluation residual below the X1 left-inverse dual-eval
packet: every dual functional kills the additive error between the extracted and input
coordinates.
- dual_difference_zero (φ : Module.Dual (ZMod 2) (towerM K)) : φ (carrier.extractedValue - carrier.inputValue) = 0
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.
Instances For
Lower residual: prove source-level scalar-dual vanishing of the X1 coordinate
left-inverse error for one dual functional.
Former carrier-level dual-difference residual, now theorem-level from the direct source-coordinate scalar residual.
Former X1 dual-evaluation residual, now theorem-level from scalar-dual
vanishing of the additive error.
Former equality-only X1 left-inverse atom, now theorem-level from all dual
scalar evaluations and finite-dimensional/projective separation.
Former X1 direct coordinate residual, now theorem-level from a closed carrier
and an equality-only coordinate atom.
Former pointwise X1 left-inverse residual, now theorem-level from the additive
zero-difference form.
Former x₁ coordinate left-inverse residual, now theorem-level from pointwise
coordinate equations.
Former value-level left inverse residual, now theorem-level from the four coordinate left inverse laws.
Former left-inverse residual, now theorem-level from equality of the underlying four-coordinate cocycle values.
Generator-level right inverse law for the current lift reconstructed from an extracted cocycle.
- of_to_gen (ρ : boundaryFramedSurj boundaryPackage_GammaA child.lowerChild.fst child.lowerChild.snd) (x : { f : boundaryFramedSurj boundaryPackage_GammaA p.fst p.snd // sec7_frattiniTrivial_elementaryMStageCandidateLiftIndexProjectionFromRaw raw land f = ρ }) (a : Gen) : (ProfiniteGrp.Hom.hom (↑↑(lift.ofCocycle ρ (toMap.toCocycle ρ x))).hom) (gammaGen a) = (ProfiniteGrp.Hom.hom (↑↑x).hom) (gammaGen a)
Instances For
Pointwise generator residual for the cocycle-lift right inverse law.
- of_to_gen : (ProfiniteGrp.Hom.hom (↑↑(lift.ofCocycle ρ (toMap.toCocycle ρ x))).hom) (gammaGen a) = (ProfiniteGrp.Hom.hom (↑↑x).hom) (gammaGen a)
Instances For
Lower residual below the right-inverse generator equation: explicitly named finite target values for the rebuilt and original current lift.
- rebuiltValue_eq : self.rebuiltValue = (ProfiniteGrp.Hom.hom (↑↑(lift.ofCocycle ρ (toMap.toCocycle ρ x))).hom) (gammaGen a)
Instances For
Direct generator-equality residual below the right-inverse value packet; the artificially named rebuilt/original finite values are recovered theorem-level.
- rebuilt_eq_original_gen : (ProfiniteGrp.Hom.hom (↑↑(lift.ofCocycle ρ (toMap.toCocycle ρ x))).hom) (gammaGen a) = (ProfiniteGrp.Hom.hom (↑↑x).hom) (gammaGen a)
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.
- rebuiltValue_eq : self.rebuiltValue = (ProfiniteGrp.Hom.hom (↑↑(lift.ofCocycle ρ (toMap.toCocycle ρ x))).hom) (gammaGen a)
Instances For
The right-inverse generator carrier is closed by choosing the displayed rebuilt and original values.
Equality-only atom below the right-inverse generator residual.
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.
- rebuilt_mul_original_inv_mem_kernelFrattini : carrier.rebuiltValue * carrier.originalValue⁻¹ ∈ kernelFrattini K
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.
- defectInK : ↥K.Ksub
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 direct right-inverse generator residual, now theorem-level from a closed carrier and an equality-only generator-value atom.
Former pointwise right-inverse generator residual, now theorem-level from named finite source values.
Former right-inverse generator residual, now theorem-level from pointwise generator equalities.
Former right-inverse residual, now theorem-level from generator-level equality and
gammaGen_hom_ext.
Former right-inverse residual, now theorem-level from equality of the underlying current candidate lifts.
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 cardinality-only sigma-fibre residual, now theorem-level from the fibrewise projection/cardinality datum.
Former sigma-fibre candidate lift-index residual, now theorem-level from the cardinality-only sigma-fibre residual and finite-cardinality choice.
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 arbitrary-fibre canonical lift-index datum, now theorem-level from the
canonical Fin liftMultiplicity fibre.
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.
Former candidate source-index residual, now theorem-level from an actual lift-index bijection.
Product/fibre form of the local elementary lift index.
- BaseQ : Type
Local lower-child lift index.
- FiberQ : Type
Local elementary cocycle fibre index.
The lower-child local boundary-framed surjection set is indexed by
BaseQ.The elementary fibre cardinality is the common lift multiplicity.
All local framed lifts at
pare indexed by lower lift plus cocycle fibre.
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.
- finTotalQ : Fintype (boundaryFramedSurj boundaryPackage_GQ2 p.fst p.snd)
The total local framed lift set is finite at this elementary stage.
- finLowerQ : Fintype (boundaryFramedSurj boundaryPackage_GQ2 D.lowerChild.fst D.lowerChild.snd)
The local lower-child framed lift set is finite at this elementary stage.
- liftProjection : boundaryFramedSurj boundaryPackage_GQ2 p.fst p.snd → boundaryFramedSurj boundaryPackage_GQ2 D.lowerChild.fst D.lowerChild.snd
Projection from a local lift of
pto its lower-child local lift. - liftProjection_fiber_card (ρ : boundaryFramedSurj boundaryPackage_GQ2 D.lowerChild.fst D.lowerChild.snd) : Nat.card { f : boundaryFramedSurj boundaryPackage_GQ2 p.fst p.snd // self.liftProjection f = ρ } = mult.liftMultiplicity
Every projection fibre has the common elementary cocycle cardinality.
Instances For
Cardinality-only sigma-fibre form of the local lift index.
- finTotalQ : Fintype (boundaryFramedSurj boundaryPackage_GQ2 p.fst p.snd)
The total local framed lift set is finite.
- finLowerQ : Fintype (boundaryFramedSurj boundaryPackage_GQ2 D.lowerChild.fst D.lowerChild.snd)
The local lower-child framed lift set is finite.
- total_sigma_card : Nat.card (boundaryFramedSurj boundaryPackage_GQ2 p.fst p.snd) = Nat.card ((_ : boundaryFramedSurj boundaryPackage_GQ2 D.lowerChild.fst D.lowerChild.snd) × Fin mult.liftMultiplicity)
The total local lift set has the cardinality of the constant-fibre sigma index.
Instances For
Sigma-fibre bijective form of the local lift index.
- finLowerQ : Fintype (boundaryFramedSurj boundaryPackage_GQ2 D.lowerChild.fst D.lowerChild.snd)
The local lower-child framed lift set is finite.
- total_sigma_equiv : boundaryFramedSurj boundaryPackage_GQ2 p.fst p.snd ≃ (_ : boundaryFramedSurj boundaryPackage_GQ2 D.lowerChild.fst D.lowerChild.snd) × Fin mult.liftMultiplicity
All local framed lifts at
pare a sigma family with constant fibreFin liftMultiplicityover lower-child local lifts.
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 sigma-cardinality lift-index residual, now theorem-level from the projection and constant fibre-cardinality datum.
Former local sigma-fibre lift-index equivalence, now theorem-level from finite cardinality choice.
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 local source-index residual, now theorem-level from the local product index decomposition.
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.
- partition_card : Nat.card src.XA + (List.map (⇑Cardinal.toNat) (List.map framedCountA D.properChildren)).sum = mult.liftMultiplicity * Cardinal.toNat (framedCountA D.lowerChild)
Candidate exact-image partition cardinality in additive form.
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.
- ProperA : Type
Finite index for all proper exact-image contributions.
- LowerA : Type
Finite index for the candidate lower-child framed lifts.
- proper_card : Nat.card self.ProperA = (List.map (⇑Cardinal.toNat) (List.map framedCountA D.properChildren)).sum
The proper-image index has the cardinality of the proper-child sum.
The lower-child index has the cardinality of the lower-child framed count.
The exact-image partition as a finite bijection.
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.
- ProperA : Type
Finite index for all proper exact-image contributions.
- finLowerA : Fintype (boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd)
The actual lower-child candidate surjection set is finite in this stage.
- proper_card : Nat.card self.ProperA = (List.map (⇑Cardinal.toNat) (List.map framedCountA D.properChildren)).sum
The proper-image index has the cardinality of the proper-child sum.
- lower_card : Nat.card (boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd) = Cardinal.toNat (framedCountA D.lowerChild)
The actual lower-child index has the cardinality of the lower-child framed count.
- partition_equiv : src.XA ⊕ self.ProperA ≃ Fin mult.liftMultiplicity × boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd
The exact-image partition as a finite bijection over the actual lower-child index.
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.
- finLowerA : Fintype (boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd)
The actual lower-child candidate surjection set is finite in this stage.
- lower_card : Nat.card (boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd) = Cardinal.toNat (framedCountA D.lowerChild)
The actual lower-child index has the cardinality of the lower-child framed count.
- partition_equiv : src.XA ⊕ Fin (List.map (⇑Cardinal.toNat) (List.map framedCountA D.properChildren)).sum ≃ Fin mult.liftMultiplicity × boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd
The exact-image partition over the canonical finite proper-image index.
Instances For
Lower-child cardinality half of the canonical candidate exact-image partition.
- finLowerA : Fintype (boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd)
The actual lower-child candidate surjection set is finite in this stage.
- lower_card : Nat.card (boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd) = Cardinal.toNat (framedCountA D.lowerChild)
The actual lower-child candidate index has the cardinality of the lower-child framed count.
Instances For
Bijection half of the canonical candidate exact-image partition.
- partition_equiv : src.XA ⊕ Fin (List.map (⇑Cardinal.toNat) (List.map framedCountA D.properChildren)).sum ≃ Fin mult.liftMultiplicity × boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd
The exact-image partition over the canonical finite proper-image index.
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.
- partition_sigma_equiv : src.XA ⊕ Fin (List.map (⇑Cardinal.toNat) (List.map framedCountA D.properChildren)).sum ≃ (_ : Fin mult.liftMultiplicity) × boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd
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.
- partition_sigma_card : Nat.card (src.XA ⊕ Fin (List.map (⇑Cardinal.toNat) (List.map framedCountA D.properChildren)).sum) = Nat.card ((_ : Fin mult.liftMultiplicity) × boundaryFramedSurj boundaryPackage_GammaA D.lowerChild.fst D.lowerChild.snd)
Instances For
Former bijective sigma-fibre partition input, now theorem-level from the strictly weaker finite-cardinality partition statement.
Former product-form candidate exact-image partition input, now theorem-level from the sigma-fibre partition and the canonical constant-fibre sigma/product equivalence.
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.
Former arbitrary-proper-index exact-image partition datum, now theorem-level from the
canonical Fin (Σ proper child counts) index.
Former finite disjoint-union exact-image partition atom, now theorem-level from the canonical partition over the actual lower-child candidate surjection set.
Former candidate exact-image partition residual, now theorem-level from the finite partition bijection and the two child-index cardinality identifications.
Former candidate exact-count residual, now theorem-level from the additive exact-image partition cardinality.
Finite disjoint-union form of the local exact-image partition.
- ProperQ : Type
Finite index for all local proper exact-image contributions.
- LowerQ : Type
Finite index for the local lower-child framed lifts.
- proper_card : Nat.card self.ProperQ = (List.map (⇑Cardinal.toNat) (List.map framedCountQ D.properChildren)).sum
The proper-image index has the cardinality of the local proper-child sum.
The lower-child index has the cardinality of the local lower-child framed count.
The local exact-image partition as a finite bijection.
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.
- finLowerQ : Fintype (boundaryFramedSurj boundaryPackage_GQ2 D.lowerChild.fst D.lowerChild.snd)
The actual local lower-child boundary-framed surjection set is finite.
- lower_card : Nat.card (boundaryFramedSurj boundaryPackage_GQ2 D.lowerChild.fst D.lowerChild.snd) = Cardinal.toNat (framedCountQ D.lowerChild)
The actual local lower-child index has the cardinality of the lower-child framed local count.
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.
- partition_sigma_card : Nat.card (src.XQ ⊕ Fin (List.map (⇑Cardinal.toNat) (List.map framedCountQ D.properChildren)).sum) = Nat.card ((_ : Fin mult.liftMultiplicity) × boundaryFramedSurj boundaryPackage_GQ2 D.lowerChild.fst D.lowerChild.snd)
Instances For
Bijection form of the local exact-image partition before flattening the constant lower-child sigma fibre.
- partition_sigma_equiv : src.XQ ⊕ Fin (List.map (⇑Cardinal.toNat) (List.map framedCountQ D.properChildren)).sum ≃ (_ : Fin mult.liftMultiplicity) × boundaryFramedSurj boundaryPackage_GQ2 D.lowerChild.fst D.lowerChild.snd
Instances For
Product-form canonical local exact-image partition over the actual lower-child local source set.
- finLowerQ : Fintype (boundaryFramedSurj boundaryPackage_GQ2 D.lowerChild.fst D.lowerChild.snd)
The actual local lower-child boundary-framed surjection set is finite.
- lower_card : Nat.card (boundaryFramedSurj boundaryPackage_GQ2 D.lowerChild.fst D.lowerChild.snd) = Cardinal.toNat (framedCountQ D.lowerChild)
The lower-child local source set has the framed lower-child cardinality.
- partition_equiv : src.XQ ⊕ Fin (List.map (⇑Cardinal.toNat) (List.map framedCountQ D.properChildren)).sum ≃ Fin mult.liftMultiplicity × boundaryFramedSurj boundaryPackage_GQ2 D.lowerChild.fst D.lowerChild.snd
The exact-image partition over the canonical finite proper-image index.
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.
Former local exact-image sigma-partition equivalence, now theorem-level from the finite cardinality statement and the lower-child finiteness/cardinality residual.
Former product-form local exact-image partition, now theorem-level from the sigma-fibre partition and the canonical constant-fibre sigma/product equivalence.
Former local exact-image partition residual, now theorem-level from the canonical finite proper-image index and the actual local lower-child source set.
Former local exact-count residual, now theorem-level from the local finite partition bijection.
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 exact-count residual, now theorem-level. The paired exact-image
subtraction packet is assembled from its candidate and local eq:Mstage halves.
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.
Former normalized source-count residual, now theorem-level. The old normalized-count
packet is assembled from the concrete eq:Mstage count packet by using the common
functional z_M · e(C) - Σ_J e(J) as partialN.
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.