Encyclopedia Gravity Gravity Admissible Triangulation Procedure Is Rsadmissible

ARTICLE 3 claims 2 theorems 1 model

Gravity Admissible Triangulation Procedure Is Rsadmissible

A machine-checked definition that separates provable geometric facts from one explicit physical assumption in Recognition Science's gravity procedure.

Verify this page

The admissibility predicate

In Recognition Science, the path from discrete recognition events to continuous gravity runs through triangulations: ways of chopping a curved shape into flat pieces, like a geodesic dome. The declaration IsRSAdmissible is a formal predicate, a machine-checkable checklist, that says which triangulation families are allowed to appear in the recognition path sum. It does not invent new physics. It records, in the framework's machine-checked library of formal theorems, exactly which conditions are proved and which one is assumed.

Three of the conditions are derived facts, provable from the underlying structure of an admissible triangulation family. The mesh lower bound is positive, meaning the smallest piece has nonzero size. The simplex-count cap is finite, so no family uses infinitely many pieces. The growth base is positive, so the family does not shrink to nothing. These are not assumptions; they follow from the definition of the family itself.

The fourth condition is the bridge, and it is the load-bearing assumption. It states that the logarithm of a recognition ratio, written log x_σ, equals a constant κ times the deficit angle δ, plus an error term of order mesh³. In plain words: the way recognition ratios change with curvature is proportional to the deficit angle, up to a small correction that shrinks as the mesh gets finer. The docstring is explicit that this is an ASSUMED physical hypothesis, not derived from RS axioms. It is the bridge that connects the discrete recognition ledger to the continuous geometry of deficit angles.

The library also proves two closure facts. One shows that a witness family exists: a concrete triangulation family with simple constants, maxSimplexCount = 1, growthBase = 2, minMesh = 1, that satisfies all four conditions, including the bridge with κ = 1 and zero error. The other shows monotonicity: if a family is admissible with error constant C, it remains admissible with any larger C'. Larger error bounds preserve admissibility. These are formal theorems, checked by the kernel, and they establish that the predicate is not empty and behaves sensibly under loosening.

What the declaration does not claim is just as important. It does not prove that the bridge holds for any real physical system; that remains a hypothesis, named and explicit, to be tested against the world. It does not derive the value of κ or the form of the recognition ratio from first principles. It does not claim that every triangulation family is admissible, only that the predicate is satisfiable and monotone. The procedure is a scaffold, not a theory of gravity by itself.

THEOREM 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
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 · bridge_constant_monotone · 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
  }⟩
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 hypothesis is not proved for any physical system. The value of κ is not derived from Recognition Science axioms. The predicate does not assert that all triangulation families are admissible.

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