The norm-bounded trade (finiteness-and-chi, gated file 1/3)

Unit: finiteness-and-chi (docs/design/finiteness-and-chi.md §4.4, §4.5, proof plan §5, §6.3 step 5). This is the first of the three files that were blocked on the cech Colimit/Window/ Skyscraper gate and dolbeault's Leray.lean gate — both are now open.

• isCompactOperator_resZ_UV/isCompactOperator_tradeCompact (§4.4, still owed from Chain.lean/CompactRestrict.lean): the finite-Pi assembly of Montel compactness into the cocycle-level U → V restriction and the tradeCompact Schwartz leg.
• toGermZ1/boundZ1: the Banach ↔ Čech germ bridges at a fixed level (D5).
• tradePi_surjective (Forster 14.6(a) upgraded to the Banach layer): the trade projection is onto — the Schwartz surjectivity input.
• classMap/classMap_tradeDiff_eq_zero/classMap_surjective: the Čech class map and its two Schwartz-consumer properties.

§4.4: the compact-operator assembly (owed from Chain.lean/CompactRestrict.lean)

theorem RS.Finiteness.isCompactOperator_pi {ι : Type u_2} [Finite ι] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : ι → Type u_4} [(i : ι) → NormedAddCommGroup (F i)] [(i : ι) → NormedSpace ℂ (F i)] (f : (i : ι) → E →L[ℂ] F i) (hf : ∀ (i : ι), IsCompactOperator ⇑(f i)) : IsCompactOperator ⇑(ContinuousLinearMap.pi f)

A finite Pi of compact operators (all sharing the same domain) is a compact operator.

