INCLUSION CRITERIA
An entry belongs in this subdivision if and only if its consequence relation omits contraction while retaining weakening, so that each hypothesis is used at most once.
Required: At least one of the following:
- A sequent or natural-deduction system without the contraction rule but with weakening
- An "at-most-once" resource reading of hypotheses
- A calculus explicitly presented as affine over a linear or classical base
Not sufficient: Dropping weakening as well as contraction (Linear). Dropping exchange (Ordered). Dropping weakening for relevance (Relevant). Full structural rules (a classical or intuitionistic base belongs in Algebraic).
Boundary: Affine type systems that enforce at-most-once use through typing belong in Type/Simple or Type/Effects; the pure affine proof theory belongs here.