Encyclopedia Gravity Gravity Admissible Triangulation Procedure

ARTICLE 3 claims 2 theorems 1 model

Gravity Admissible Triangulation Procedure

A triangulation is a way to build curved space from flat pieces; this procedure says which such constructions Recognition Science may use.

Verify this page

Admissible triangulation

A triangulation is a way to build a curved surface or space from flat triangular pieces, the way a geodesic dome is built from flat panels. In general relativity, Regge calculus uses this idea to approximate curved spacetime by a mesh of flat simplices, with curvature concentrated along the hinges where the pieces meet. The key quantity is the deficit angle, the amount by which the flat pieces fail to close around a hinge; a positive deficit angle means positive curvature there.

Recognition Science (RS) needs triangulations for its recognition path sum, a sum over ways reality might keep a discrete record of events. The gravity admissible triangulation procedure is the explicit, machine-checkable rule for which triangulation families may enter that sum. The rule is a predicate called IsRSAdmissible, defined in the framework's machine-checked library of formal theorems. It records four conditions: the mesh size has a positive lower bound, the number of simplices is capped at a finite positive number, the growth base is positive, and a bridge relation holds between recognition ratios and deficit angles.

The first three conditions are derived from the existing triangulation structure, so they are theorems. The fourth, the bridge, is different. It states that the logarithm of the recognition ratio equals a constant kappa times the deficit angle, plus an error term of order mesh cubed. In plain language: the ratio of recognition weights across a hinge grows exponentially with the curvature there, and the approximation improves as the mesh shrinks. The docstring tags this as ASSUMED, a physical hypothesis, not something the framework's axioms force. This is the load-bearing assumption that connects the discrete ledger of recognition events to the geometry of curved space.

The module also proves that such admissible families exist. It constructs one explicit witness with simple constants: one simplex, growth base two, mesh size one, kappa equal to one, and recognition ratio equal to the exponential function, so the bridge holds exactly with zero error. The theorem exists_RSAdmissible establishes that this witness satisfies the predicate. A second theorem, bridge_constant_monotone, shows that if a family is admissible with a given error constant, it remains admissible with any larger constant; the set of admissible error bounds is upward closed.

What this establishes in plain terms is a precise, checkable answer to the question of which triangulations Recognition Science allows. The procedure does not invent new physics; it makes the admissibility conditions explicit and machine-checkable, and it flags the one physical assumption that the framework cannot derive. The consequence is that any later result built on an RS-admissible triangulation carries its own warrant: the derived conditions are proved, and the bridge is stated as a hypothesis with its error term visible.

MODEL IsRSAdmissible · IndisputableMonolith/Gravity/AdmissibleTriangulationProcedure.lean
IsRSAdmissible · IndisputableMonolith/Gravity/AdmissibleTriangulationProcedure.lean:33 
/-- The RS admissibility predicate for triangulation families.

This predicate records the admissibility conditions that a triangulation
family must satisfy to be used in the recognition path sum:

1. **Positive mesh lower bound** (derived): minMesh > 0
2. **Finite simplex-count cap** (derived): maxSimplexCount > 0
3. **Positive growth base** (derived): growthBase > 0
4. **Recognition-ratio bridge** (ASSUMED): log x_σ = κ · deficit + O(mesh³)

The bridge condition is tagged as ASSUMED: it is a physical hypothesis
bridging recognition ratios to deficit angles, not derived from RS axioms. -/
structure IsRSAdmissible (F : AdmissibleTriangulationFamily) where
  /-- Mesh lower bound: minMesh > 0 (derived from F.minMesh_pos). -/
  mesh_lower_bound : 0 < F.minMesh
  /-- Finite simplex-count cap: maxSimplexCount > 0 (derived). -/
  simplex_count_finite : 0 < F.maxSimplexCount
  /-- Positive growth base: growthBase > 0 (derived). -/
  growth_base_pos : 0 < F.growthBase
  /-- Mesh upper bound for admissibility comparison. -/
  meshUpperBound : ℝ
  /-- minMesh ≤ meshUpperBound (with generous slack). -/
  mesh_upper_bound_ge : F.minMesh ≤ meshUpperBound
  /-- The coupling constant κ in the bridge relation. -/
  kappa : ℝ
  /-- κ > 0. -/
  kappa_pos : 0 < kappa
  /-- The error constant C in O(mesh³). -/
  bridge_constant : ℝ
  /-- C ≥ 0. -/
  bridge_constant_nonneg : 0 ≤ bridge_constant
  /-- The recognition ratio function x_σ : deficit → ratio. -/
  recognitionRatio : ℝ → ℝ
  /-- The recognition ratio is positive for non-negative deficits. -/
  recognitionRatio_pos : ∀ δ : ℝ, 0 ≤ δ → 0 < recognitionRatio δ
  /-- BRIDGE (ASSUMED): log x_σ = κ · deficit + O(mesh³).

      Here `deficit` denotes the deficit angle δ at a hinge.
      This states |log(x_σ(deficit)) - κ · deficit| ≤ C · mesh³ for all deficit ≥ 0.
      This is an ASSUMED physical hypothesis, not derived from RS axioms. -/
  bridge_holds : ∀ deficit : ℝ, 0 ≤ deficit →
    |Real.log (recognitionRatio deficit) - kappa * deficit| ≤ bridge_constant * F.minMesh ^ 3
