`Config`

definition

show as: view math explainer →

module: IndisputableMonolith.Modal.Possibility
domain: Modal
line: 59 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Modal.Possibility on GitHub at line 59.

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

  56
  57    In the full theory, this would be a LedgerState.
  58    Here we use a simplified representation for modal logic development. -/
  59structure Config where
  60  /-- Configuration value (positive real, generalizes bond multiplier) -/
  61  value : ℝ
  62  /-- Positivity constraint -/
  63  pos : 0 < value
  64  /-- Time coordinate (in ticks) -/
  65  time : ℕ
  66  /-- Boundedness constraint: physical values satisfy |log(value)| ≤ 16.
  67      This covers values from exp(-16) ≈ 1.1×10⁻⁷ to exp(16) ≈ 8.9×10⁶. -/
  68  log_bound : |Real.log value| ≤ 16
  69
  70/-- The set of all well-formed configurations (value > 0) -/
  71def ConfigSpace : Set Config := {c | 0 < c.value}
  72
  73/-- The identity configuration (value = 1, minimal cost) -/
  74def identity_config (t : ℕ) : Config := ⟨1, one_pos, t, by simp [Real.log_one]⟩
  75
  76/-! ## Cost Functions for Modal Logic -/
  77
  78/-- The fundamental cost J(x) = ½(x + 1/x) - 1.
  79
  80    This is the unique cost satisfying d'Alembert + normalization + calibration (T5). -/
  81noncomputable def J (x : ℝ) : ℝ := (1/2) * (x + x⁻¹) - 1
  82
  83/-- J is non-negative for positive arguments. -/
  84lemma J_nonneg {x : ℝ} (hx : 0 < x) : 0 ≤ J x := by
  85  unfold J
  86  have hx_ne : x ≠ 0 := hx.ne'
  87  have h_rewrite : (1:ℝ)/2 * (x + x⁻¹) - 1 = (x - 1)^2 / (2 * x) := by field_simp; ring
  88  rw [h_rewrite]
  89  apply div_nonneg (sq_nonneg _) (by linarith : 0 ≤ 2 * x)

papers checked against this theorem

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