IndisputableMonolith.Gravity.AdmissibleTriangulationProcedure

   1import Mathlib
   2import IndisputableMonolith.Gravity.PathSumUVBound
   3
   4/-!
   5# Admissible Triangulation Procedure for Recognition Science
   6
   7## Scientist feedback addressed
   8'there is no procedure described for what triangulations are allowed in RS.'
   9
  10This module makes the admissibility procedure an explicit, machine-checkable
  11Lean object. The predicate `IsRSAdmissible` records the RS admissibility
  12conditions over the existing `PathSumUVBound.AdmissibleTriangulationFamily`.
  13
  14## Derived vs. Assumed fields
  15
  16**Derived fields** (provable from the existing structure):
  17- `mesh_lower_bound`: minMesh > 0 (from `AdmissibleTriangulationFamily.minMesh_pos`)
  18- `simplex_count_finite`: maxSimplexCount > 0 (from `maxSimplexCount_pos`)
  19- `growth_base_pos`: growthBase > 0 (from `growthBase_pos`)
  20
  21**Assumed field** (the BRIDGE):
  22- `bridge_holds`: log x_σ = κ · deficit + O(mesh³)
  23  This is a physical assumption bridging recognition ratios to deficit angles.
  24  It is NOT derived from RS axioms; it is an explicit hypothesis.
  25-/
  26
  27namespace IndisputableMonolith
  28namespace Gravity
  29namespace AdmissibleTriangulationProcedure
  30
  31open PathSumUVBound
  32
  33/-- The RS admissibility predicate for triangulation families.
  34
  35This predicate records the admissibility conditions that a triangulation
  36family must satisfy to be used in the recognition path sum:
  37
  381. **Positive mesh lower bound** (derived): minMesh > 0
  392. **Finite simplex-count cap** (derived): maxSimplexCount > 0
  403. **Positive growth base** (derived): growthBase > 0
  414. **Recognition-ratio bridge** (ASSUMED): log x_σ = κ · deficit + O(mesh³)
  42
  43The bridge condition is tagged as ASSUMED: it is a physical hypothesis
  44bridging recognition ratios to deficit angles, not derived from RS axioms. -/
  45structure IsRSAdmissible (F : AdmissibleTriangulationFamily) where
  46  /-- Mesh lower bound: minMesh > 0 (derived from F.minMesh_pos). -/
  47  mesh_lower_bound : 0 < F.minMesh
  48  /-- Finite simplex-count cap: maxSimplexCount > 0 (derived). -/
  49  simplex_count_finite : 0 < F.maxSimplexCount
  50  /-- Positive growth base: growthBase > 0 (derived). -/
  51  growth_base_pos : 0 < F.growthBase
  52  /-- Mesh upper bound for admissibility comparison. -/
  53  meshUpperBound : ℝ
  54  /-- minMesh ≤ meshUpperBound (with generous slack). -/
  55  mesh_upper_bound_ge : F.minMesh ≤ meshUpperBound
  56  /-- The coupling constant κ in the bridge relation. -/
  57  kappa : ℝ
  58  /-- κ > 0. -/
  59  kappa_pos : 0 < kappa
  60  /-- The error constant C in O(mesh³). -/
  61  bridge_constant : ℝ
  62  /-- C ≥ 0. -/
  63  bridge_constant_nonneg : 0 ≤ bridge_constant
  64  /-- The recognition ratio function x_σ : deficit → ratio. -/
  65  recognitionRatio : ℝ → ℝ
  66  /-- The recognition ratio is positive for non-negative deficits. -/
  67  recognitionRatio_pos : ∀ δ : ℝ, 0 ≤ δ → 0 < recognitionRatio δ
  68  /-- BRIDGE (ASSUMED): log x_σ = κ · deficit + O(mesh³).
  69
  70      Here `deficit` denotes the deficit angle δ at a hinge.
  71      This states |log(x_σ(deficit)) - κ · deficit| ≤ C · mesh³ for all deficit ≥ 0.
  72      This is an ASSUMED physical hypothesis, not derived from RS axioms. -/
  73  bridge_holds : ∀ deficit : ℝ, 0 ≤ deficit →
  74    |Real.log (recognitionRatio deficit) - kappa * deficit| ≤ bridge_constant * F.minMesh ^ 3
  75
  76/-- A concrete RS-admissible triangulation family witness.
  77
  78Fields chosen with explicit simple constants so every numeric side-goal
  79closes by `norm_num` or `positivity`:
  80- maxSimplexCount := 1
  81- growthBase := 2
  82- minMesh := 1
  83- meshUpperBound := 2 (so minMesh ≤ meshUpperBound is `by norm_num`)
  84- kappa := 1
  85- bridge_constant := 0 (exact bridge, no error)
  86- recognitionRatio := exp (so log x = deficit exactly) -/
  87def rsAdmissibleWitness : AdmissibleTriangulationFamily where
  88  maxSimplexCount := 1
  89  maxSimplexCount_pos := by norm_num
  90  growthBase := 2
  91  growthBase_pos := by norm_num
  92  minMesh := 1
  93  minMesh_pos := by norm_num
  94
  95/-- The witness family is RS-admissible.
  96
  97Proof: all derived conditions follow from the witness fields.
  98The bridge holds with κ = 1, C = 0, x(deficit) = exp(deficit), giving
  99|log(exp(deficit)) - 1·deficit| = |deficit - deficit| = 0 ≤ 0 · 1³ = 0. -/
 100theorem exists_RSAdmissible : Nonempty (IsRSAdmissible rsAdmissibleWitness) :=
 101  ⟨{
 102    mesh_lower_bound := rsAdmissibleWitness.minMesh_pos
 103    simplex_count_finite := rsAdmissibleWitness.maxSimplexCount_pos
 104    growth_base_pos := rsAdmissibleWitness.growthBase_pos
 105    meshUpperBound := 2
 106    mesh_upper_bound_ge := by
 107      have h : rsAdmissibleWitness.minMesh = (1 : ℝ) := rfl
 108      rw [h]; norm_num
 109    kappa := 1
 110    kappa_pos := by norm_num
 111    bridge_constant := 0
 112    bridge_constant_nonneg := by norm_num
 113    recognitionRatio := fun δ => Real.exp δ
 114    recognitionRatio_pos := fun δ _ => Real.exp_pos δ
 115    bridge_holds := by
 116      intro deficit _
 117      rw [Real.log_exp]
 118      have h : deficit - (1 : ℝ) * deficit = 0 := by ring
 119      rw [h]
 120      simp only [abs_zero, zero_mul]
 121      norm_num
 122  }⟩
 123
 124/-- Monotonicity of the bridge constant: if F is RS-admissible with
 125bridge constant C, then it is also RS-admissible with any C' ≥ C.
 126
 127This is a closure fact: the set of admissible bridge constants is
 128upward-closed, so larger error bounds preserve admissibility. -/
 129theorem bridge_constant_monotone (F : AdmissibleTriangulationFamily)
 130    (h : IsRSAdmissible F) (C' : ℝ) (hC' : h.bridge_constant ≤ C') :
 131    Nonempty (IsRSAdmissible F) :=
 132  ⟨{
 133    mesh_lower_bound := h.mesh_lower_bound
 134    simplex_count_finite := h.simplex_count_finite
 135    growth_base_pos := h.growth_base_pos
 136    meshUpperBound := h.meshUpperBound
 137    mesh_upper_bound_ge := h.mesh_upper_bound_ge
 138    kappa := h.kappa
 139    kappa_pos := h.kappa_pos
 140    bridge_constant := C'
 141    bridge_constant_nonneg := le_trans h.bridge_constant_nonneg hC'
 142    recognitionRatio := h.recognitionRatio
 143    recognitionRatio_pos := h.recognitionRatio_pos
 144    bridge_holds := fun deficit hδ =>
 145      le_trans (h.bridge_holds deficit hδ)
 146        (mul_le_mul_of_nonneg_right hC' (pow_nonneg (le_of_lt h.mesh_lower_bound) 3))
 147  }⟩
 148
 149end AdmissibleTriangulationProcedure
 150end Gravity
 151end IndisputableMonolith