rsAdmissibleWitness
plain-language theorem explainer
A concrete triangulation family with maxSimplexCount 1, growth base 2, and unit mesh, packaged as an AdmissibleTriangulationFamily. Gravity and discrete-geometry workers cite it as the explicit witness that RS admissibility is inhabited. Field values are pure constants so positivity side-goals close by norm_num.
Claim. There is an explicit admissible triangulation family with maximum simplex count $1$, growth base $2$, and minimum mesh $1$ (all strictly positive). Downstream, the recognition-ratio bridge is realized by $x(\mathrm{deficit})=\exp(\mathrm{deficit})$ with $\kappa=1$ and bridge constant $0$, so the log-deficit identity holds exactly.
background
The module answers the demand for a machine-checkable procedure stating which triangulations RS allows. It layers the predicate IsRSAdmissible on the existing AdmissibleTriangulationFamily structure from PathSumUVBound: positivity of mesh, simplex count, and growth base are derived; the bridge relating recognition ratios to hinge deficits is an explicit physical hypothesis.
Hinge deficit is the standard geometric quantity $2\pi - \sum\theta$ (DihedralAngle / Schläfli). The bridge assumption is $\log x_\sigma = \kappa\cdot\mathrm{deficit} + O(\mathrm{mesh}^3)$, not derived from the T0–T8 forcing chain; it is stated openly as assumed structure linking recognition operators to Regge-style discrete curvature.
This definition supplies one concrete family so that non-emptiness of the RS-admissible class can be proved by exhibition rather than abstract existence.
proof idea
Definitional construction, not a tactic proof. The structure fields are set to literal constants (maxSimplexCount := 1, growthBase := 2, minMesh := 1). Each positivity obligation (maxSimplexCount_pos, growthBase_pos, minMesh_pos) is discharged by a one-line norm_num. Remaining bridge parameters (mesh upper bound 2, $\kappa=1$, bridge constant 0, recognition ratio $\exp$) live on the downstream IsRSAdmissible instance built from this witness.
why it matters
Feeds exists_RSAdmissible, which packages this witness into a nonempty proof that an RS-admissible family exists: derived positivity fields are copied from the witness, and the bridge holds exactly because $|\log(\exp(d)) - 1\cdot d| = 0 \le 0\cdot 1^3$. Without a concrete family, the admissibility predicate would be vacuously uninhabited in Lean.
In the gravity stack this closes the procedural gap between continuum RS claims and discrete path-sum / UV-bound arguments that need a triangulation family. It does not derive the bridge from the forcing chain (T5 J-uniqueness, T7 eight-tick, T8 $D=3$); it only shows the admissibility interface is satisfiable once the bridge is granted with exact exponential recognition ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.