`Configuration`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.InitialCondition
domain: Foundation
line: 40 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.InitialCondition on GitHub at line 40.

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

  37/-! ## Ledger Configuration -/
  38
  39/-- A configuration of N ledger entries, each a positive real ratio. -/
  40structure Configuration (N : ℕ) where
  41  entries : Fin N → ℝ
  42  entries_pos : ∀ i, 0 < entries i
  43
  44/-- Total defect of a configuration: sum of individual J-costs. -/
  45noncomputable def total_defect {N : ℕ} (c : Configuration N) : ℝ :=
  46  ∑ i : Fin N, LawOfExistence.defect (c.entries i)
  47
  48/-- Total defect is non-negative (each term is non-negative). -/
  49theorem total_defect_nonneg {N : ℕ} (c : Configuration N) : 0 ≤ total_defect c := by
  50  apply Finset.sum_nonneg
  51  intro i _
  52  exact LawOfExistence.defect_nonneg (c.entries_pos i)
  53
  54/-- The zero-defect configuration: all entries equal to 1. -/
  55def unity_config (N : ℕ) (_hN : 0 < N) : Configuration N :=
  56  { entries := fun _ => 1
  57    entries_pos := fun _ => by norm_num }
  58
  59/-- The unity configuration has zero total defect. -/
  60theorem unity_defect_zero {N : ℕ} (hN : 0 < N) :
  61    total_defect (unity_config N hN) = 0 := by
  62  unfold total_defect unity_config
  63  simp only [LawOfExistence.defect_at_one]
  64  exact Finset.sum_const_zero
  65
  66/-! ## The Initial Condition is Forced -/
  67
  68/-- **Theorem (F-005 core)**: The unity configuration is the unique
  69    zero-total-defect configuration.
  70    Every entry must be 1 for total defect to vanish. -/

papers checked against this theorem

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