`RecognitionEvent`

definition

show as: view math explainer →

module: IndisputableMonolith.Information.InformationIsLedger
domain: Information
line: 46 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Information.InformationIsLedger on GitHub at line 46.

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

  43
  44/-- A recognition event: a positive ratio x in the ledger.
  45    Each physical fact is encoded as such a ratio. -/
  46structure RecognitionEvent where
  47  /-- The recognition ratio x > 0. -/
  48  ratio : ℝ
  49  /-- Positivity is required for J-cost to be well-defined. -/
  50  ratio_pos : ratio > 0
  51
  52/-- The information cost of a recognition event = J(x). -/
  53noncomputable def infoCost (e : RecognitionEvent) : ℝ := Jcost e.ratio
  54
  55/-- **THEOREM IC-001.1**: Every recognition event has non-negative information cost.
  56    J(x) ≥ 0 for all x > 0. This follows from AM-GM: (x + 1/x)/2 ≥ 1. -/
  57theorem info_cost_nonneg (e : RecognitionEvent) : infoCost e ≥ 0 :=
  58  Jcost_nonneg e.ratio_pos
  59
  60/-- **THEOREM IC-001.2**: Information cost is zero iff the ratio is 1.
  61    J(x) = 0 ↔ x = 1 — the unique balanced/zero-defect state. -/
  62theorem info_cost_zero_iff_unit (e : RecognitionEvent) :
  63    infoCost e = 0 ↔ e.ratio = 1 := by
  64  unfold infoCost
  65  constructor
  66  · intro h
  67    rw [Jcost_eq_sq e.ratio_pos.ne'] at h
  68    have hden_pos : 0 < 2 * e.ratio := by linarith [e.ratio_pos]
  69    have hden_ne : (2 * e.ratio) ≠ 0 := ne_of_gt hden_pos
  70    have hsq : (e.ratio - 1) ^ 2 = 0 := by
  71      rwa [div_eq_zero_iff, or_iff_left hden_ne] at h
  72    nlinarith [sq_nonneg (e.ratio - 1)]
  73  · intro h; rw [h]; exact Jcost_unit0
  74
  75/-- **THEOREM IC-001.3**: Any ratio x ≠ 1 carries strictly positive information cost.
  76    J(x) > 0 for all x > 0, x ≠ 1. -/

papers checked against this theorem

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