`derivation_chain_consistent`

proved

show as: view math explainer →

module: IndisputableMonolith.RRF.Foundation.MetaPrinciple
domain: RRF
line: 184 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RRF.Foundation.MetaPrinciple on GitHub at line 184.

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

formal source

 181  forces_phi : True
 182
 183/-- The derivation chain is consistent. -/
 184theorem derivation_chain_consistent : Nonempty DerivationChain := by
 185  constructor
 186  exact {
 187    has_recognition := ⟨Unit, ⟨fun _ _ => True, (), trivial⟩⟩,
 188    forces_ledger := trivial,
 189    forces_phi := trivial
 190  }
 191
 192/-- φ is the unique positive solution to x² = x + 1. -/
 193theorem phi_unique : ∀ x : ℝ, 0 < x → x ^ 2 = x + 1 → x = phi :=
 194  self_similarity_forces_phi
 195
 196end RRF.Foundation
 197end IndisputableMonolith

papers checked against this theorem

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