IsRSAdmissible
plain-language theorem explainer
RS-admissible triangulation families are those with positive mesh lower bound, finite simplex-count cap, positive growth base, and a recognition-ratio bridge log x_σ = κ·deficit + O(mesh³). Gravity and path-sum workers cite this predicate when fixing which meshes enter the recognition path sum. It is a structure packing three derived positivity facts plus one assumed physical bridge, not a proved theorem.
Claim. An admissible triangulation family $F$ is RS-admissible when $F.(\mathrm{minMesh})>0$, $F.(\mathrm{maxSimplexCount})>0$, $F.(\mathrm{growthBase})>0$, and there exist $\mathrm{meshUpperBound}\ge F.(\mathrm{minMesh})$, $\kappa>0$, $C\ge 0$, and a map $x_\sigma:\mathbb{R}\to\mathbb{R}$ with $x_\sigma(\delta)>0$ for all $\delta\ge 0$, such that $|\log x_\sigma(\delta)-\kappa\,\delta|\le C\,F.(\mathrm{minMesh})^3$ for every deficit $\delta\ge 0$.
background
The module answers the demand for an explicit procedure naming which triangulations RS allows in the recognition path sum. It sits on top of AdmissibleTriangulationFamily from the path-sum UV-bound layer: a family already carries a positive minimum mesh, a finite simplex-count cap, and a positive growth base used to control refinement.
RS-admissibility re-records those three positivity facts as derived fields, then adds a mesh upper bound for comparison and the recognition-ratio bridge. The bridge links the recognition ratio $x_\sigma$ at a hinge deficit angle $\delta$ to a linear law $\log x_\sigma=\kappa\delta$ with cubic mesh error. Module documentation stresses that this bridge is a physical hypothesis, not a consequence of the RS forcing chain or the Recognition Composition Law.
Notation: mesh is the characteristic edge length of the triangulation; deficit is the angular deficit at a hinge; $\kappa$ is the coupling in the bridge; $C$ is the $O(\mathrm{mesh}^3)$ error constant.
proof idea
No proof: this is a structure definition. Fields are either copied positivity hypotheses from the underlying triangulation family (mesh, simplex count, growth base) or parameters of the assumed bridge (upper mesh bound, $\kappa$, $C$, the map $x_\sigma$, positivity of $x_\sigma$ on nonnegative deficits, and the pointwise log-bridge inequality). Downstream constructions fill the fields by norm_num/positivity on concrete constants or by reusing an existing witness.
why it matters
Makes the admissibility procedure a machine-checkable Lean object rather than prose. Downstream, exists_RSAdmissible exhibits a concrete witness family (unit mesh, exact exponential bridge with $\kappa=1$, $C=0$), and bridge_constant_monotone shows the set of admissible error constants is upward-closed: any $C'\ge C$ still yields an RS-admissible packing.
In the gravity stack this is the gate on meshes that enter recognition path sums and UV bounds. The bridge is deliberately tagged assumed: it is not forced by T5 J-uniqueness, T6 $\varphi$, or the eight-tick octave, so later master theorems that quote RS-admissible families inherit an explicit physical hypothesis rather than a hidden axiom. Closing or replacing that bridge is the open scientific question this interface isolates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.