theorem RS.Finiteness.resZ_apply_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) {P P' : Fin T.n → TopologicalSpace.Opens X} (h : ∀ (i : Fin T.n), P' i ≤ P i) (x : ↥(NZ1 T P)) : ↑((resZ T P P' h) x) = (resNC1 T P P' h) ↑x

theorem RS.Finiteness.isCompactOperator_resNC1_U_V {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] (T : ShrinkChain X) : IsCompactOperator ⇑(resNC1 T T.U T.V ⋯)

theorem RS.Finiteness.isCompactOperator_resZ_UV {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] (T : ShrinkChain X) : IsCompactOperator ⇑(resZ T T.U T.V ⋯)

§4.4: the finite-Pi Montel assembly of the cocycle-level U → V restriction.

theorem RS.Finiteness.isCompactOperator_tradeCompact {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] (T : ShrinkChain X) : IsCompactOperator ⇑(tradeCompact T)

§4.4: the Montel-compact leg of the Schwartz cospan.

Compat: evalAt arithmetic missing from Meromorphic/OrderEval.lean

theorem RS.Finiteness.MeroGermOn.evalAt_neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {U : Set X} (hU : IsOpen U) {x : X} (hx : x ∈ U) {φ : MeroGermOn X U} (h : 0 ≤ φ.ord x) : (-φ).evalAt x = -φ.evalAt x

theorem RS.Finiteness.MeroGermOn.evalAt_sub {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {U : Set X} (hU : IsOpen U) {x : X} (hx : x ∈ U) {φ ψ : MeroGermOn X U} (h1 : 0 ≤ φ.ord x) (h2 : 0 ≤ ψ.ord x) : (φ - ψ).evalAt x = φ.evalAt x - ψ.evalAt x

theorem RS.Finiteness.MeroGermOn.evalAt_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {U : Set X} (hU : IsOpen U) {x : X} (hx : x ∈ U) : MeroGermOn.evalAt 0 x = 0

theorem RS.Finiteness.LinSysOn.ord_nonneg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} (hU : IsOpen U) {x : X} (hx : x ∈ U) (φ : ↥(LinSysOn 0 U)) : 0 ≤ (↑φ).ord x

LinSysOn 0-membership gives 0 ≤ ord unconditionally (D=0's own zero divisor).

theorem RS.Finiteness.Z1.rel_res_evalAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {𝒰 : Cech.FinCover ⊤} {f : Cech.C1 0 𝒰} (hf : f ∈ Cech.Z1 0 𝒰) (a b c : Fin 𝒰.n) {z : X} (hbc : z ∈ 𝒰.U b ⊓ 𝒰.U c) (hac : z ∈ 𝒰.U a ⊓ 𝒰.U c) (hab : z ∈ 𝒰.U a ⊓ 𝒰.U b) : (↑(f (b, c))).evalAt z - (↑(f (a, c))).evalAt z + (↑(f (a, b))).evalAt z = 0

The "repr_cocycle" pattern (dolbeault §6.2): a Z1-cocycle relation, evaluated pointwise.

§5: the germ ↔ Banach bridges at a cover level (D5)

noncomputable def RS.Finiteness.toGermSub {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (S : TopologicalSpace.Opens X) : ↥(BddHoloOn S) →ₗ[ℂ] ↥(LinSysOn 0 ↑S)

Germification into the LinSysOn 0 submodule (D5, bundled linear form of toGerm).

Equations

• RS.Finiteness.toGermSub S = LinearMap.codRestrict (RS.LinSysOn 0 ↑S) (RS.Finiteness.toGerm S) ⋯

theorem RS.Finiteness.toGermSub_apply_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (S : TopologicalSpace.Opens X) (f : ↥(BddHoloOn S)) : ↑((toGermSub S) f) = (toGerm S) f

theorem RS.Finiteness.toGermSub_restrictCLM_comm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {S' S : TopologicalSpace.Opens X} (h : S' ≤ S) (f : ↥(BddHoloOn S)) : (toGermSub S') ((restrictCLM h) f) = (Cech.LinSysOn.restrictL 0 h) ((toGermSub S) f)

@[reducible]

noncomputable def RS.Finiteness.coverOfP {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) (hcov : ∀ (x : X), ∃ (i : Fin T.n), x ∈ P i) : Cech.FinCover ⊤

The FinCover (⊤ : Opens X) induced by a ShrinkChain-indexed family P (generic form of T.coverU/T.coverV/T.coverW; kept separate from those concrete defs so that this section's lemmas typecheck for a bare P : Fin T.n → Opens X without needing 𝒰.n to be syntactically T.n — a genuine dependent-type obstruction for a free 𝒰 : FinCover (⊤ : Opens X) variable). T.coverU/T.coverV/T.coverW are rfl-equal to coverOfP T.U T.covers_U etc. (same fields, Prop-irrelevant covers witness), so this is used transparently at call sites.

Equations

• RS.Finiteness.coverOfP T P hcov = { n := T.n, U := P, le_base := ⋯, covers := ⋯ }

noncomputable def RS.Finiteness.toGermC1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) : NC1 T P →ₗ[ℂ] (p : Fin T.n × Fin T.n) → ↥(LinSysOn 0 ↑(P p.1 ⊓ P p.2))

Germification of a P-indexed 1-cochain of BddHoloOns (§5 step 3).

Equations

• RS.Finiteness.toGermC1 T P = LinearMap.pi fun (p : Fin T.n × Fin T.n) => RS.Finiteness.toGermSub (P p.1 ⊓ P p.2) ∘ₗ LinearMap.proj p

theorem RS.Finiteness.toGermC1_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) (f : NC1 T P) (p : Fin T.n × Fin T.n) : (toGermC1 T P) f p = (toGermSub (P p.1 ⊓ P p.2)) (f p)

theorem RS.Finiteness.toGermC1_mem_Z1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) (hcov : ∀ (x : X), ∃ (i : Fin T.n), x ∈ P i) {f : NC1 T P} (hf : f ∈ NZ1 T P) : (toGermC1 T P) f ∈ Cech.Z1 0 (coverOfP T P hcov)

noncomputable def RS.Finiteness.toGermZ1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) (hcov : ∀ (x : X), ∃ (i : Fin T.n), x ∈ P i) : ↥(NZ1 T P) →ₗ[ℂ] ↥(Cech.Z1 0 (coverOfP T P hcov))

Germification of bounded cocycles into Z1 0 (coverOfP T P hcov), bundled linear (§5 step 3).

Equations

• RS.Finiteness.toGermZ1 T P hcov = LinearMap.codRestrict (RS.Cech.Z1 0 (RS.Finiteness.coverOfP T P hcov)) (RS.Finiteness.toGermC1 T P ∘ₗ (RS.Finiteness.NZ1 T P).subtype) ⋯

theorem RS.Finiteness.toGermZ1_apply_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) (hcov : ∀ (x : X), ∃ (i : Fin T.n), x ∈ P i) (ξ : ↥(NZ1 T P)) : ↑((toGermZ1 T P hcov) ξ) = (toGermC1 T P) ↑ξ

