rank
plain-language theorem explainer
rank counts the number of states y with strictly smaller J-value than x within a finite set equipped with decidable equality. Order-preservation results in RRF and downstream SAT or cost models cite this to compare relative positions under monotone transforms. The definition computes this directly as the cardinality of the strict lower set in the finite universe.
Claim. Let $S$ be a finite type with decidable equality. Given a map $J : S → ℝ$, the rank of an element $x ∈ S$ is the cardinality of the set of all $y ∈ S$ such that $J(y) < J(x)$.
background
In the RRF module, theorems focus on preservation of ordering under operations on states. States come from discrete models such as the 2D Galerkin truncation in CPM2D or finite lattice vorticity fields in DiscreteVorticity. The J map assigns a real-valued cost or strain to each state. This rank mirrors the stage-based rank in PreTemporalForcingOrder, where lower numerical rank corresponds to prior structure in the forcing chain. The module emphasizes that RRF prioritizes relative ordering by strain over absolute values, so any monotone operation preserves meaning.
proof idea
The definition is a direct one-line computation: it forms the Finset of all y in the universe where J y is strictly less than J x, then takes its cardinality.
why it matters
This definition supplies the basic rank measure used across 39 downstream declarations, including feasible_implies_boolean in SAT models and sharp in Ndim projectors. It supports the order-preservation theorems in the RRF module, which underpin channel transfer and strain ordering results. In the broader framework it aligns with the emphasis on J-uniqueness and self-similar ordering from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.