Function beta_zeta_normal_form 

pub fn beta_zeta_normal_form(
    term: &Term,
    inert: &dyn Fn(&str) -> bool,
    budget: u64,
) -> Option<Term>

THE PURE β/ζ DOOR. The Term-level entry point a tree reducer wires in so a β-heavy reduction stops being quadratic — and the only one it needs, because it answers None for every term it is not certain about.

Some(nf) is a promise that nf is EXACTLY what a full kernel reduction would have produced: the same term, not merely an α-equivalent one. None means “not mine” and the caller falls through to the path it already has, unchanged.

Why this is the fix and a faster loop is not

lean_conformance_t00_terms::a_deep_spine_costs_linearly_in_its_depth_and_not_quadratically asks for at most 5× when a spine’s depth TRIPLES. A tree reducer pays Θ(size) per step — the β step copies the remaining spine, and the fixpoint comparison walks it — over Θ(size) steps, so it is Θ(size²) and tripling costs about 9×. A ratio is immune to constant factors, so no amount of tuning reaches the bar; the representation has to change. On this store every step is u32 work against hash-consed nodes, and the same reduction is linear. W_perf_extra::w_perf_measure_the_spine_in_the_tree_and_in_the_store prints both columns at the corpus’s own two depths, and W_perf_extra::the_pure_door_triples_the_corpus_spine_in_under_five asserts the bar on this path.

What it refuses, and why each refusal is exact

The store implements β and occurrence-gated ζ. It implements nothing else, so it must never be handed a term another rule could touch. Six shapes are refused in O(1) from TermStore::shapes:

• Match — ι lives there.
• Fix and MutualFix — unrolling asks termination::structural_columns which column the recursion descends on; the store cannot call it.
• Const — δ with a level substitution, plus the well-formedness test that turns a mis-levelled reference into Term::Hole rather than into a normal form.
• Lit — the arithmetic primitives fire only when the ARGUMENT is a literal, so a term with no literal anywhere cannot reach one.
• Hole — not a term of the calculus; the type checker refuses it by construction.

And every Global name in the term must satisfy inert. That predicate is the CALLER’s because only the caller has the Context: a name is inert when δ cannot unfold it (ctx.get_definition_body(name).is_none()) and it is not one of the names a rule is keyed on rather than a shape — the reflection builtins syn_*, the native-evaluation hook reduceBool, and the quotient eliminators Quot_lift/Quot_ind. The caller must also refuse the whole door when its context has any registered @[simp] rule, since a rewrite can fire on any shape at all.

The two remaining honesty conditions

• Budget. budget counts β and ζ steps. Exhausting it is None, never a term passed off as normal — the same distinction normalize_checked draws between a normal form and a spent budget.
• No invented names, on EITHER side. Capture-avoiding substitution renames binders, and an answer that renamed is α-equivalent to the kernel’s rather than equal to it. Both implementations rename on the same criterion — the binder’s name is a free variable of the replacement — so where that criterion never fires they are the SAME FUNCTION. Where it does fire they can still differ, because type_checker::substitute_avoiding descends the WHOLE body and renames such a binder even in a subtree the substituted variable never reaches, while this store descends only where the substitution is live. So the door refuses on TermStore::rename_risk — set the moment any substitution pushes a value into a body that binds one of the value’s free names — and, as a second and independent check, on TermStore::binders_within.