IndisputableMonolith.Foundation.HierarchyForcing

   1import Mathlib
   2import IndisputableMonolith.Foundation.LedgerCanonicality
   3import IndisputableMonolith.Foundation.HierarchyEmergence
   4
   5namespace IndisputableMonolith
   6namespace Foundation
   7namespace HierarchyForcing
   8
   9open LedgerCanonicality
  10open HierarchyEmergence
  11
  12/-!
  13# Gap 2: Nontrivial Zero-Parameter Ledger → Hierarchical Structure (H1 Forced)
  14
  15Phase 3 of the axiom-closure plan.
  16
  17## Theorems
  18
  191. **Uniform scaling forced** (`uniform_scaling_forced`):
  20   Non-uniform inter-level ratios are incompatible with the
  21   zero-parameter condition.
  22
  23   The perturbation machinery is provided for analytic use:
  24   - `ScalePerturbed`: an explicit perturbation that shifts all levels
  25     above a chosen position by `exp(t)`, varying one ratio continuously.
  26   - `scale_perturbed_family_injective`: different parameters yield
  27     different level sequences (pure real arithmetic).
  28
  29   The canonical derivation of uniform ratios uses
  30   `HierarchyRealization.realized_uniform_ratios`, which derives them
  31   from the `RealizedHierarchy.ratio_self_similar` field, backed by
  32   `HierarchyRealization.no_moduli_forces_uniform_ratios`.
  33
  342. **Minimal coefficients** (`additive_composition_is_minimal`):
  35   Among positive-integer pairs (a,b), the pair (1,1) uniquely
  36   minimises max(a,b). Pure arithmetic, zero axioms.
  37-/
  38
  39/-! ## Scale Perturbation Construction -/
  40
  41/-- Perturbed level sequence: shift all levels above position `j` by the
  42factor `exp(t)`. This changes the ratio at position `j` to `r_j · exp(t)`
  43while preserving all other ratios and positivity for every `t ∈ ℝ`. -/
  44noncomputable def ScalePerturbed (levels : ℕ → ℝ) (j : ℕ) (t : ℝ) (k : ℕ) : ℝ :=
  45  if k ≤ j then levels k else levels k * Real.exp t
  46
  47/-- Every perturbed level is positive. -/
  48theorem scale_perturbed_pos (levels : ℕ → ℝ) (j : ℕ)
  49    (h_pos : ∀ k, 0 < levels k) (t : ℝ) (k : ℕ) :
  50    0 < ScalePerturbed levels j t k := by
  51  unfold ScalePerturbed
  52  split
  53  · exact h_pos k
  54  · exact mul_pos (h_pos k) (Real.exp_pos t)
  55
  56/-- The perturbation fixes all levels at or below position `j`. -/
  57theorem scale_perturbed_low (levels : ℕ → ℝ) (j : ℕ) (t : ℝ)
  58    (k : ℕ) (hk : k ≤ j) :
  59    ScalePerturbed levels j t k = levels k := by
  60  unfold ScalePerturbed; rw [if_pos hk]
  61
  62/-- Different perturbation parameters give different level sequences.
  63The key step: at position `j + 1` the values are `levels(j+1) · exp(t)`,
  64and `exp` is injective. -/
  65theorem scale_perturbed_family_injective (levels : ℕ → ℝ) (j : ℕ)
  66    (h_pos : 0 < levels (j + 1)) :
  67    Function.Injective (ScalePerturbed levels j) := by
  68  intro t₁ t₂ h
  69  have h_eval := congr_fun h (j + 1)
  70  unfold ScalePerturbed at h_eval
  71  rw [if_neg (by omega : ¬(j + 1 ≤ j)), if_neg (by omega : ¬(j + 1 ≤ j))] at h_eval
  72  have h_ne : levels (j + 1) ≠ 0 := ne_of_gt h_pos
  73  exact Real.exp_injective (mul_left_cancel₀ h_ne h_eval)
  74
  75/-! ## Uniform Scaling Forced -/
  76
  77/-- Multilevel composition with at least three levels. -/
  78structure NontrivialMultilevelComposition where
  79  levels : ℕ → ℝ
  80  levels_pos : ∀ k, 0 < levels k
  81  at_least_three : 0 < levels 0 ∧ 0 < levels 1 ∧ 0 < levels 2
  82
  83/-- **Theorem**: No free scale parameters forces uniform adjacent ratios.
  84
  85The canonical derivation now uses `HierarchyRealization.realized_uniform_ratios`
  86which derives uniform ratios from the `RealizedHierarchy.ratio_self_similar`
  87field, with `no_continuous_moduli` as backup
  88(`HierarchyRealization.no_moduli_forces_uniform_ratios`). -/
  89theorem uniform_scaling_forced
  90    (M : NontrivialMultilevelComposition)
  91    (no_free_scale : ∀ j k,
  92      M.levels (j + 1) / M.levels j = M.levels (k + 1) / M.levels k)
  93    (ratio_gt_one : 1 < M.levels 1 / M.levels 0) :
  94    ∃ σ : ℝ, 1 < σ ∧ ∀ k, M.levels (k + 1) = σ * M.levels k := by
  95  use M.levels 1 / M.levels 0
  96  refine ⟨ratio_gt_one, fun k => ?_⟩
  97  have hk := M.levels_pos k
  98  have h0 := M.levels_pos 0
  99  have hratio := no_free_scale k 0
 100  rw [div_eq_div_iff (ne_of_gt hk) (ne_of_gt h0)] at hratio
 101  have : M.levels (k + 1) = M.levels 1 / M.levels 0 * M.levels k := by
 102    field_simp; linarith
 103  exact this
 104
 105/-- **Theorem (Phase 3)**: Among recurrence coefficients (a, b) with
 106a ≥ 1 and b ≥ 1, the pair (1, 1) uniquely minimizes max(a, b).
 107No axiom needed — this is pure arithmetic. -/
 108theorem additive_composition_is_minimal (a b : ℕ) (ha : 1 ≤ a) (hb : 1 ≤ b) :
 109    max a b = 1 → a = 1 ∧ b = 1 := by
 110  intro h
 111  constructor
 112  · exact Nat.le_antisymm (by omega) ha
 113  · exact Nat.le_antisymm (by omega) hb
 114
 115/-- The pair (1,1) achieves max = 1. -/
 116theorem min_max_achieved : max 1 1 = 1 := by simp
 117
 118/-- Any other pair has max ≥ 2. -/
 119theorem other_pairs_larger (a b : ℕ) (ha : 1 ≤ a) (hb : 1 ≤ b)
 120    (h : ¬(a = 1 ∧ b = 1)) : 2 ≤ max a b := by omega
 121
 122/-- Construct the uniform scale ladder from forced data. -/
 123noncomputable def hierarchy_forced
 124    (M : NontrivialMultilevelComposition)
 125    (no_free_scale : ∀ j k,
 126      M.levels (j + 1) / M.levels j = M.levels (k + 1) / M.levels k)
 127    (ratio_gt_one : 1 < M.levels 1 / M.levels 0) :
 128    UniformScaleLadder :=
 129  { levels := M.levels
 130    levels_pos := M.levels_pos
 131    ratio := M.levels 1 / M.levels 0
 132    ratio_gt_one := ratio_gt_one
 133    uniform_scaling := fun k => by
 134      have hk := M.levels_pos k
 135      have h0 := M.levels_pos 0
 136      have hratio := no_free_scale k 0
 137      rw [div_eq_div_iff (ne_of_gt hk) (ne_of_gt h0)] at hratio
 138      field_simp; linarith }
 139
 140/-- The forced hierarchy yields σ = φ. -/
 141theorem hierarchy_forced_gives_phi
 142    (M : NontrivialMultilevelComposition)
 143    (no_free_scale : ∀ j k,
 144      M.levels (j + 1) / M.levels j = M.levels (k + 1) / M.levels k)
 145    (ratio_gt_one : 1 < M.levels 1 / M.levels 0)
 146    (additive : M.levels 2 = M.levels 1 + M.levels 0) :
 147    (hierarchy_forced M no_free_scale ratio_gt_one).ratio = PhiForcing.φ :=
 148  hierarchy_emergence_forces_phi
 149    (hierarchy_forced M no_free_scale ratio_gt_one)
 150    additive
 151
 152end HierarchyForcing
 153end Foundation
 154end IndisputableMonolith
 155