Generic layer: the child bridge across the collapse #
The forward collapse (B_λ)/(R/ker λ) → Y/R as a hom of finite discrete
profinite groups (mirror of scalarCollapseInvHom, other direction;
source-generic — placed here as its only consumer is the child bridge).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The child transport is a bijection: g ↦ scalarCoverChild g
(post-composition with the group isomorphism scalarCollapse.symm) is an
equivalence between the child-framed surjection sets of Y/R and of
(B_λ)/(R/ker λ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Lift-set match under the bridge is DEFINITIONAL (ScalarPushout.lean: 461–468): the keep's cover-lift set at g is the engine's lift set at the
transported child. Recorded as a rfl-lemma for readability.
Generic layer: the child marked kernel across the collapse #
The collapse carries the cover-child marked kernel into the plain child marked kernel.
The inverse collapse carries the plain child marked kernel into the cover-child marked kernel.
The collapse restricts to a bijection of the child marked kernels — the cover child and the plain child have the SAME framed measure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pinned instantiation at the Frattini layer #
The exact-image strata of the scalar cover: subgroups of B_λ mapping
onto the child (J̃ ≤ p_λ⁻¹(B) with p_λ(J̃) = B — the manuscript sum index
of eq:covertransform at the full lower target).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The stratum framed pair (J̃, J̃ ∩ L̃, π̃|_J̃, θ̃|_J̃; same frame) —
an ordinary exact-image object in the same global boundary-framed category
(same H, same E, p.2's frame verbatim), ready for the engine's children
lists. Its measure is |J̃ ∩ L̃|, lem:strictdecrease's quantity.
Equations
- One or more equations did not get rendered due to their size.
Instances For
P4/P8 measure prep (eq:properweighteddescent engine): a stratum's
measure is at most twice the cover-child measure (|J̃ ∩ L̃| ≤ 2·|L_B|).
P8-lite measure prep: the cover-child measure IS the xrChild measure
(count transport along the collapse).
Combined form for P8: stratum measure ≤ 2 · (xrChild measure).
The exit theorems (the keep's exact spelling; hR-free) #
lem:covertransform at the scalar cover, candidate source
(eq:covertransform l.3834–3840 at J = B): eight times the weak-lift count
m_{A,λ}(B) — the keep sec7_scalarCoverCountAgreement's LHS — is the sum of
the boundary-framed exact-image counts of the cover strata.
lem:covertransform at the scalar cover, local source: the mirror of
sec7_scalarCoverPartition_gammaA for G_{ℚ₂}; the uniform 8 is
cover_Z1_card_gq2, derived from the citable q2_localduality_general.
The keep, restated as a strata-sum agreement (the exact residue P8
must produce): m_{A,λ}(B) = m_{Q,λ}(B) iff the SAME source-independent list
of stratum framed pairs has equal A/Q-counts — which is exactly what the
engine's strong-induction IH supplies once the strata are children.