noncomputable def RS.Finiteness.boundZ1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) [CompactSpace X] {P : Fin T.n → TopologicalSpace.Opens X} (h : ∀ (i : Fin T.n), closure ↑(P i) ⊆ ↑(T.Ustar i)) (F : ↥(Cech.Z1 0 T.coverStar)) : NC1 T P

De-germification of a good-cover cocycle down onto a ⋐-nested level (§5 step 5).

Equations

• RS.Finiteness.boundZ1 T h F p = RS.Finiteness.restrictGerm ⋯ (↑F (p.1, p.2))

noncomputable def RS.Finiteness.starPairMem {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) (F : ↥(Cech.Z1 0 T.coverStar)) (i j : Fin T.n) : ↥(LinSysOn 0 ↑(T.Ustar i ⊓ T.Ustar j))

The (i, j)-component of a good-cover cocycle, as a LinSysOn-membership term (a named helper: writing the LinSysOn-then-MeroGermOn coercion inline as a single doubly-nested type ascription hits a hard isDefEq rejection — T.coverStar.U i ⊓ T.coverStar.U j vs T.Ustar i ⊓ T.Ustar j — that a two-step named unfolding avoids entirely; see the build log for the diagnosis).

Equations

• RS.Finiteness.starPairMem T F i j = ↑F (i, j)

noncomputable def RS.Finiteness.starPairGerm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) (F : ↥(Cech.Z1 0 T.coverStar)) (i j : Fin T.n) : MeroGermOn X ↑(T.Ustar i ⊓ T.Ustar j)

The (i, j) component of a coverStar-level cocycle, as a germ.

Equations

• RS.Finiteness.starPairGerm T F i j = ↑(RS.Finiteness.starPairMem T F i j)

theorem RS.Finiteness.boundZ1_apply_eq_evalAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) [CompactSpace X] {P : Fin T.n → TopologicalSpace.Opens X} (h : ∀ (i : Fin T.n), closure ↑(P i) ⊆ ↑(T.Ustar i)) (F : ↥(Cech.Z1 0 T.coverStar)) (i j : Fin T.n) (z : ↑↑(P i ⊓ P j)) : ↑(boundZ1 T h F (i, j)) z = (starPairGerm T F i j).evalAt ↑z

theorem RS.Finiteness.boundZ1_mem_NZ1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) [CompactSpace X] {P : Fin T.n → TopologicalSpace.Opens X} (h : ∀ (i : Fin T.n), closure ↑(P i) ⊆ ↑(T.Ustar i)) (F : ↥(Cech.Z1 0 T.coverStar)) : boundZ1 T h F ∈ NZ1 T P

§5 step 5's NZ1-membership: the de-germified cochain is a genuine bounded cocycle (the "repr_cocycle" pattern: evaluate F's germ cocycle relation pointwise).

noncomputable def RS.Finiteness.boundZ1C0 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) [CompactSpace X] (g : Cech.C0 0 T.coverV) : NC0 T T.W

De-germification of a 0-cochain down onto the W-level (§5 step 5, second half).

Equations

• RS.Finiteness.boundZ1C0 T g i = RS.Finiteness.restrictGerm ⋯ (g i)

noncomputable def RS.Finiteness.vMem {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) (g : Cech.C0 0 T.coverV) (i : Fin T.n) : ↥(LinSysOn 0 ↑(T.V i))

The i-component of a T.coverV-level 0-cochain, as a LinSysOn-membership term (same two-step naming device as starPairMem/starPairGerm).

Equations

• RS.Finiteness.vMem T g i = g i

noncomputable def RS.Finiteness.vGerm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) (g : Cech.C0 0 T.coverV) (i : Fin T.n) : MeroGermOn X ↑(T.V i)

The i-th component of a coverV-level cochain, as a germ.

Equations

• RS.Finiteness.vGerm T g i = ↑(RS.Finiteness.vMem T g i)

theorem RS.Finiteness.boundZ1C0_apply_eq_evalAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) [CompactSpace X] (g : Cech.C0 0 T.coverV) (i : Fin T.n) (z : ↑↑(T.W i)) : ↑(boundZ1C0 T g i) z = (vGerm T g i).evalAt ↑z

