`rs_ledger_is_unique`

proved

show as: view math explainer →

module: IndisputableMonolith.Meta.LedgerUniqueness
domain: Meta
line: 229 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Meta.LedgerUniqueness on GitHub at line 229.

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

 226    The objection "there could be other discrete ledgers" fails because
 227    each component is uniquely determined by its constraint.
 228-/
 229theorem rs_ledger_is_unique :
 230    ∀ (altPhi : ℝ) (altD : ℕ) (altT : ℕ),
 231      -- If an alternative satisfies the same constraints...
 232      (altPhi > 0 ∧ altPhi^2 = altPhi + 1) →
 233      (altD ≥ 2 ∧ linkingNumber altD ≠ 0) →
 234      (altT = grayCodeCycleLength altD) →
 235      -- ...it must equal the RS values
 236      altPhi = phi ∧ altD = 3 ∧ altT = 8 := by
 237  intro altPhi altD altT ⟨hPhiPos, hPhiEq⟩ ⟨hDPos, hDLink⟩ hT
 238  constructor
 239  · exact phi_unique_fixed_point altPhi hPhiPos hPhiEq
 240  constructor
 241  · exact (Q3_unique_linking_dimension altD hDPos).mp hDLink
 242  · have hD3 : altD = 3 := (Q3_unique_linking_dimension altD hDPos).mp hDLink
 243    rw [hD3] at hT
 244    exact hT
 245
 246end LedgerUniqueness
 247end Meta
 248end IndisputableMonolith

papers checked against this theorem

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