Encyclopedia Gravity Gravity Admissible Triangulation Procedure Bridge Constant Monotone

ARTICLE 3 claims 2 theorems 1 model

Gravity Admissible Triangulation Procedure Bridge Constant Monotone

A machine-checked theorem shows that if a triangulation is allowed for gravity, then any larger error allowance is also allowed, a closure property that keeps the framework's bookkeeping consistent.

Verify this page

The bridge constant

A triangulation is a way of dividing a curved surface into flat pieces, like the facets of a geodesic dome. In Recognition Science, a framework that derives physical structure from a discrete record of recognition events, only certain triangulations are admissible for use in its path sum. The admissible ones must have a positive mesh size, a finite number of simplices, and a positive growth base. These three conditions are derived from the existing structure.

The fourth condition is different. It is the bridge: the logarithm of a recognition ratio must equal a constant times the deficit angle, plus an error term that shrinks with the cube of the mesh size. In plain terms, the bridge says that the bookkeeping distortion of a hinge is proportional to how much that hinge deviates from flatness, up to a small correction. This is an assumed physical hypothesis, not a derived theorem. It is the link between the abstract ledger and the geometry of gravity.

The theorem bridge_constant_monotone concerns the error constant in that bridge. It proves a closure fact: if a triangulation family is admissible with a certain error constant, then it remains admissible with any larger constant. The set of admissible error bounds is upward-closed. The proof is direct: the bridge inequality still holds when the right-hand side is made larger. This is a small but necessary consistency check, ensuring that the admissibility predicate does not depend on a fragile, exact choice of error bound.

The framework's library, a machine-checked collection of formal theorems, also provides a concrete witness that the admissibility conditions are satisfiable. That witness uses a recognition ratio equal to the exponential function, so the bridge holds exactly with error constant zero. The monotonicity theorem then guarantees that this witness remains admissible under any larger error allowance, a flexibility that keeps the framework's bookkeeping steady without changing its physical content.

What the theorem does not do is derive the bridge from first principles. The bridge remains an explicit assumption, a physical hypothesis about how recognition ratios relate to deficit angles. The monotonicity result only manages the error term around that assumption; it does not justify the assumption itself. The distinction is central to the framework's honesty: derived conditions are proved, assumed conditions are labeled as such.

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))
  }⟩
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
  }⟩

What this page does not claim

The bridge condition is derived from the framework's axioms. The monotonicity theorem justifies the physical assumption behind the bridge. The witness family represents a physically realistic triangulation of spacetime.

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