Registry · Definition III.D39 tau-effective formalized

III.D39 — Defect Functional Δ

Δ(f, n) measures the deviation of an ω-germ f from canonical form at primorial depth n. Δ ≥ 0; Δ = 0 iff stabilized. The defect is computable at each finite level.

Book III Part 5 Ch. 35

Dependency Graph

Depends on (2)

Depended on by (4)

Lean Formalization

Module: TauLib.BookIII.Physics.FluidData

Symbol: defect_monotone_check