diff --git a/vortex-array/src/stats/rewrite.rs b/vortex-array/src/stats/rewrite.rs
index bf342a95cdd..52d354df1a0 100644
--- a/vortex-array/src/stats/rewrite.rs
+++ b/vortex-array/src/stats/rewrite.rs
@@ -23,18 +23,34 @@ pub(crate) use builtins::register_builtins;
 /// Shared reference to a stats rewrite rule.
 pub(crate) type StatsRewriteRuleRef = Arc<dyn StatsRewriteRule>;
 
-/// A plugin-provided rule that rewrites predicates into stats-backed proof expressions.
+/// A plugin-provided rule for predicates whose root scalar function matches this rule.
 ///
-/// A falsifier evaluates to `true` only when the original predicate is definitely false for the
-/// current stats scope. A satisfier evaluates to `true` only when the original predicate is
-/// definitely true for the current stats scope. Returning `None` means the rule cannot prove
-/// anything for the expression.
-#[allow(dead_code)]
+/// Rules do not produce expressions equivalent to `expr`. They produce optional sufficient
+/// conditions over stats for the current scope:
+///
+/// - a falsifier evaluating to `true` proves that `expr` is false for every row in the scope;
+/// - a satisfier evaluating to `true` proves that `expr` is true for every row in the scope.
+///
+/// Returning `None` means this rule cannot prove anything for the expression. A returned proof
+/// expression that evaluates to `false` or `null` is also inconclusive.
+///
+/// Multiple rules may be registered for the same scalar function. Their proofs are combined with
+/// `OR`, so every proof returned by an individual rule must be sound on its own.
+///
+/// `expr` is the full predicate expression whose root scalar function id is
+/// [`Self::scalar_fn_id`]. Use [`StatsRewriteCtx`] to resolve dtypes and recursively rewrite child
+/// predicates.
 pub(crate) trait StatsRewriteRule: Debug + Send + Sync + 'static {
-    /// The scalar function ID this rule applies to.
+    /// Returns the scalar function id handled by this rule.
     fn scalar_fn_id(&self) -> ScalarFnId;
 
-    /// Rewrite an expression into a stats-backed falsifier.
+    /// Returns a stats-backed proof that `expr` is false for the current scope.
+    ///
+    /// If the returned expression evaluates to `true` against the scope's stats, then `expr` is
+    /// guaranteed to be false for every row in that scope. A returned proof expression that
+    /// evaluates to `false` or `null` is inconclusive.
+    ///
+    /// Returns `Ok(None)` when this rule cannot construct a sound falsity proof for `expr`.
     fn falsify(
         &self,
         expr: &Expression,
@@ -45,7 +61,16 @@ pub(crate) trait StatsRewriteRule: Debug + Send + Sync + 'static {
         Ok(None)
     }
 
-    /// Rewrite an expression into a stats-backed satisfier.
+    /// Returns a stats-backed proof that `expr` is true for the current scope.
+    ///
+    /// If the returned expression evaluates to `true` against the scope's stats, then `expr` is
+    /// guaranteed to be true for every row in that scope. A returned proof expression that
+    /// evaluates to `false` or `null` is inconclusive.
+    ///
+    /// This is not the complement of [`Self::falsify`]; both methods are one-way proofs and may be
+    /// implemented independently.
+    ///
+    /// Returns `Ok(None)` when this rule cannot construct a sound truth proof for `expr`.
     fn satisfy(
         &self,
         expr: &Expression,