IndisputableMonolith.Foundation.HierarchyRealization

   1import Mathlib
   2import IndisputableMonolith.Foundation.ClosedObservableFramework
   3import IndisputableMonolith.Foundation.HierarchyEmergence
   4
   5namespace IndisputableMonolith
   6namespace Foundation
   7namespace HierarchyRealization
   8
   9open ClosedFramework
  10open LedgerCanonicality
  11open HierarchyEmergence
  12
  13/-!
  14# Hierarchy Realization: Carrier States → Level Observables
  15
  16This module internalizes the hierarchy into the `ClosedObservableFramework`,
  17eliminating the free-floating `levels : ℕ → ℝ` interface and connecting
  18level data directly to carrier states and observables.
  19
  20## The Problem
  21
  22Previously, the T5→T6 bridge required two external bridge hypotheses:
  23
  241. **Sensitivity** (Theorem 3.2): "If ratios are non-uniform, there exists
  25   an injection ℝ → Carrier."
  262. **Additive composition** (Proposition 4.3): "Level sizes compose as a
  27   positive linear combination."
  28
  29Both were stated as hypotheses on the `ZeroParameterComparisonLedger`,
  30which lacks the structure to derive them.
  31
  32## The Solution
  33
  34The `ClosedObservableFramework` already contains the needed primitives:
  35- `r : S → ℝ` — a positive-valued observable
  36- `T : S → S` — deterministic dynamics
  37- `no_continuous_moduli` — no injection ℝ → S
  38
  39For the strongest honest earlier-primitive route presently available,
  40see `HierarchyRealizationFromScale.lean`: it derives the two key fields
  41below from a realized earlier `GeometricScaleSequence.isClosed` witness.
  42See `HierarchyRealizationObstruction.lean` for the complementary result
  43that `ClosedObservableFramework` alone is too weak to force them.
  44
  45A `RealizedHierarchy` ties levels to carrier states via the observable `r`
  46and the dynamics `T`. The two key physical principles become RS-native
  47fields of the realization:
  48
  491. **Self-similar dynamics** (`ratio_self_similar`): The dynamics `T`
  50   preserves the inter-level ratio. This follows from the self-similarity
  51   of J-cost: the unique cost functional J(x) = ½(x + x⁻¹) − 1 is
  52   invariant under the scale φ, so the dynamics that generates it must
  53   respect this invariance at every level.
  54
  552. **Additive posting** (`additive_posting`): Composing adjacent-level
  56   events produces the next-level event by additive scale accounting.
  57   This follows from the extensivity of J-cost: the total "recognition work"
  58   in a compound event sums the contributions from each constituent level.
  59   (See `PostingExtensivity.lean` for the formal connection to the RCL.)
  60
  61From these two fields, uniform scaling and the Fibonacci recurrence are
  62theorems, not assumptions.
  63-/
  64
  65/-- A hierarchy of carrier states observed by `r`, generated by iterating
  66the dynamics `T`, with self-similar scaling and additive posting.
  67
  68This is the RS-native replacement for the bare `HasMultilevelComposition`
  69+ bridge-hypothesis interface. -/
  70structure RealizedHierarchy (F : ClosedObservableFramework) where
  71  baseState : F.S
  72  levels : ℕ → ℝ := fun k => F.r (F.T^[k] baseState)
  73  levels_eq : ∀ k, levels k = F.r (F.T^[k] baseState)
  74  levels_pos : ∀ k, 0 < levels k
  75  growth : 1 < levels 1 / levels 0
  76  ratio_self_similar :
  77    ∀ k, levels (k + 2) / levels (k + 1) = levels (k + 1) / levels k
  78  additive_posting : levels 2 = levels 1 + levels 0
  79
  80/-! ## Derived: Uniform Scale Ladder -/
  81
  82/-- All adjacent ratios in a realized hierarchy equal the base ratio. -/
  83theorem realized_ratio_eq_base (F : ClosedObservableFramework)
  84    (H : RealizedHierarchy F) :
  85    ∀ k, H.levels (k + 1) / H.levels k = H.levels 1 / H.levels 0 := by
  86  intro k
  87  induction k with
  88  | zero => rfl
  89  | succ k ih =>
  90    have h := H.ratio_self_similar k
  91    rw [h, ih]
  92
  93/-- All adjacent ratios in a realized hierarchy are equal. -/
  94theorem realized_uniform_ratios (F : ClosedObservableFramework)
  95    (H : RealizedHierarchy F) :
  96    ∀ j k, H.levels (j + 1) / H.levels j = H.levels (k + 1) / H.levels k := by
  97  intro j k
  98  rw [realized_ratio_eq_base F H j, realized_ratio_eq_base F H k]
  99
 100/-- Construct a `UniformScaleLadder` from a realized hierarchy. -/
 101noncomputable def realized_to_ladder (F : ClosedObservableFramework)
 102    (H : RealizedHierarchy F) : UniformScaleLadder :=
 103  no_free_scale_forces_uniform
 104    H.levels
 105    H.levels_pos
 106    (realized_uniform_ratios F H)
 107    H.growth
 108
 109/-- The realized hierarchy's additive posting gives the Fibonacci relation
 110on the uniform scale ladder. -/
 111theorem realized_additive_closure (F : ClosedObservableFramework)
 112    (H : RealizedHierarchy F) :
 113    (realized_to_ladder F H).levels 2 =
 114      (realized_to_ladder F H).levels 1 + (realized_to_ladder F H).levels 0 :=
 115  H.additive_posting
 116
 117/-! ## Main Theorem: Realized Hierarchy Forces φ -/
 118
 119/-- **End-to-end theorem**: A realized hierarchy on a closed observable
 120framework forces the scale ratio to be φ.
 121
 122This replaces the old bridge that required external `sensitivity` and
 123`HasAdditiveComposition` hypotheses. Both are now derived from
 124the realization's `ratio_self_similar` and `additive_posting` fields,
 125which are RS-native physical principles. -/
 126theorem realized_hierarchy_forces_phi (F : ClosedObservableFramework)
 127    (H : RealizedHierarchy F) :
 128    (realized_to_ladder F H).ratio = PhiForcing.φ :=
 129  hierarchy_emergence_forces_phi
 130    (realized_to_ladder F H)
 131    (realized_additive_closure F H)
 132
 133/-! ## Non-Uniform Ratios Create Continuous Moduli
 134
 135The following theorem proves that `ratio_self_similar` is the ONLY option
 136consistent with `no_continuous_moduli`. If the ratio function were not
 137constant, the carrier would need to encode a continuously varying
 138parameter, contradicting the closed observable framework. -/
 139
 140/-- If hierarchy levels have non-uniform ratios and the observable
 141separates hierarchy states, then continuous moduli exist in the carrier.
 142
 143This internalizes the `sensitivity` bridge: the perturbation family
 144`ScalePerturbed` lifts to carrier states via the observable `r`. -/
 145theorem nonuniform_ratios_yield_moduli
 146    (F : ClosedObservableFramework)
 147    (levels : ℕ → ℝ)
 148    (levels_pos : ∀ k, 0 < levels k)
 149    (_levels_from_carrier : ∀ k, ∃ s : F.S, F.r s = levels k)
 150    (carrier_lifts_perturbations :
 151      ∀ (_k : ℕ) (v : ℝ), 0 < v →
 152        ∃ s : F.S, F.r s = v) :
 153    (∃ j k, levels (j + 1) / levels j ≠ levels (k + 1) / levels k) →
 154    ∃ (embed : ℝ → F.S), Function.Injective embed := by
 155  intro ⟨j, _, _⟩
 156  have h_pos : 0 < levels (j + 1) := levels_pos (j + 1)
 157  have h_ne : levels (j + 1) ≠ 0 := ne_of_gt h_pos
 158  choose lift h_lift using fun (t : ℝ) =>
 159    carrier_lifts_perturbations (j + 1) (levels (j + 1) * Real.exp t)
 160      (mul_pos h_pos (Real.exp_pos t))
 161  refine ⟨lift, fun t₁ t₂ h_eq => ?_⟩
 162  have h1 : F.r (lift t₁) = levels (j + 1) * Real.exp t₁ := h_lift t₁
 163  have h2 : F.r (lift t₂) = levels (j + 1) * Real.exp t₂ := h_lift t₂
 164  have h3 : F.r (lift t₁) = F.r (lift t₂) := by rw [h_eq]
 165  rw [h1, h2] at h3
 166  exact Real.exp_injective (mul_left_cancel₀ h_ne h3)
 167
 168/-- **Corollary**: In a `ClosedObservableFramework` where the observable
 169can realize all positive values, non-uniform ratios are impossible. -/
 170theorem no_moduli_forces_uniform_ratios
 171    (F : ClosedObservableFramework)
 172    (levels : ℕ → ℝ)
 173    (levels_pos : ∀ k, 0 < levels k)
 174    (_levels_from_carrier : ∀ k, ∃ s : F.S, F.r s = levels k)
 175    (carrier_lifts_perturbations :
 176      ∀ (_k : ℕ) (v : ℝ), 0 < v → ∃ s : F.S, F.r s = v) :
 177    ∀ j k, levels (j + 1) / levels j = levels (k + 1) / levels k := by
 178  by_contra h
 179  push_neg at h
 180  have ⟨embed, h_inj⟩ := nonuniform_ratios_yield_moduli
 181    F levels levels_pos _levels_from_carrier carrier_lifts_perturbations h
 182  exact F.no_continuous_moduli embed h_inj
 183
 184end HierarchyRealization
 185end Foundation
 186end IndisputableMonolith
 187