Assembly: levelwise nonemptiness → two epis → Hopfian → bLab (ticket L1/L5) #
Statements final (ticket L1); fills ticket L5 (including the serialized
GQ2/Reconstruction.lean refactor). Design record: docs/orchestration/ labute-l1-design.md; sources: labute-plan.md §2.1 (items 2–3), labute-spike.md §4.7.
The chain (plan §2.1, the "β-architecture" of the design memo — maximal reuse of the in-tree König machinery):
sPR0_nonempty/sPR2_nonempty: the levelwise sets are nonempty at every level — basek₀ = 3(Levelwise.lean) + the stage step (StageLemma.lean) upward + the restriction maps downward.nonempty_contSurj_levelQuot_*: for every open normalU, continuous surjections onto the finite quotient exist — the λ-tower is cofinal (exists_twoCentralSeries_le), a level-ktriple is a hom by the universal propertiesd0LiftHom/drLiftHom(triples ⟺ homs, plan §2.1), generation modλₖis surjectivity, and quotients compose.exists_contSurj_of_levelwise_nonempty: the generic König/Cantor assembly — the exact statement whose proof is lines 224–309 ofexists_contSurj_of_card_le(GQ2/Reconstruction.lean:213) with the twohaveI-inputs promoted to hypotheses. L5 protocol (byte-identical-consumers gate), executed: the statement now lives inReconstruction.leanasGQ2.exists_contSurj_of_levelwise_nonempty(module file, mathlib-only imports),exists_contSurj_of_card_leis re-derived from it throughcontSurj_quotient_nonempty_finite, andreconstruction/reconstruction_of_equinumand every consumer are unchanged — verified byte-identically, statements and#print axioms. The Labute-namespaced form below is the frozen consumer-facing statement and is a one-line application of the Reconstruction-side lemma.bLab : BLabHypothesis— proved below (not sorried): the two epis + the profinite Hopfian endgame, byte-for-byte the endgame ofreconstruction_of_equinum(GQ2/Reconstruction.lean:319). The four antecedents ofBLabHypothesisare discarded: the pinned χ-data enters the proof through the levelwise sets (chiR,chiD0pres, tickets R10/R11), not through the abstract hypotheses — plan §1 ("conveniences, not gates").
Census note (plan §8): this file imports GQ2/Roe/MarkedPro2.lean solely for the
statement BLabHypothesis; the proof chain (towers, levelwise sets, Reconstruction,
dr_topGen/topGen_d0) is axiom-file-free, and #print axioms bLab reports
[propext, Classical.choice, Quot.sound] — std-3 exactly, zero census axioms, no
sorryAx (measured at L5, with the whole L-campaign fill chain in place).
The χ-intertwining bonus of spike §2.4 (the limit epi can be taken χ-compatible) is
deliberately not frozen — no bLab-consumer needs it; the design memo records the
α-architecture sketch for R15 should it ever be wanted.
Topological finite generation, Finset-packaged #
The Finset forms consumed by profinite_hopfian and finite_continuousMonoidHom
(GQ2/Reconstruction.lean:76,56), discharged from the in-tree generator facts.
D_R is topologically generated by the finite set {s, x, y} (packaging of
dr_topGen, GQ2/Roe/DRAbelianization.lean:132; smoke).
D₀ is topologically generated by the finite set {A, S, Y} (packaging of
topGen_d0, GQ2/DyadicNielsen.lean:47; smoke).
The generic König/Cantor assembly (the L5 Reconstruction.lean refactor target) #
Surjection assembly from levelwise nonemptiness (plan §2.1 item 2): if S
continuously surjects onto every finite quotient of R in at least one and at most
finitely many ways, then S continuously surjects onto R.
This is exists_contSurj_of_card_le (GQ2/Reconstruction.lean:213) with the
konigFunctor-level inputs (hne, hfin) taken as hypotheses instead of being derived
from surjection counts; its proof is lines 224–309 of that lemma verbatim. Fill: L5,
by the serialized Reconstruction.lean refactor described in the module docstring
(byte-identical-consumers regression gate).
Finiteness of the level sets from topological finite generation of the source
(the hfin-supplier; the reconstruction_of_equinum pattern, Reconstruction.lean:330;
smoke).
Levelwise nonemptiness at every level #
Levelwise nonemptiness, direction 1 (the mathematical core, assembled): S^P_ₖ is
nonempty for every k — upward from the base sPR0_three_nonempty by stageStepR0,
downward from level 3 by the restrictions sPR0_levelProj. Fill: L5 (pure induction;
all inputs frozen).
Levelwise nonemptiness, direction 2. Fill: L5.
From levelwise triples to surjections onto all finite quotients #
The cofinality bridge, direction 1: D₀ continuously surjects onto every finite
quotient of D_R. Route (plan §2.1): U contains some λₖ (exists_twoCentralSeries_le
with drFinsetTopGen, isProP_DR), a triple T ∈ S⁰ₖ is a continuous hom
D₀ → Qₖ(D_R) by d0LiftHom (at the finite 2-group Qₖ), generation makes it
surjective, and composing with Qₖ(D_R) ↠ D_R/U finishes. Fill: L5.
The cofinality bridge, direction 2: D_R continuously surjects onto every finite
quotient of D₀ (via drLiftHom at S⁰ₖ-triples of the D₀-tower). Fill: L5.
The two epis and the Hopfian endgame #
The continuous epi φ : D₀ ↠ D_R (assembled; not a fill target — this composition is
part of the L1 elaboration certificate).
The continuous epi ψ : D_R ↠ D₀ (assembled; not a fill target).
The B-Lab classification instance, as a theorem — the L-campaign deliverable
(plan §1: the exact interface of GQ2/Roe/MarkedPro2.lean section Draft, verbatim).
The proof is complete here modulo the upstream skeleton sorries: the four antecedents
are discarded (the pinned orientation data enters through the levelwise χ-clauses instead
— plan §1), the two epis come from the levelwise assembly above, and the endgame is
byte-for-byte the reconstruction_of_equinum endgame (GQ2/Reconstruction.lean:350–354):
φ ∘ ψ : D_R ↠ D_R is a continuous surjective endomorphism of a topologically f.g.
profinite group, hence injective (profinite_hopfian), so ψ is a continuous bijective
homomorphism, so a topological isomorphism (continuousMulEquivOfBijective).