bridge_constant_monotone
plain-language theorem explainer
If a triangulation family is RS-admissible at bridge constant C, it remains RS-admissible at every larger constant C' ≥ C. Gravity path-sum arguments cite this to loosen error budgets without re-checking mesh and growth constraints. The proof rebuilds the admissibility witness, transporting the bridge inequality by right-multiplication with a nonnegative mesh cube and transitivity of ≤.
Claim. Let $F$ be an admissible triangulation family that is RS-admissible with bridge constant $C \ge 0$. For every real $C' \ge C$, the family $F$ is again RS-admissible, with the same mesh bounds, growth data, curvature scale, and recognition ratio, and with bridge constant equal to $C'$.
background
This module answers the demand for an explicit, machine-checkable procedure describing which triangulations Recognition Science allows in the recognition path sum. An admissible triangulation family already packages a positive mesh lower bound, a finite simplex-count cap, and a positive growth base. The RS-admissibility predicate layers further data: a mesh upper bound, a positive curvature scale $\kappa$, a nonnegative bridge constant $C$, a positive recognition ratio, and the bridge inequality itself.
The bridge is a physical hypothesis, not derived from RS axioms: $\log x_\sigma = \kappa \cdot \mathrm{deficit} + O(\mathrm{mesh}^3)$. Deficit means the angular deficit $2\pi - \sum \theta$ at a hinge, as in the Schläfli and dihedral-angle geometry. The bridge constant $C$ is the implicit constant in that cubic mesh error, so enlarging $C$ loosens the error budget while leaving the combinatorial family fixed.
proof idea
Term-mode construction of a fresh RS-admissibility witness. Mesh bounds, $\kappa$, recognition ratio, and all positivity proofs are copied from the given witness. The new bridge constant is set to $C'$. Nonnegativity of $C'$ is le_trans of the original nonnegativity with $C \le C'$. The bridge inequality is transported by le_trans: the original bound gives an error at most $C \cdot \mathrm{mesh}^3$, and $C \cdot \mathrm{mesh}^3 \le C' \cdot \mathrm{mesh}^3$ follows from mul_le_mul_of_nonneg_right using nonnegativity of the cube of the mesh lower bound (pow_nonneg). The constructed witness is wrapped in Nonempty.
why it matters
Closure fact: the set of admissible bridge constants is upward-closed. In the gravity path-sum UV-bound pipeline one often extracts a concrete $C$ from a local estimate and later needs a uniform or slightly larger constant; monotonicity avoids re-proving mesh and growth constraints. The module deliberately treats the bridge as an assumed physical interface rather than an RS axiom, so this lemma keeps that interface flexible under coarser error budgets.
No downstream consumers are wired yet (used_by is empty). Natural call sites are the sibling witnesses in the same procedure module (existence of an RS-admissible family, concrete admissibility witnesses). Framework-wise it supports the triangulation side of recognition gravity; it does not touch the T0–T8 forcing chain, the Recognition Composition Law, or the $\phi$-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.