moveRate
plain-language theorem explainer
Every legal LIFO post or unpost on a tet-free bounded complex is assigned primitive rate one, independent of source and target. Gravity and measure-derivation arguments cite this as the generator of the C16 Poisson process. The body is the constant function 1: no Metropolis factor, Aut weight, or state dependence.
Claim. For any bound $B$ and any two tet-free serially named complexes $K,K'$ at cap $B$, the directed transition rate is $\mathrm{rate}(K\to K')=1$.
background
Gap 2 / A20 (lane C16) studies a raw LIFO Poissonized post/unpost process on serially named tet-free bounded complexes. The state space is TetFree B: complexes with vertex and edge counts at most $B$, edge endpoints in the named vertex set, and no tetrahedra. Process symbols deliberately name neither Aut, orbit, gauge class, nor Gibbs weight (C35 firewall).
Legal moves are: append a vertex; unpost the max-named vertex if unused; append an edge with chosen endpoints; unpost the max-named edge. The module headline is that this process has symmetric legal rates, hence a uniform stationary law on each finite cap. Cap-3 has 910 named states with exact uniform stationary measure $1/910$; cap-4 uniformity (host of the $(4,2,0)$ witnesses) is derived-unformalized from the same rate-symmetry plus irreducibility argument.
The rate is the continuous-time Markov generator entry for a directed transition. Setting every legal move to unit rate is the MODEL clause of the C16 kill test: no state-dependent Metropolis factor and no orbit weight enter the process side.
proof idea
Definitional constant: the body is the natural number $1$, ignoring both complex arguments. No lemmas are applied. Downstream symmetry theorems (moveRate_symm, the LIFO vertex/edge reverse-pair lemmas) hold by rfl precisely because both directions evaluate to the same constant.
why it matters
This constant rate is the process primitive that forces rate symmetry and, with irreducibility, uniform stationarity on each finite cap. Downstream, moveRate_symm and the LIFO reverse-pair lemmas specialize it; uniform_detailed_balance then shows that the uniform named weight satisfies detailed balance for this generator.
Those facts feed c16_process_discrimination and measureDerivationPremises in Gap2MeasureDerivation: under the named uniformity premise, the $\pi$-weighted class-mass ratio at census $(4,2,0)$ is exactly $1/2$, matching the directed inverse-Aut ratio. Aut appears only on the comparison side. The definition therefore anchors the MODEL half of the Poisson recognition coarea argument without importing FullTheoryLedger or moving flag 8.
In the broader Seven Gaps gravity stack this is the rate that makes factorial arrival-order counts emerge as cardinalities rather than measure hypotheses, separating process from orbit bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.