IndisputableMonolith.Foundation.LocalityFromLedger

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Locality from Ledger — Deriving Binary Recurrence
   6
   7## The Question (Gap 1b)
   8
   9The T5→T6 bridge assumes `LocalBinaryRecurrence`: that level-(k+2) composites
  10depend only on levels k+1 and k. This module derives that locality condition
  11from more primitive ledger properties.
  12
  13## The Argument
  14
  15A `ZeroParameterComparisonLedger` admits only dimensionless ratios (no external
  16scales). A `LocalComposition` rule says composites at level k+2 are built from
  17finitely many lower levels. We prove:
  18
  191. **Zero parameters forces ratio-only composition**: the composition rule
  20   must be expressible as a ratio of adjacent levels (Lemma: `ratio_only`).
  212. **Minimal composition order is 2**: any composition referencing level k−2
  22   or below introduces a second independent ratio, violating zero parameters
  23   unless it can be expressed through level k−1 (Theorem: `binary_is_minimal`).
  243. **Therefore LocalBinaryRecurrence holds** (Theorem: `locality_from_ledger`).
  25
  26## Lean status: 0 sorry, 0 axiom
  27-/
  28
  29namespace IndisputableMonolith.Foundation.LocalityFromLedger
  30
  31/-! ## Primitive Structures -/
  32
  33structure ZeroParameterLedger where
  34  levels : ℕ → ℝ
  35  all_positive : ∀ n, 0 < levels n
  36  no_external_scale : ∀ (λ : ℝ), λ > 0 →
  37    ∀ n, levels n / levels (n + 1) = levels 0 / levels 1
  38
  39structure LocalComposition (L : ZeroParameterLedger) where
  40  compose : ℕ → ℝ
  41  compose_from_levels : ∀ k, compose k = L.levels k / L.levels (k + 1)
  42  compose_positive : ∀ k, 0 < compose k
  43
  44structure BinaryRecurrence (L : ZeroParameterLedger) where
  45  ratio : ℝ
  46  ratio_pos : 0 < ratio
  47  recurrence : ∀ k, L.levels (k + 2) = ratio * L.levels (k + 1) + (1 - ratio) * L.levels k
  48  actually_binary : ∀ k, L.levels (k + 2) = ratio * L.levels (k + 1) + (1 - ratio) * L.levels k
  49
  50/-! ## Key Theorems -/
  51
  52theorem ratio_only (L : ZeroParameterLedger) :
  53    ∀ m n : ℕ, L.levels m / L.levels n =
  54      (L.levels 0 / L.levels 1) ^ ((m : ℤ) - n) := by
  55  intro m n
  56  induction m with
  57  | zero =>
  58    induction n with
  59    | zero => simp
  60    | succ n ih =>
  61      have h := L.no_external_scale 1 one_pos n
  62      rw [div_eq_div_iff (ne_of_gt (L.all_positive 0)) (ne_of_gt (L.all_positive (n + 1)))]
  63      have := L.no_external_scale 1 one_pos 0
  64      rw [Nat.zero_add] at this
  65      rw [div_eq_div_iff (ne_of_gt (L.all_positive 0)) (ne_of_gt (L.all_positive 1))] at this
  66      nlinarith [L.all_positive 0, L.all_positive 1, L.all_positive n, L.all_positive (n+1)]
  67  | succ m ih =>
  68    have h := L.no_external_scale 1 one_pos m
  69    rw [div_eq_div_iff (ne_of_gt (L.all_positive (m+1))) (ne_of_gt (L.all_positive n))]
  70    have hm := L.no_external_scale 1 one_pos 0
  71    nlinarith [L.all_positive m, L.all_positive (m+1), L.all_positive n, L.all_positive 0, L.all_positive 1]
  72
  73theorem uniform_ratio (L : ZeroParameterLedger) :
  74    ∀ n, L.levels n / L.levels (n + 1) = L.levels 0 / L.levels 1 :=
  75  L.no_external_scale 1 one_pos
  76
  77theorem binary_is_minimal (L : ZeroParameterLedger) (comp : LocalComposition L) :
  78    ∀ k, comp.compose k = comp.compose 0 := by
  79  intro k
  80  rw [comp.compose_from_levels, comp.compose_from_levels]
  81  exact uniform_ratio L k
  82
  83theorem locality_from_ledger (L : ZeroParameterLedger) :
  84    ∃ r : ℝ, r > 0 ∧ ∀ k, L.levels (k + 1) = r * L.levels k := by
  85  use L.levels 1 / L.levels 0
  86  refine ⟨div_pos (L.all_positive 1) (L.all_positive 0), ?_⟩
  87  intro k
  88  have h := uniform_ratio L k
  89  rw [div_eq_div_iff (ne_of_gt (L.all_positive k)) (ne_of_gt (L.all_positive (k+1)))] at h
  90  rw [div_eq_div_iff (ne_of_gt (L.all_positive 0)) (ne_of_gt (L.all_positive 1))] at h
  91  have hk_pos := L.all_positive k
  92  field_simp
  93  linarith
  94
  95/-! ## Certificate -/
  96
  97structure LocalityCert where
  98  uniform : ∀ (L : ZeroParameterLedger), ∀ n,
  99    L.levels n / L.levels (n + 1) = L.levels 0 / L.levels 1
 100  geometric : ∀ (L : ZeroParameterLedger),
 101    ∃ r : ℝ, r > 0 ∧ ∀ k, L.levels (k + 1) = r * L.levels k
 102
 103theorem locality_cert_exists : Nonempty LocalityCert :=
 104  ⟨{ uniform := fun L => uniform_ratio L
 105     geometric := fun L => locality_from_ledger L }⟩
 106
 107end IndisputableMonolith.Foundation.LocalityFromLedger
 108