Constant LAW_CLASS_MARKER_PREFIX 

pub const LAW_CLASS_MARKER_PREFIX: &str = "-- aver:law-class ";

Statement-class channel for emitted law theorems.

aver proof --check’s universal metric must know, per law theorem, whether the emitted STATEMENT is genuinely universal or bounded: for a when-law over non-refinement-lifted givens, law_theorem_prop prepends sampled-domain disjunction premises (a = 0 ∨ a = 1 ∨ …) — the theorem then only claims the law on the finite sample domain, even when it is proven by real tactics with a kernel-clean axiom profile. Refinement-lifted when-laws drop those premises (the Subtype carries the invariant) and stay genuinely universal.

Only the code that BUILDS the statement knows which premises it prepended, so the emitter records the class as one structured marker comment per emitted law theorem, preceding it in the generated .lean source (self-contained artifact — the classification travels with the export):

-- aver:law-class <theorem_name> universal
-- aver:law-class <theorem_name> bounded-domain

The checker (lean_universal_proof in the CLI) consumes these markers and must NEVER re-derive the class from theorem names or by re-parsing statements. A law theorem without a marker earns no universal credit (fail-closed for stale/foreign export dirs).