exists_RSAdmissible
plain-language theorem explainer
A concrete triangulation family is RS-admissible: positive mesh floor, finite simplex cap, positive growth base, and a recognition-ratio bridge that holds exactly. Gravity path-sum work needing a checked admissible mesh cites this existence. The proof is a direct structure inhabitant: derived positivity comes from the witness fields; the bridge closes with κ=1, C=0 and x(δ)=e^δ, so the log-deficit error is identically zero.
Claim. The concrete admissible triangulation family witness carries an RS-admissibility structure: its minimum mesh, maximum simplex count, and growth base are strictly positive; a mesh upper bound of $2$ dominates the minimum mesh; taking bridge slope $\kappa=1$, bridge constant $C=0$, and recognition ratio $x(\delta)=e^{\delta}$, one has $|\log x(\delta)-\kappa\cdot\delta|\le C\cdot(\mathrm{mesh})^3$ for every deficit angle $\delta$.
background
This module answers the demand for an explicit, machine-checkable procedure saying which triangulations RS gravity may use. It layers the predicate of RS admissibility on top of an existing admissible triangulation family (from the path-sum UV bound development): positive mesh lower bound, finite simplex-count cap, and positive growth base are derived from that family; a mesh upper bound and a recognition-to-deficit bridge are recorded as additional data.
The bridge is the physical link: $\log x_\sigma = \kappa\cdot\mathrm{deficit}+O(\mathrm{mesh}^3)$, tying recognition ratios on simplices to angular deficit (hinge deficit $2\pi-\sum\theta$ in the geometry layer). Module documentation is explicit that the bridge is an assumed hypothesis, not a consequence of the RS forcing chain or the Recognition Composition Law.
The witness family supplies concrete positive constants (minimum mesh equal to $1$ in the proof) so the derived positivity fields are immediate. Admissibility here is about mesh and bridge bookkeeping for path sums, not the ledger-state admissibility flag elsewhere in the foundation.
proof idea
Construct an inhabitant of the RS-admissibility structure on the witness family. Copy the three derived positivity proofs straight from the witness (minMesh_pos, maxSimplexCount_pos, growthBase_pos). Set mesh upper bound to $2$ and discharge $\mathrm{minMesh}\le 2$ by unfolding $\mathrm{minMesh}=1$ and norm_num. Choose $\kappa=1$, $C=0$ (both positivity/nonnegativity by norm_num), and recognition ratio $x(\delta)=e^{\delta}$ with positivity from Real.exp_pos.
The bridge goal reduces to $|\log(e^{\delta})-1\cdot\delta|\le 0\cdot(\mathrm{mesh})^3$. Rewrite with Real.log_exp, cancel $\delta-\delta$ by ring, then abs_zero and zero_mul leave $0\le 0$, finished by norm_num. No external geometric lemmas are needed beyond the witness fields.
why it matters
Closes the procedural gap flagged in the module header: RS gravity path sums now have a checked existence proof that at least one triangulation family meets the full RS admissibility predicate, including an explicit bridge choice. Downstream usage is not yet wired in this snapshot (used_by empty), but the sibling monotonicity fact for the bridge constant is the natural closure: any larger $C'\ge C$ preserves admissibility, so the zero-error witness seeds an upward-closed family of bounds.
Within the framework this is infrastructure for continuum or semiclassical gravity limits on the recognition side, not a step in the T0–T8 forcing chain. The bridge remains an external physical hypothesis (recognition ratio versus deficit), cleanly separated from derived mesh bookkeeping. That separation is the scientific content: existence is proved for a concrete choice, while the status of the bridge as axiom versus theorem stays visible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.