5. The common tamepro-2 boundary and the global induction🔗

Theorem5.1

uses 0used by 1✓L∃∀N

Theorem 4.2 of the paper (Boundary-framed exact-image theorem).

For every boundary-framed marked target \mathcal Y,

e_{\GA}^\beta(\mathcal Y)=e_{\GQ}^\beta(\mathcal Y).

The same equality holds for every exact-image target \mathcal J defined above.

Lean code for Theorem5.1●2 theorems

theoremdefined in GQ2/ThmFourTwo.lean

complete

theorem GQ2.thm_4_2 {H E : Type} [Group H] [TopologicalSpace H]
  [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E]
  [DiscreteTopology E] [Finite E] (B : GQ2.BoundaryMaps)
  (F : GQ2.BoundaryFrame H E) (R : GQ2.LocalReciprocity)
  (horient : GQ2.TameUnitOrientation R B.tameF)
  [CompactSpace GQ2.AbsGalQ2] [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y]
  [Finite Y] (T : GQ2.MarkedTarget H E Y) (hE2 : ∀ (e : E), e ^ 2 = 1) :
  GQ2.exactImageCount B.bA F T = GQ2.exactImageCount B.bF F T

theorem GQ2.thm_4_2 {H E : Type} [Group H]
  [TopologicalSpace H]
  [DiscreteTopology H] [Finite H]
  [CommGroup E] [TopologicalSpace E]
  [DiscreteTopology E] [Finite E]
  (B : GQ2.BoundaryMaps)
  (F : GQ2.BoundaryFrame H E)
  (R : GQ2.LocalReciprocity)
  (horient :
    GQ2.TameUnitOrientation R B.tameF)
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  {Y : Type} [Group Y]
  [TopologicalSpace Y]
  [DiscreteTopology Y] [Finite Y]
  (T : GQ2.MarkedTarget H E Y)
  (hE2 : ∀ (e : E), e ^ 2 = 1) :
  GQ2.exactImageCount B.bA F T =
    GQ2.exactImageCount B.bF F T

**Theorem 4.2 (boundary-framed exact-image theorem).**  For every boundary frame and
every boundary-framed marked target `𝒴`, the exact-image lift counts from the two sources
agree: `e^β_{Γ_A}(𝒴) = e^β_{G_ℚ₂}(𝒴)`.

Stated for any `BoundaryMaps` witness of the Prop 3.14 data (the choice is fixed "once and
for all" in §4 and only its bundled properties are used).

**Encoding correction** (documented in `docs/section9-extraction.md`): the hypothesis
`(hE2 : ∀ e : E, e ^ 2 = 1)` is required because the §9 induction descends the θ-decoration
through the block via `lemma_7_3`, whose (paper-stated)
hypothesis is that the decoration target is elementary abelian 2; the terminal case kills
the odd complement through `θ` for the same reason.  §10 consumes the theorem at `E = 0`
only, so the correction is downstream-harmless.  The theorem lives here because its proof
needs §§5–9 machinery, including `blockEnrichment` and
`prop_8_9`, both downstream of `SectionNine`; see the module docstring.

**Instance binders**: the two `AbsGalQ2` topology hypotheses mirror
`terminal_count_eq`'s (the `Half139Local`/`BoundaryMapsWitness` tower discipline — they are
deliberately not global instances); the consumer `eq_154` already carries exactly
these two.  The remaining topology instances the inductive lanes need (`GammaA`'s
compact/t.d./topological-group triple, `IsTopologicalGroup AbsGalQ2`) are globally inferable
(`GammaA : ProfiniteGrp`; mathlib's Krull-topology instance), so they are *not* binders.

The proof combines the induction scaffold, terminal lane, `M`-stage lane, and the `R`-stage lane
assembled against `prop_8_9` in `GQ2/Prop89Close.lean`.
Axioms B1/B3c/B6/B7/B8/B9 enter through the ingredients, per App. D (B7′, the dyadic Hilbert
symbol, is now an in-repo theorem, not an axiom).

theoremdefined in GQ2/ThmFourTwo.lean

complete

theorem GQ2.thm_4_2_stratum {H E : Type} [Group H] [TopologicalSpace H]
  [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E]
  [DiscreteTopology E] [Finite E] (B : GQ2.BoundaryMaps)
  (F : GQ2.BoundaryFrame H E) (R : GQ2.LocalReciprocity)
  (horient : GQ2.TameUnitOrientation R B.tameF)
  [CompactSpace GQ2.AbsGalQ2] [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y]
  [Finite Y] (T : GQ2.MarkedTarget H E Y) (hE2 : ∀ (e : E), e ^ 2 = 1)
  (J : Subgroup Y) (hJ : Function.Surjective ⇑(T.piY.comp J.subtype)) :
  GQ2.exactImageCount B.bA F (T.stratum J hJ) =
    GQ2.exactImageCount B.bF F (T.stratum J hJ)

theorem GQ2.thm_4_2_stratum {H E : Type} [Group H]
  [TopologicalSpace H]
  [DiscreteTopology H] [Finite H]
  [CommGroup E] [TopologicalSpace E]
  [DiscreteTopology E] [Finite E]
  (B : GQ2.BoundaryMaps)
  (F : GQ2.BoundaryFrame H E)
  (R : GQ2.LocalReciprocity)
  (horient :
    GQ2.TameUnitOrientation R B.tameF)
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  {Y : Type} [Group Y]
  [TopologicalSpace Y]
  [DiscreteTopology Y] [Finite Y]
  (T : GQ2.MarkedTarget H E Y)
  (hE2 : ∀ (e : E), e ^ 2 = 1)
  (J : Subgroup Y)
  (hJ :
    Function.Surjective
      ⇑(T.piY.comp J.subtype)) :
  GQ2.exactImageCount B.bA F
      (T.stratum J hJ) =
    GQ2.exactImageCount B.bF F
      (T.stratum J hJ)

Theorem 4.2's second clause: "the same equality holds for every exact-image target `𝒥`"
— an *instance* of the first (strata are ordinary objects of the same category), recorded to
fix the consumption shape for §8.  [Relocated with `thm_4_2`; carries the same `hE2`.]

Proof for Theorem 5.1

Proof uses 2

Proof dependency previews

Preview

Proposition 4.8

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

Proved in §4 of the paper. Ingredients: Lemma 10.2 Proposition 4.8.