pith. machine review for the scientific record. sign in
theorem

hierarchy_emergence_forces_phi

proved
show as:
view math explainer →
module
IndisputableMonolith.Foundation.HierarchyEmergence
domain
Foundation
line
95 · github
papers citing
66 papers (below)

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.HierarchyEmergence on GitHub at line 95.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  92
  93/-- **Bridge B1 (unconditional)**: from a zero-parameter scale ladder
  94with additive composition, the scale ratio is forced to `φ`. -/
  95theorem hierarchy_emergence_forces_phi
  96    (L : UniformScaleLadder)
  97    (additive_closure : L.levels 2 = L.levels 1 + L.levels 0) :
  98    L.ratio = φ := by
  99  let S : GeometricScaleSequence :=
 100    { ratio := L.ratio
 101      ratio_pos := lt_trans (by norm_num) L.ratio_gt_one
 102      ratio_ne_one := by linarith [L.ratio_gt_one] }
 103  have h_closed : S.isClosed := by
 104    unfold GeometricScaleSequence.isClosed
 105    unfold ledgerCompose
 106    unfold GeometricScaleSequence.scale
 107    have hrec := locality_forces_additive_composition L additive_closure
 108    nlinarith [hrec]
 109  exact closed_ratio_is_phi S h_closed
 110
 111/-- Combined emergence theorem: from ledger primitives (uniform scale
 112ladder + additive composition), derive the `MinimalHierarchy` package
 113and conclude `φ`. -/
 114theorem ledger_forces_phi
 115    (L : UniformScaleLadder)
 116    (additive_closure : L.levels 2 = L.levels 1 + L.levels 0) :
 117    ∃ H : MinimalHierarchy, H.scales.ratio = φ := by
 118  let S : GeometricScaleSequence :=
 119    { ratio := L.ratio
 120      ratio_pos := lt_trans (by norm_num) L.ratio_gt_one
 121      ratio_ne_one := by linarith [L.ratio_gt_one] }
 122  have h_closed : S.isClosed := by
 123    unfold GeometricScaleSequence.isClosed
 124    unfold ledgerCompose
 125    unfold GeometricScaleSequence.scale