Pith. sign in
module module high

IndisputableMonolith.Gravity.AdmissibleTriangulationProcedure

show as:
view Lean formalization →

Defines the RS admissibility predicate for triangulation families in the recognition path sum. It packages three derived positivity/finiteness bounds (mesh, simplex count, growth base) plus an assumed bridge from recognition ratios to deficit angles. Path-sum and UV-bound arguments in gravity cite this to restrict which triangulations enter the sum. Content is definitional: the bridge is tagged as a physical hypothesis, not an RS-derived theorem.

claimA triangulation family is RS-admissible when $\min\mathrm{Mesh}>0$, the simplex-count cap is finite and positive, the growth base is positive, and the assumed bridge $\log x_\sigma = \kappa\cdot\mathrm{deficit}+O(\mathrm{mesh}^3)$ holds.

background

In Recognition Science gravity, the path sum runs over triangulations $T$ of a compact 4-manifold $M$, with mesh controlled from below by a sub-Planck cutoff $\ell_{\mathrm{sub}}$. Only families that stay UV-safe and recognition-compatible are allowed into that sum.

This module records the admissibility package for such families. Three conditions are structural and derived in form: a positive lower mesh bound, a finite positive simplex-count cap, and a positive growth base for how counts may scale. The fourth is the recognition-ratio bridge: $\log x_\sigma$ tracks a constant times angular deficit, up to $O(\mathrm{mesh}^3)$. The module doc tags that bridge as ASSUMED: a physical link from ratios to deficit geometry, not forced by the RS axiom chain.

Upstream, PathSumUVBound frames UV finiteness of the recognition path sum as a structural theorem over admissible triangulations with mesh bounded below. The predicate here is the local filter those arguments need.

proof idea

Definition and interface module, not a single end-to-end proof. It introduces the RS-admissibility predicate and supporting witnesses: existence of an admissible package, a concrete witness constructor, and monotonicity for the bridge constant. No deep tactic development is required at module scope; the mathematical load sits in stating the four conditions and marking the bridge as an external physical hypothesis rather than an internal RS derivation.

why it matters in Recognition Science

Without a sharp admissibility cut, the recognition path sum over triangulations is not a well-posed gravity object. This module supplies that cut for the Gravity domain: mesh, count, and growth controls plus the ratio-to-deficit bridge. It sits under the UV-finiteness program described in PathSumUVBound (sum over admissible $T$ on compact 4-manifolds with mesh $\ge\ell_{\mathrm{sub}}$).

The ASSUMED bridge is the honest seam: RS forcing (T0–T8, RCL, $\phi$) does not by itself produce $\log x_\sigma=\kappa\cdot\mathrm{deficit}+O(\mathrm{mesh}^3)$; gravity applications that quote admissibility inherit that physical hypothesis. Downstream use is currently thin in the graph (no recorded used_by edges), so the module is infrastructure for path-sum bounds rather than a leaf theorem in a finished chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)