Descendant--ancestor comparison

Mathematically, stable-map and stable-curve cotangent classes differ on loci contracted by stabilization. The current interface records only their residual difference. It does not encode support on boundary strata, factorization, or a derivation from a stabilization morphism.

structure AxiomaticGW.DescendantAncestorComparison {R V B : Type u} [CommRing R] [Algebra ℚ R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] [AddCancelCommMonoid B] {D : EffectiveCurveMonoid B} {C : StableCurveCohomology R} {Omega : GromovWittenTheory R V B D C} (P : PsiClasses C) (M : StableMapDescendants Omega) : Type (max 1 u)

A residual decomposition comparing stabilized stable-map descendants with stable-curve ancestors. This structure alone does not certify that the residual is geometrically boundary-supported.

• boundaryCorrection (g : ℕ) (S : Type) [Fintype S] (_h : StableArity g S) : B → (S → ℕ) → MultilinearMap R (fun (x : S) => V) (C.H g S).carrier

  Residual difference. The field name is retained for API compatibility; no boundary-support property is part of its type.

• comparison (g : ℕ) (S : Type) [Fintype S] (h : StableArity g S) (beta : B) (k : S → ℕ) : M.descendantClass g S h beta k = Omega.ancestorClass P g S h beta k + self.boundaryCorrection g S h beta k

  Stable-map descendants equal ancestors plus the recorded residual.

theorem AxiomaticGW.DescendantAncestorComparison.boundaryCorrection_eq_sub {R V B : Type u} [CommRing R] [Algebra ℚ R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] [AddCancelCommMonoid B] {D : EffectiveCurveMonoid B} {C : StableCurveCohomology R} {Omega : GromovWittenTheory R V B D C} {P : PsiClasses C} {M : StableMapDescendants Omega} (X : DescendantAncestorComparison P M) (g : ℕ) (S : Type) [Fintype S] (h : StableArity g S) (beta : B) (k : S → ℕ) : X.boundaryCorrection g S h beta k = M.descendantClass g S h beta k - Omega.ancestorClass P g S h beta k

The recorded residual is uniquely the descendant class minus the ancestor class. This makes explicit that the weak comparison structure alone carries no additional boundary-support information.

theorem AxiomaticGW.DescendantAncestorComparison.boundaryCorrection_zero {R V B : Type u} [CommRing R] [Algebra ℚ R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] [AddCancelCommMonoid B] {D : EffectiveCurveMonoid B} {C : StableCurveCohomology R} {Omega : GromovWittenTheory R V B D C} {P : PsiClasses C} {M : StableMapDescendants Omega} (X : DescendantAncestorComparison P M) (g : ℕ) (S : Type) [Fintype S] (h : StableArity g S) (beta : B) : (X.boundaryCorrection g S h beta fun (x : S) => 0) = 0

The residual vanishes when every cotangent power is zero.

theorem AxiomaticGW.DescendantAncestorComparison.boundaryCorrection_relabel {R V B : Type u} [CommRing R] [Algebra ℚ R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] [AddCancelCommMonoid B] {D : EffectiveCurveMonoid B} {C : StableCurveCohomology R} {Omega : GromovWittenTheory R V B D C} {P : PsiClasses C} {M : StableMapDescendants Omega} (X : DescendantAncestorComparison P M) (g : ℕ) (S T : Type) [Fintype S] [Fintype T] (hS : StableArity g S) (hT : StableArity g T) (e : S ≃ T) (beta : B) (k : S → ℕ) : (C.rename g S T hS hT e).toLinearMap.compMultilinearMap (MultilinearMap.domDomCongr e (X.boundaryCorrection g S hS beta k)) = X.boundaryCorrection g T hT beta fun (t : T) => k (e.symm t)

The residual is natural under simultaneous relabelling of markings, powers, and state-space inputs.

theorem AxiomaticGW.DescendantAncestorComparison.boundaryCorrection_degree {R V B : Type u} [CommRing R] [Algebra ℚ R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] [AddCancelCommMonoid B] {D : EffectiveCurveMonoid B} {C : StableCurveCohomology R} {Omega : GromovWittenTheory R V B D C} {P : PsiClasses C} {M : StableMapDescendants Omega} (X : DescendantAncestorComparison P M) (g : ℕ) (S : Type) [Fintype S] (h : StableArity g S) (beta : B) (k p : S → ℕ) (a : S → V) (q : ℕ) (ha : ∀ (s : S), a s ∈ Omega.graded.degree (p s)) (hq : GWOutputDegree Omega.graded.dimension g (∑ s : S, p s + ∑ s : S, k s) q (Omega.c1Degree beta)) : (X.boundaryCorrection g S h beta k) a ∈ (C.H g S).degree q

For homogeneous inputs, the residual has the same total codimension as the descendant and ancestor classes it compares.

theorem AxiomaticGW.DescendantAncestorComparison.invariant_eq_ancestor_add_boundary {R V B : Type u} [CommRing R] [Algebra ℚ R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] [AddCancelCommMonoid B] {D : EffectiveCurveMonoid B} {C : StableCurveCohomology R} {Omega : GromovWittenTheory R V B D C} {P : PsiClasses C} {M : StableMapDescendants Omega} (X : DescendantAncestorComparison P M) (I : StableCurveIntegration C) (g : ℕ) (S : Type) [Fintype S] (h : StableArity g S) (beta : B) (k : S → ℕ) : M.invariant I g S h beta k = Omega.ancestorInvariant P I g S h beta k + (I.integrate g S h).compMultilinearMap (X.boundaryCorrection g S h beta k)

Integrating the residual decomposition gives the numerical descendant--ancestor identity.