Function zeta_or_share_opt 

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

zeta_or_share against a reducer that reports PROGRESS: step answers None when there is no redex. reduction.rs’s reduce_step_opt calls it for every Term::Let.

use logicaffeine_kernel::term_store::zeta_or_share_opt;
use logicaffeine_kernel::Term;

let v = |n: &str| Term::Var(n.into());
let g = |n: &str| Term::Global(n.into());
let app = |f: Term, x: Term| Term::App(Box::new(f), Box::new(x));
let normal = |_: &Term| None;

// Used once: ζ fires on the unreduced value.
let once = app(g("Succ"), v("x"));
assert_eq!(
    zeta_or_share_opt("x", &g("Nat"), &g("Zero"), &once, &normal),
    Some(app(g("Succ"), g("Zero"))),
);

// Used twice, nothing inside steps and neither does the expansion: the shared `Let` is the
// normal form.
let twice = app(app(g("quad"), v("x")), v("x"));
assert_eq!(zeta_or_share_opt("x", &g("Nat"), &g("Zero"), &twice, &normal), None);

The rule, in four cases, and note that NONE of them needs a structural comparison:

• The name occurs at most ONCE in the body → ζ fires exactly as it did before, Some(body[name := value]) on the UNREDUCED value. Byte-identical to the old 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 and something inside still steps → the binding is KEPT as the sharing node and the step is reported on whichever of the annotation, value and body moved. A value bound once and used n times is written ONCE instead of n times, which is a_shared_subterm_is_checked_once_and_not_once_per_occurrence: the corpus’s term is 329 nodes under the old arm and 92 under this one, against a ceiling of 97.
• The name occurs MORE, nothing inside steps, and the one-step ζ EXPANSION still has a redex → Some(expansion). “Nothing inside steps” is NOT “no redex”. ζ is always available, and firing it can unblock a rule that could not see past the binding: let twice := 4 in plus twice twice is stuck only because plus’s structural argument is a VARIABLE, and expanding it lets ι unroll to 8. Getting this wrong took lean_conformance_t02_declarations::a_let_rec_is_a_fix_bound_by_a_let_and_a_plain_let_cannot_ carry_it — recorded Native — from green to a stuck Let, along with six other tests in five different files; W_perf_extra::the_zeta_gate_expands_a_shared_binding_whose_ expansion_can_still_compute is the lock.
• The name occurs MORE, nothing inside steps, and the expansion has no redex either → None. The shared Let IS the normal form — the corpus’s quad b b b b, whose head is a declaration with no body and which cannot step however b is spelled — said exactly rather than recovered from reduced == current, so the fixpoint in normalize_checked_at terminates on the nose and never pays a Θ(size) compare to find out.

The probe is run at most ONE level deep (see ZETA_SPECULATING): inside it, a nested shared binding answers with the verdict the rule gives it — a shared Let whose parts are all normal is not a redex — because an unguarded probe is T(k) = 2·T(k−1) in the nesting depth of stuck shared bindings, which is a hang inside a single reduction step on input a caller chooses. W_perf_extra::a_nest_of_shared_bindings_does_not_make_the_zeta_probe_exponential is the lock, at sixteen levels.

The gate is RE-READ for free: reduction erases occurrences, and a body that stepped comes back through this same arm on the next pass, where a name now used once expands. That is what keeps a_dependent_let_body_types_only_because_zeta_runs_before_inference green — its body has three uses of n before reduction and one after.

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. def_eq(let b := v in body, body[b := v]) is the RED test to write BEFORE touching the arm.