`ledger_forces_phi`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.HierarchyEmergence
domain: Foundation
line: 114 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.HierarchyEmergence on GitHub at line 114.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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
 126    have hrec := locality_forces_additive_composition L additive_closure
 127    nlinarith [hrec]
 128  exact ⟨⟨S, h_closed⟩, hierarchy_forces_phi ⟨S, h_closed⟩⟩
 129
 130end HierarchyEmergence
 131end Foundation
 132end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.