Constant OMEGA_PROOF_SENTINEL 

pub const OMEGA_PROOF_SENTINEL: &str = "__aver_omega_proof__";

Sentinel identifier injected as an extra synthetic argument at every recursive callsite inside an IntCountdownGuarded body. Lean’s expr emitter recognises this name and renders it as (by omega); Dafny’s codegen never sees it because Dafny discharges preconditions via auto-inference at the existing fn-def emit path.