theorem RS.Finiteness.trade_evalAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) {𝒱 : Cech.FinCover ⊤} {τ : Fin 𝒱.n → Fin T.n} (hτ : Cech.IsRefIdx T.coverStar 𝒱 τ) (F : ↥(Cech.Z1 0 T.coverStar)) (f : Cech.C1 0 𝒱) (g : Cech.C0 0 𝒱) (hFg : ↑((Cech.resZ1 0 τ hτ) F) = f + (Cech.d0 0 𝒱) g) (α β : Fin 𝒱.n) {z : X} (hz : z ∈ 𝒱.U α ⊓ 𝒱.U β) : (starPairGerm T F (τ α) (τ β)).evalAt z = (↑(f (α, β))).evalAt z + ((↑(g β)).evalAt z - (↑(g α)).evalAt z)

The trade equation, evaluated pointwise (the "repr_cocycle" pattern applied to exists_trade's conclusion): reads off a scalar identity relating the good-cover cocycle F, the traded cocycle f, and the coboundary witness g at a point. Reused for both tradePi_surjective (§5 steps 5–6, at level V) and classMap_surjective (§5 step 9, at level W).

§5 steps 4–6: tradePi_surjective (the qualitative trade, Banach layer)

noncomputable def RS.Finiteness.cC1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (ξ : ↥(NZ1 T T.V)) : Cech.C1 0 T.coverV

The germified V-level cocycle c viewed at T.coverV directly (same two-step naming device as starPairMem/starPairGerm, needed since coverOfP T T.V T.covers_V and T.coverV are rfl-equal but the coercion chain Z1 → C1 → (ascribe) cannot be nested inline).

Equations

• RS.Finiteness.cC1 T ξ = ↑((RS.Finiteness.toGermZ1 T T.V ⋯) ξ)

noncomputable def RS.Finiteness.cCompMem {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (ξ : ↥(NZ1 T T.V)) (α β : Fin T.n) : ↥(LinSysOn 0 ↑(T.V α ⊓ T.V β))

Membership witness for the (α, β) component of a norm-bounded cocycle.

Equations

• RS.Finiteness.cCompMem T ξ α β = RS.Finiteness.cC1 T ξ (α, β)

noncomputable def RS.Finiteness.cComp {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (ξ : ↥(NZ1 T T.V)) (α β : Fin T.n) : MeroGermOn X ↑(T.V α ⊓ T.V β)

The (α, β) component of a norm-bounded cocycle, as a LinSysOn element.

Equations

• RS.Finiteness.cComp T ξ α β = ↑(RS.Finiteness.cCompMem T ξ α β)

theorem RS.Finiteness.cComp_eq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (ξ : ↥(NZ1 T T.V)) (α β : Fin T.n) : cComp T ξ α β = (toGerm (T.V α ⊓ T.V β)) (↑ξ (α, β))

theorem RS.Finiteness.tradePi_surjective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] (T : ShrinkChain X) : Function.Surjective ⇑(tradePi T)

§5's centerpiece: the trade projection π : L →L Z¹(𝔙) is onto (Forster 14.6(a) upgraded to the Banach layer).

§5 steps 8–9: classMap and the two Schwartz-consumer properties

theorem RS.Finiteness.resZ_resZ {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) {P P' P'' : Fin T.n → TopologicalSpace.Opens X} (h1 : ∀ (i : Fin T.n), P' i ≤ P i) (h2 : ∀ (i : Fin T.n), P'' i ≤ P' i) (h3 : ∀ (i : Fin T.n), P'' i ≤ P i) (x : ↥(NZ1 T P)) : (resZ T P' P'' h2) ((resZ T P P' h1) x) = (resZ T P P'' h3) x

Composition law for the Banach-level restriction (mirrors resZ1_comp/resC1_comp).

noncomputable def RS.Finiteness.toGermC0 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) : NC0 T P →ₗ[ℂ] (i : Fin T.n) → ↥(LinSysOn 0 ↑(P i))

Germification of a P-indexed 0-cochain (needed for classMap's coboundary witness).

Equations

• RS.Finiteness.toGermC0 T P = LinearMap.pi fun (i : Fin T.n) => RS.Finiteness.toGermSub (P i) ∘ₗ LinearMap.proj i

theorem RS.Finiteness.toGermC0_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (P : Fin T.n → TopologicalSpace.Opens X) (h : NC0 T P) (i : Fin T.n) : (toGermC0 T P) h i = (toGermSub (P i)) (h i)

theorem RS.Finiteness.toGermC1_deltaCLM_eq_d0 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (η : NC0 T T.W) (p : Fin T.n × Fin T.n) : (toGermC1 T T.W) ((deltaCLM T T.W) η) p = (Cech.d0 0 T.coverW) ((toGermC0 T T.W) η) p

Naturality: germifying a 0-cochain then taking its cover-level coboundary agrees with germifying the Banach-level coboundary (§5 step 8's "toGermZ1 ∘ δ_W = d0 ∘ toGermC0").

noncomputable def RS.Finiteness.toGermZ1W {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (ψ : ↥(NZ1 T T.W)) : ↥(Cech.Z1 0 T.coverW)

The toGermZ1-image of a T.W-level bounded cocycle, viewed at T.coverW directly (same two-step naming device as cC1).

Equations

• RS.Finiteness.toGermZ1W T ψ = (RS.Finiteness.toGermZ1 T T.W ⋯) ψ

theorem RS.Finiteness.toGermZ1W_apply_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (ψ : ↥(NZ1 T T.W)) : ↑(toGermZ1W T ψ) = (toGermC1 T T.W) ↑ψ

noncomputable def RS.Finiteness.classMap {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) : ↥(NZ1 T T.V) →ₗ[ℂ] Cech.H1Cover 0 T.coverW

The Čech class map (§5 step 8): bound V-level cocycles down to W, germify, take the Mittag-Leffler class.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.Finiteness.classMap_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (ψ : ↥(NZ1 T T.V)) : (classMap T) ψ = (Cech.H1Cover.mk 0 T.coverW) (toGermZ1W T ((resZ T T.V T.W ⋯) ψ))

theorem RS.Finiteness.classMap_tradeDiff_eq_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (T : ShrinkChain X) (x : ↥(tradeSpace T)) : (classMap T) ((tradePi T) x - (tradeCompact T) x) = 0

Schwartz-consumer property 1 (§5 step 8): the trade defect dies in H¹(𝔚).

theorem RS.Finiteness.resZ_boundZ1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] (T : ShrinkChain X) {P P' : Fin T.n → TopologicalSpace.Opens X} (h : ∀ (i : Fin T.n), closure ↑(P i) ⊆ ↑(T.Ustar i)) (h' : ∀ (i : Fin T.n), P' i ≤ P i) (h2 : ∀ (i : Fin T.n), closure ↑(P' i) ⊆ ↑(T.Ustar i)) (F : ↥(Cech.Z1 0 T.coverStar)) : (resZ T P P' h') ⟨boundZ1 T h F, ⋯⟩ = ⟨boundZ1 T h2 F, ⋯⟩

Restriction commutes with boundZ1 (Banach-level restriction of a de-germified good-cover cocycle equals de-germifying with the transitively-composed closure hypothesis).

noncomputable def RS.Finiteness.wPairMem {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) (c : ↥(Cech.Z1 0 T.coverW)) (i j : Fin T.n) : ↥(LinSysOn 0 ↑(T.W i ⊓ T.W j))

The (i, j)-component of a T.coverW-level Z1 element, as a LinSysOn-membership term (same two-step naming device as starPairMem/starPairGerm).

Equations

• RS.Finiteness.wPairMem T c i j = ↑c (i, j)

noncomputable def RS.Finiteness.wPairGerm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (T : ShrinkChain X) (c : ↥(Cech.Z1 0 T.coverW)) (i j : Fin T.n) : MeroGermOn X ↑(T.W i ⊓ T.W j)

The (i, j) component of a coverW-level cocycle, as a germ.

Equations

• RS.Finiteness.wPairGerm T c i j = ↑(RS.Finiteness.wPairMem T c i j)

theorem RS.Finiteness.toGermZ1W_boundZ1 {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] (T : ShrinkChain X) (h : ∀ (i : Fin T.n), closure ↑(T.W i) ⊆ ↑(T.Ustar i)) (F : ↥(Cech.Z1 0 T.coverStar)) : ↑(toGermZ1W T ⟨boundZ1 T h F, ⋯⟩) = ↑((Cech.resZ1 0 id ⋯) F)

The germ roundtrip: germifying the T.W-level de-germified F recovers F's own germ restriction down to T.coverW (resZ1 0 id T.ref_star_W F).

theorem RS.Finiteness.classMap_surjective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] (T : ShrinkChain X) : Function.Surjective ⇑(classMap T)

§5's second centerpiece: classMap is surjective (§5 step 9).