`DiscreteLedger`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.PhiForcing
domain: Foundation
line: 193 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.PhiForcing on GitHub at line 193.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 190/-! ## Discrete Ledger with Self-Similarity -/
 191
 192/-- A discrete ledger structure (from LedgerForcing). -/
 193structure DiscreteLedger where
 194  /-- The ledger structure -/
 195  ledger : LedgerForcing.Ledger
 196  /-- A concrete discrete configuration space witnessing finite step structure. -/
 197  discrete_space : DiscretenessForcing.DiscreteConfigSpace
 198
 199/-- Self-similarity property for a discrete ledger. -/
 200def is_self_similar (_L : DiscreteLedger) (r : ℝ) : Prop :=
 201  ∃ S : SelfSimilar, S.ratio = r
 202
 203/-! ## Phi Forcing Theorem -/
 204
 205/-- **PHI FORCING THEOREM**: In a self-similar discrete ledger, the scale ratio is φ.
 206
 207If:
 2081. L is a discrete ledger (from DiscretenessForcing + LedgerForcing)
 2092. L is self-similar with scale ratio r
 2103. r satisfies the compositional constraint r² = r + 1
 211
 212Then: r = φ = (1 + √5)/2 -/
 213theorem phi_forced (L : DiscreteLedger) (r : ℝ) (hr : is_self_similar L r) : r = φ := by
 214  rcases hr with ⟨S, rfl⟩
 215  exact golden_constraint_unique S.ratio_pos (self_similar_forces_golden_constraint S)
 216
 217/-! ## Consequences of φ -/
 218
 219/-- The minimum non-trivial cost: J_bit = ln(φ). -/
 220noncomputable def J_bit : ℝ := Real.log φ
 221
 222/-- J_bit is positive. -/
 223theorem J_bit_pos : 0 < J_bit := Real.log_pos phi_gt_one

papers checked against this theorem

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