The absent module — why there is no free Divisive.

Divisive adds recip :: a -> a with the law a / a == one || a == zero. The law is conditional: it only applies when a ≠ zero. Conditional laws are not equations; the theory is not an equational variety, and initial objects do not exist.

This is the same boundary found diagrammatically: division refused to be a generator and demanded mirror wires (the relational move) instead of maps. The value-level statement and the wiring-level statement are one fact: division is not algebraic.

Two escape routes

1. Localization — formal fractions carrying explicit nonzero witnesses in the type:

data Fraction a = Fraction { numerator :: a, nonzeroWitness :: NonZero a }

Partiality is made visible. Arithmetic becomes a proof obligation.

2. The relational move — from linear maps to linear relations. "Divide by n" is the converse of "multiply by n". Converse absorbs partiality natively: the relation simply has nothing at zero. This is Duplex in circuits, Stage 3, the compact-closed stage where wires run backwards.

Neither route yields a naive Recip constructor with equations, because the equations do not exist. hasknum stops here.