Theorem 1.2, literal presentation form #
main_presentation_literal : Nonempty (ContinuousMulEquiv GammaA AbsGalQ2) — the literal
Theorem 1.2 — as the instantiation of Statement.main_presentation at the honest candidate Γ_A
(GQ2/GammaA.lean, paper eq. (7)).
Why here, not in GammaA.lean. The proof supplies main_presentation's two count hypotheses:
hΓA := prop_2_3 (Prop. 2.3, Nat.card (ContSurj Γ_A G) = admissibleCount G) and
hcount := SectionTen.main_surjection_count' (Theorem 1.2's surjection count for G_{ℚ₂},
eq. (154) + Prop. 2.3). Prop23 and SectionTenSources sit downstream of the upstream
GammaA.lean, so an in-place proof would create an import cycle;
GammaA.lean carries a comment-pointer here.
Axioms. Std-3 + the nine census axioms of GQ2/Foundations/Axioms.lean (B1, B3c, B5–B11a),
entering via main_surjection_count' / the boundary construction and B1 (topological finite
generation of G_{ℚ₂}).
Theorem 1.2 (literal presentation form): the honest candidate Γ_A is continuously
isomorphic to G_{ℚ₂}. Instantiates main_presentation at Γ_A: hΓA := prop_2_3 (the Γ_A
admissible-marking count), hcount := SectionTen.main_surjection_count' (the G_{ℚ₂} surjection
count), and the topological finite-generation witnesses of Γ_A and G_{ℚ₂}.
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- eq. (154) = ⟦eq-app-cup-convention⟧ [≥ drift window; verify against v428 tex]
- eq. (7) = ⟦eq-candidateinverse⟧
- Prop 2.3 = ⟦prop-epi-semantics⟧
- Theorem 1.2 = ⟦thm-main⟧