Function zeta_or_share 

pub fn zeta_or_share(
    name: &str,
    ty: &Term,
    value: &Term,
    body: &Term,
    step: &dyn Fn(&Term) -> Term,
) -> Term

ONE ζ step, OCCURRENCE-GATED, against a reducer that always returns a Term.

zeta_or_share_opt is the one to wire in. reduction.rs no longer has a Term-returning reduce_step_at; its reducer is reduce_step_opt -> Option<Term>, and the progress-reporting form is both simpler and stricter. This form stays because a step function that cannot say “no redex” is still a legitimate shape — the in-file fixpoint driver uses it — and because the two must be provably the same rule, which the_two_zeta_gates_are_the_same_rule pins on every shape.

The rule, in three cases:

• The name occurs at most ONCE in the body → ζ fires exactly as it does today, body[name := value], on the UNREDUCED value. Byte-identical to the current arm, which is what keeps every let_zeta.rs case and the T00 ζ-transparency cases green: all of them are single-occurrence.
• The name occurs MORE → the binding is KEPT as the sharing node and step is run on the annotation, the value and the body instead. The Let survives into the normal form, so a value bound once and used n times is written ONCE rather than n times. That is a_shared_subterm_is_checked_once_and_not_once_per_occurrence: the corpus’s term is 329 nodes under the current arm and 92 under this one, against a ceiling of 97.
• When nothing inside can step any further the gate is RE-EVALUATED on the reduced body, because reduction ERASES occurrences: a body with three uses of n before reduction and one after must still expand, or a_dependent_let_body_types_only_because_zeta_runs_before_ inference goes red.

What the caller owes in return

A Let that survives into a normal form is a Let that conversion has to see through. def_eq/types_equal/is_subtype must ζ-expand a Let HEAD on demand — zeta_expand_head_term is that step — or two convertible terms, one of which happens to have kept its binding, will compare unequal. That is the negative test to write first.