Paper: Tropical Token Types — novel graded session types

Formal contribution to type theory:
1. First use of tropical semiring (ℕ∪{ω}, +, max, 0, 0) as grading
   for a type system — grades represent LLM token cost
2. First combination of graded types with multiparty session types —
   static verification that protocols complete within token budgets
3. Harvard Architecture = tropical zero set (connection to tropical
   algebraic geometry)
4. Shadow pricing of type errors (BudgetExceeded = tropical dual)
5. Reversibility theorem: bounded total cost under caching + reversal

Typing rules: T-Seq (costs add), T-Branch (costs max), T-Cached (0),
T-Neural (0), T-Harvard (Data = grade 0), T-Budget (grade ≤ N).

Theorem: Budget Sufficiency for graded session types.
Theorem: Harvard = Tropical Zero Set.
Theorem: Bounded Total Cost under Reversibility.

Connects: Granule (graded types), QTT/Idris2 (linearity), AARA
(resource analysis), Honda/Yoshida (session types), Landauer
(reversibility), Eclexia (shadow pricing).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath