IndisputableMonolith.Foundation.HierarchyRealizationFromScale

   1import Mathlib
   2import IndisputableMonolith.Foundation.HierarchyRealization
   3
   4namespace IndisputableMonolith
   5namespace Foundation
   6namespace HierarchyRealizationFromScale
   7
   8open ClosedFramework
   9open HierarchyRealization
  10open PhiForcingDerived
  11
  12/-!
  13# Deriving Realized-Hierarchy Fields from Earlier Scale Primitives
  14
  15This module isolates the strongest honest derivation currently supported
  16by the codebase.
  17
  18If a `ClosedObservableFramework` orbit realizes an earlier
  19`GeometricScaleSequence` that is closed under `ledgerCompose`, then the
  20two target fields of `RealizedHierarchy`
  21
  22* `ratio_self_similar`
  23* `additive_posting`
  24
  25are theorems rather than assumptions.
  26
  27What remains genuinely open is proving that such a realized closed scale
  28model exists from `ClosedObservableFramework` alone.
  29-/
  30
  31/-- A `ClosedObservableFramework` orbit that realizes an earlier closed
  32geometric scale sequence. -/
  33structure RealizedClosedScaleModel (F : ClosedObservableFramework) where
  34  baseState : F.S
  35  amplitude : ℝ
  36  amplitude_pos : 0 < amplitude
  37  scales : GeometricScaleSequence
  38  scales_closed : scales.isClosed
  39  growth : 1 < scales.ratio
  40  realize : ∀ k, F.r (F.T^[k] baseState) = amplitude * scales.scale k
  41
  42/-- In any geometric scale sequence, each adjacent ratio equals the
  43base ratio. -/
  44theorem scale_step_ratio (S : GeometricScaleSequence) (k : ℕ) :
  45    S.scale (k + 1) / S.scale k = S.ratio := by
  46  unfold GeometricScaleSequence.scale
  47  rw [pow_succ]
  48  have hr : S.ratio ≠ 0 := ne_of_gt S.ratio_pos
  49  have hk : S.ratio ^ k ≠ 0 := pow_ne_zero k hr
  50  simpa using (mul_div_cancel_left₀ S.ratio hk)
  51
  52/-- The realized orbit has constant adjacent ratio. -/
  53theorem realized_closed_scale_ratio_step
  54    (F : ClosedObservableFramework) (H : RealizedClosedScaleModel F) (k : ℕ) :
  55    F.r (F.T^[k + 1] H.baseState) / F.r (F.T^[k] H.baseState) = H.scales.ratio := by
  56  rw [H.realize (k + 1), H.realize k]
  57  have ha : H.amplitude ≠ 0 := ne_of_gt H.amplitude_pos
  58  calc
  59    H.amplitude * H.scales.scale (k + 1) / (H.amplitude * H.scales.scale k)
  60      = H.scales.scale (k + 1) / H.scales.scale k := by
  61          rw [mul_div_mul_left _ _ ha]
  62    _ = H.scales.ratio := scale_step_ratio H.scales k
  63
  64/-- Therefore the realized orbit satisfies ratio self-similarity. -/
  65theorem ratio_self_similar_of_realized_closed_scale
  66    (F : ClosedObservableFramework) (H : RealizedClosedScaleModel F) :
  67    ∀ k,
  68      F.r (F.T^[k + 2] H.baseState) / F.r (F.T^[k + 1] H.baseState) =
  69        F.r (F.T^[k + 1] H.baseState) / F.r (F.T^[k] H.baseState) := by
  70  intro k
  71  rw [realized_closed_scale_ratio_step F H (k + 1), realized_closed_scale_ratio_step F H k]
  72
  73/-- Closure of the earlier geometric scale sequence yields additive
  74posting on the realized orbit. -/
  75theorem additive_posting_of_realized_closed_scale
  76    (F : ClosedObservableFramework) (H : RealizedClosedScaleModel F) :
  77    F.r (F.T^[2] H.baseState) =
  78      F.r (F.T^[1] H.baseState) + F.r (F.T^[0] H.baseState) := by
  79  have hclosed : H.scales.scale 0 + H.scales.scale 1 = H.scales.scale 2 := by
  80    simpa [GeometricScaleSequence.isClosed, ledgerCompose] using H.scales_closed
  81  have hclosed' : H.scales.scale 2 = H.scales.scale 1 + H.scales.scale 0 := by
  82    linarith
  83  rw [H.realize 2, H.realize 1, H.realize 0]
  84  rw [hclosed']
  85  ring
  86
  87/-- The earlier closed-scale model packages into the later
  88`RealizedHierarchy` interface, with the two critical fields now proved
  89rather than assumed. -/
  90noncomputable def toRealizedHierarchy
  91    (F : ClosedObservableFramework) (H : RealizedClosedScaleModel F) :
  92    RealizedHierarchy F where
  93  baseState := H.baseState
  94  levels_eq := by
  95    intro k
  96    rfl
  97  levels_pos := by
  98    intro k
  99    exact F.r_pos _
 100  growth := by
 101    rw [realized_closed_scale_ratio_step F H 0]
 102    exact H.growth
 103  ratio_self_similar := ratio_self_similar_of_realized_closed_scale F H
 104  additive_posting := by
 105    simpa using additive_posting_of_realized_closed_scale F H
 106
 107end HierarchyRealizationFromScale
 108end Foundation
 109end IndisputableMonolith
 110