Function check_positivity_resolved 

pub fn check_positivity_resolved(
    ctx: &Context,
    inductive: &str,
    constructor: &str,
    ty: &Term,
) -> KernelResult<()>

Strict positivity with every REFERENCE resolved — the paradox fence that a definitional alias cannot walk around.

check_positivity reads the constructor type as written, so a name is an occurrence of the inductive only when it is SPELLED as the inductive. That is not a property of the type, it is a property of the spelling, and δ makes the two different things:

Inductive Bad : Type 0                 -- no constructors yet
Definition Negate : Prop := Bad -> False
Constructor cons : Negate -> Bad       -- `Bad` does not literally occur in `Negate`

Negate is Bad → False up to δ, so cons is the Russell constructor (Bad → False) → Bad — and λx. match x with | cons f => f (cons f) then inhabits Bad → False, which applied to its own cons inhabits False. No fixpoint and no recursor are needed: a bare Term::Match does it, so no later gate can catch what this one lets past. The blind check accepts it because occurs_in asks whether the STRING “Bad” appears.

This entry point answers the same four questions about the same four shapes, but resolves a reference to a transparent definition (or a universe-polymorphic one) before deciding whether the inductive occurs in it and whether an occurrence is a legitimate recursive one. Both directions fail SAFE: a reference whose unfolding cannot be decided counts as an occurrence (so the constructor is refused), and never as a recursive one.