Function beta_zeta_normal_form_in_context 

pub fn beta_zeta_normal_form_in_context(
    ctx: &Context,
    term: &Term,
    budget: u64,
) -> Option<Term>

beta_zeta_normal_form with every policy question answered from the Context — the form a reducer wires in, with nothing left for the caller to get wrong.

The inertness criterion, and why it is POSITIVE

A Global is admitted only when it is a CONSTRUCTOR or an INDUCTIVE and carries no definition body. That is a closed, positive criterion, and it is chosen over the obvious negative one — “not a definition and not one of these builtin names” — because the negative one is a list that a future rule can silently fall off the end of.

It is sufficient, rule by rule, against reduction::reduce_step_opt:

• δ cannot fire: a constructor and an inductive have no body, and the belt-and-braces get_definition_body(name).is_none() says so a second time.
• The arithmetic primitives cannot fire: try_primitive_reduce returns None unless the ARGUMENT is a Term::Lit, and a Lit anywhere is refused by shape.
• ι cannot fire: it is the Match rule, refused by shape.
• Fixpoint unrolling cannot fire: it needs a Fix head, refused by shape.
• Every NAME-keyed rule — the reflection builtins syn_*, the tactic builtins try_* and tact_*, induction_*, concludes, the native-evaluation hook reduceBool, and the quotient eliminators Quot_lift/Quot_ind — is registered with add_declaration and is therefore neither a constructor nor an inductive. W_perf_extra:: the_conservative_inertness_criterion_refuses_every_name_keyed_rule_head executes that claim over the whole list rather than asserting it in prose.
• A registered @[simp] rewrite can fire on ANY shape, so the door is shut outright whenever the context has one.

Transparency does not enter

Transparency::Excluding only ever makes δ LESS available, and the criterion already admits no term δ could touch. So the answer is the same at every transparency, which is why this takes no transparency argument.