THEOREM exists_RSAdmissible · IndisputableMonolith/Gravity/AdmissibleTriangulationProcedure.lean
exists_RSAdmissible · IndisputableMonolith/Gravity/AdmissibleTriangulationProcedure.lean:95 
/-- The witness family is RS-admissible.

Proof: all derived conditions follow from the witness fields.
The bridge holds with κ = 1, C = 0, x(deficit) = exp(deficit), giving
|log(exp(deficit)) - 1·deficit| = |deficit - deficit| = 0 ≤ 0 · 1³ = 0. -/
theorem exists_RSAdmissible : Nonempty (IsRSAdmissible rsAdmissibleWitness) :=
  ⟨{
    mesh_lower_bound := rsAdmissibleWitness.minMesh_pos
    simplex_count_finite := rsAdmissibleWitness.maxSimplexCount_pos
    growth_base_pos := rsAdmissibleWitness.growthBase_pos
    meshUpperBound := 2
    mesh_upper_bound_ge := by
      have h : rsAdmissibleWitness.minMesh = (1 : ℝ) := rfl
      rw [h]; norm_num
    kappa := 1
    kappa_pos := by norm_num
    bridge_constant := 0
    bridge_constant_nonneg := by norm_num
    recognitionRatio := fun δ => Real.exp δ
    recognitionRatio_pos := fun δ _ => Real.exp_pos δ
    bridge_holds := by
      intro deficit _
      rw [Real.log_exp]
      have h : deficit - (1 : ℝ) * deficit = 0 := by ring
      rw [h]
      simp only [abs_zero, zero_mul]
      norm_num
  }⟩
THEOREM bridge_constant_monotone · IndisputableMonolith/Gravity/AdmissibleTriangulationProcedure.lean
bridge_constant_monotone · IndisputableMonolith/Gravity/AdmissibleTriangulationProcedure.lean:124 
/-- Monotonicity of the bridge constant: if F is RS-admissible with
bridge constant C, then it is also RS-admissible with any C' ≥ C.

This is a closure fact: the set of admissible bridge constants is
upward-closed, so larger error bounds preserve admissibility. -/
theorem bridge_constant_monotone (F : AdmissibleTriangulationFamily)
    (h : IsRSAdmissible F) (C' : ℝ) (hC' : h.bridge_constant ≤ C') :
    Nonempty (IsRSAdmissible F) :=
  ⟨{
    mesh_lower_bound := h.mesh_lower_bound
    simplex_count_finite := h.simplex_count_finite
    growth_base_pos := h.growth_base_pos
    meshUpperBound := h.meshUpperBound
    mesh_upper_bound_ge := h.mesh_upper_bound_ge
    kappa := h.kappa
    kappa_pos := h.kappa_pos
    bridge_constant := C'
    bridge_constant_nonneg := le_trans h.bridge_constant_nonneg hC'
    recognitionRatio := h.recognitionRatio
    recognitionRatio_pos := h.recognitionRatio_pos
    bridge_holds := fun deficit hδ =>
      le_trans (h.bridge_holds deficit hδ)
        (mul_le_mul_of_nonneg_right hC' (pow_nonneg (le_of_lt h.mesh_lower_bound) 3))
  }⟩

What this page does not claim

The bridge relation is not derived from RS axioms; it is an explicit physical hypothesis. This procedure does not by itself derive the Einstein field equations from Recognition Science. The witness family with exponential recognition ratio is a consistency example, not a claim about physical gravity.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/AdmissibleTriangulationProcedure.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND