Documentation

GQ2.SourceData

The pluggable source interface: SourceData (the SourceData refactor, R30) #

The two-source assembly (thm_4_2, prop_8_9, prop_8_9_of) pins its candidate slot to Γ_A through the BoundaryMaps A-side fields and the _gammaA supply lemmas. This file extracts that slot into a single structure SourceData, so that a second presented source (the note's Γ_R) can be plugged in beside G_ℚ₂ with zero further refactoring: R32 builds sourceR : SourceData and instantiates thm_4_2_of_sources (GQ2/ThmFourTwo.lean).

Contents #

Import discipline #

This file must stay plain-import (non-module): it imports the §8 stack (Prop89Close and below), which is plain-import, and module-style files cannot import plain files (the R31a pitfall; precedent: GQ2/Roe/Prop23.lean, GQ2/Roe/Supply.lean).

Axioms: none introduced — every statement here is assembled from proved material; the axiom footprints of the consumers are unchanged (the R30 regression gate).

source
noncomputable def GQ2.sourceBoundaryMap {Γ : ProfiniteGrp.{u_1}} (tame : ↑Γ.toProfinite.toTop →ₜ* ↑Ttame.toProfinite.toTop) (pro2 : ↑Γ.toProfinite.toTop →ₜ* ↑PiBd.toProfinite.toTop) (compat : ∀ (g : ↑Γ.toProfinite.toTop), nuT (tame g) = nuTwo (pro2 g)) :
↑Γ.toProfinite.toTop →ₜ* ↥boundarySubgroup

The boundary map b_Γ : Γ → ∂bd of eq. (27), bundled from a tame/pro-2 pair with the Prop 3.14 ν-compatibility — the BoundaryMaps.bA construction, factored out so that SourceData fields can refer to the map determined by the structure's own fields. Definitionally equal to B.bA at (B.tameA, B.pro2A, B.compatA).

Equations
Instances For
    source
    structure GQ2.SourceData :
    Type 1

    The pluggable source (the SourceData refactor): everything the two-source assembly consumes about the candidate slot. Data fields = the eq. (27) boundary interface of a presented source (Prop 3.10 / Prop 3.14, pinned by generator values as for Γ_A), with ker_pro2 promoted to a field (the recon's 12 + 1; Γ_A derives it as SectionNine.ker_pro2A, Γ_R from its max-pro-2 identification). Prop fields = the seven supply-obligation families, each in the exact ∀-shape of its _gammaA witness, so BoundaryMaps.sourceA is assembled from the untouched lemmas and sourceR from R31's.

    Instances For
      source
      noncomputable def GQ2.SourceData.b (S : SourceData) :
      ↑S.Γ.toProfinite.toTop →ₜ* ↥boundarySubgroup

      The source's boundary map b_Γ : Γ → ∂bd (eq. (27)); at sourceA this is definitionally B.bA.

      Equations
      Instances For
        source
        @[simp]
        theorem GQ2.SourceData.b_apply_coe (S : SourceData) (g : ↑S.Γ.toProfinite.toTop) :
        ↑(S.b g) = (S.tame g, S.pro2 g)
        source
        theorem GQ2.SourceData.b_surjective (S : SourceData) :
        Function.Surjective ⇑S.b
        source
        theorem GQ2.SourceData.pro2_surjective (S : SourceData) :
        Function.Surjective ⇑S.pro2

        Surjectivity of the source's pro-2 coordinate, derived from the joint surjectivity surj (the terminal_count_eq hpro2A_surj derivation, source-generic).

        source
        noncomputable def GQ2.BoundaryMaps.sourceA (B : BoundaryMaps) :
        SourceData

        The Γ_A instance of the source interface: the BoundaryMaps A-side fields and the untouched _gammaA supply lemmas, assembled. (ker_pro2 is SectionNine.ker_pro2A, the derivation from the generator values + prop_3_10_gammaA; the scalar action is the global trivial instance of GQ2/RStage/GammaA.lean.)

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem GQ2.BoundaryMaps.sourceA_b (B : BoundaryMaps) :
          B.sourceA.b = B.bA

          The load-bearing definitional identity of the flip: sourceA's boundary map is B.bA (by rfl), so re-deriving the Γ_A capstones from the _of_sources forms changes no statement.

          source
          theorem GQ2.terminal_count_eq_of_sources {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] (S : SourceData) (B : BoundaryMaps) (F : BoundaryFrame H E) [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] (T : MarkedTarget H E Y) (hE2 : ∀ (e : E), e ^ 2 = 1) (hstack : SectionSeven.IsScalarStack T.LY) :
          exactImageCount S.b F T = exactImageCount B.bF F T

          The §9.1 terminal count over an abstract source (the SourceData refactor): SectionNine.terminal_count_eq with the candidate slot abstracted — the source enters only through b, pro2, surj and the promoted ker_pro2, via the source-generic bridges boundaryLifts_equiv_qlifts / qlifts_equiv_commonLifts at the (source-independent) Lemma 9.2 splitting datum.

          source
          theorem GQ2.gaussZ_obtain_blockD_of_sources {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [Blk.frattiniK.Normal] [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] [IsTopologicalGroup AbsGalQ2] (hE2 : ∀ (e : E), e ^ 2 = 1) (S : SourceData) (B : BoundaryMaps) (F : BoundaryFrame H E) (R : LocalReciprocity) (horient : TameUnitOrientation R B.tameF) (hsimple : ∀ (W : AddSubgroup (SectionNine.blockEnrichmentD T Blk hE2 F).Vmod), (∀ (g : (SectionNine.blockFrame T Blk hE2).YC), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) (hVne : ∃ (v : (SectionNine.blockEnrichmentD T Blk hE2 F).Vmod), v ≠ 0) (hnt : ∃ (g : (SectionNine.blockFrame T Blk hE2).YC) (v : (SectionNine.blockEnrichmentD T Blk hE2 F).Vmod), g • v ≠ v) :
          ∃ (G0 : ℤ), (∀ (l : (SectionNine.blockFrame T Blk hE2).DR) (h : l ≠ (SectionNine.blockFrame T Blk hE2).zeroDR), SectionEight.GaussZResidue S.b F (SectionNine.blockEnrichmentD T Blk hE2 F) l h G0) ∧ ∀ (l : (SectionNine.blockFrame T Blk hE2).DR) (h : l ≠ (SectionNine.blockFrame T Blk hE2).zeroDR), SectionEight.GaussZResidue B.bF F (SectionNine.blockEnrichmentD T Blk hE2 F) l h G0

          The shared-G0 obtain over an abstract source (the SourceData refactor, the recon's external-G0 seam): SectionNine.gaussZ_obtain_blockD replayed — the exponent m (from the nonsingular form, source-independent) and the head dichotomy (on F.alpha τ, source-independent) are decided once, and each source contributes exactly its dichotomy leaf at the resulting G0 = ∓2^m: the abstract slot through gaussZ_unramified/gaussZ_ramified, the G_ℚ₂ slot through the proved local twins.

          source
          theorem GQ2.prop_8_9_of_sources {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] (S : SourceData) (B : BoundaryMaps) {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (hE2 : ∀ (e : E), e ^ 2 = 1) (En : (blockFrameImpl T Blk hE2).Enrichment) (F : BoundaryFrame H E) [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] [IsTopologicalGroup AbsGalQ2] (hfgF : ∃ (s : Finset AbsGalQ2), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hheadS : Function.Surjective fun (γ : ↑S.Γ.toProfinite.toTop) => (F.frameMap (S.b γ)).1) (hheadF : Function.Surjective fun (γ : AbsGalQ2) => (F.frameMap (B.bF γ)).1) (hsimple : ∀ (W : AddSubgroup En.Vmod), (∀ (g : (blockFrameImpl T Blk hE2).YC), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤) (hVne : ∃ (v : En.Vmod), v ≠ 0) (hnt : ∃ (g : (blockFrameImpl T Blk hE2).YC) (v : En.Vmod), g • v ≠ v) (G0 : ℤ) (hGaussZS : ∀ (l : (blockFrameImpl T Blk hE2).DR) (h : l ≠ (blockFrameImpl T Blk hE2).zeroDR), SectionEight.GaussZResidue S.b F En l h G0) (hGaussZF : ∀ (l : (blockFrameImpl T Blk hE2).DR) (h : l ≠ (blockFrameImpl T Blk hE2).zeroDR), SectionEight.GaussZResidue B.bF F En l h G0) :
          ∃ (μ : ℕ) (G0' : ℤ) (DT : Type) (x : Fintype DT) (phase : (l : (blockFrameImpl T Blk hE2).DR) → l ≠ (blockFrameImpl T Blk hE2).zeroDR → DT → SectionEight.CentralCover (blockFrameImpl T Blk hE2).YC), 0 < Nat.card DT ∧ SectionEight.ClosedRecursion (blockFrameImpl T Blk hE2) S.b F μ G0' DT phase ∧ SectionEight.ClosedRecursion (blockFrameImpl T Blk hE2) B.bF F μ G0' DT phase

          Proposition 8.9 over a bundled source (the SourceData refactor): the recon's "prop_8_9 runs over a SourceData instance" form — SectionEight.prop_8_9_of_source fed from the structure's fields. R32 consumes this at sourceR; the Γ_A capstone SectionEight.prop_8_9 is (equivalently) the same statement at B.sourceA, re-derived in GQ2/Prop89Close.lean directly from the unbundled form.

          Paper-tag ledger (auto-generated by paperforge; do not edit) #