convergent
plain-language theorem explainer
The declaration convergent defines a predicate on a real parameter a2 that holds exactly when 1 minus twice a2 is positive. Researchers modeling equilibrium configurations or lattice convergence in Recognition Science would cite this predicate to enforce a strict bound on the a2 coefficient. The definition is a direct one-line abbreviation of the inequality with no further reduction.
Claim. Let $a_2$ be a real number. The predicate convergent$(a_2)$ asserts that $1 - 2 a_2 > 0$.
background
The VoxelWalks module supplies auxiliary constants and functions such as phi (the self-similar fixed point), A2 (the real parameter under test), sigmaCore, fEye, and fHalfVoxel. These support discrete path constructions whose convergence is controlled by simple inequalities on coefficients. The convergent predicate is introduced with no upstream dependencies and sits inside the broader Recognition Science lattice that encodes forcing chains and composition laws.
proof idea
This is a one-line definition that directly encodes the inequality 1 - 2 * a2 > 0 as a Prop.
why it matters
The predicate is referenced by nine downstream declarations, including unity_is_equilibrium (which shows the unity configuration is an equilibrium when log-charge vanishes), rs_implies_gr (which derives general relativity from RS convergence axioms), bet2_for_galerkin, RM2Closed, direct_rh_from_zero_free_criterion, and chi8_periodic. It supplies the elementary convergence gate that closes equilibrium and closure arguments across variational dynamics, gravity, Navier-Stokes, and analytic number theory sections of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.