This repository contains a Lean 4 formalization of the paper Factorizations, symmetry reductions, and phase transitions in rowmotion Markov chains. The formalization covers the tensor-product decomposition of Boolean rowmotion chains with inhomogeneous probabilities, the complete orthonormal eigenbasis and eigenvalue computation, the exact chi-square distance formula from any start state, sharp total-variation upper bounds, orbit lumping under group equivariance, tensor-product factorization and reversibility for disjoint unions, total-variation product bounds for probability measures, and the Bhattacharyya coefficient multiplicativity that underlies the Hellinger isometry for occupancy chains. Exit-rate positivity for complete bipartite orders and ordinal sums of antichains is also verified. Every theorem compiles against Lean 4.28.0 with Mathlib and checks cleanly under lean_verify with no axioms beyond propext, Classical.choice, and Quot.sound.

The proof architecture exploits a single recurring technique throughout: the identity $\sum_{f\colon[n]\to S}\prod_i g_i(f(i))=\prod_i\sum_{s\in S}g_i(s)$, formalized via Mathlib's Fintype.prod_sum, which converts sums over the exponentially large state space ${0,1}^n$ into products of two-element sums that close by field_simp and nlinarith. This factorization drives the row-sum proof for the product kernel, the stationary-distribution normalization, the detailed-balance verification, the eigenfunction orthogonality and normalization, the eigenfunction-eigenvalue relation, the chi-square coordinate decomposition, and the Hellinger isometry. The paper.tex and refs.bib files contain the corresponding mathematical paper aligned with the verified content.