Effective monotonicity of complete linear systems

This file records the elementary monotonicity calculus for complete linear systems of Weil divisors. If D ≤ D' coefficientwise, then adding the effective difference D' - D sends |D| into |D'|; in particular nonemptiness of complete linear systems is monotone under the divisor order.

This is the divisor-level bookkeeping behind the later symmetric-power and Abel-map lane in the Jacobian roadmap: increasing an effective divisor by fixed effective base conditions should not destroy the existence of effective representatives. It advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A, "Divisors on a curve" and "Degree", as a clean prerequisite for the Layer C/D Abel-map construction from symmetric powers. No external mathematics is vendored; the proofs reuse Tau Ceti's existing complete-linear-system addition API and the coefficientwise order on formal Weil divisors.

Monotonicity for the divisor order

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.add_sub_mem_completeLinearSystem_of_le {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D D' E : WeilDivisor X} (hDD' : D ≤ D') (hE : E ∈ S.completeLinearSystem D) : E + (D' - D) ∈ S.completeLinearSystem D'

If D ≤ D', then translating a member of |D| by the effective difference D' - D gives a member of |D'|.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.mapsTo_add_sub_completeLinearSystem_of_le {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D D' : WeilDivisor X} (hDD' : D ≤ D') : Set.MapsTo (fun (E : WeilDivisor X) => E + (D' - D)) (S.completeLinearSystem D) (S.completeLinearSystem D')

The order-induced translation map sends |D| into |D'| whenever D ≤ D'.

theorem TauCeti.AlgebraicGeometry.WeilDivisor.OrderSystem.nonempty_completeLinearSystem_of_le {X : Type u_1} {G : Type u_2} [AddCommGroup G] (S : OrderSystem X G) {D D' : WeilDivisor X} (hDD' : D ≤ D') (hD : (S.completeLinearSystem D).Nonempty) : (S.completeLinearSystem D').Nonempty

Nonemptiness of complete linear systems is monotone for the divisor order.