`LedgerEntry`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.QuantumLedger
domain: Foundation
line: 45 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.QuantumLedger on GitHub at line 45.

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

  42/-! ## Enhanced Ledger Entry -/
  43
  44/-- A ledger entry represents a single recognition event with all RS information. -/
  45structure LedgerEntry where
  46  /-- Unique identifier for the entry -/
  47  id : ℕ
  48  /-- The configuration ratio being recognized -/
  49  ratio : ℝ
  50  /-- Ratio is positive -/
  51  ratio_pos : 0 < ratio
  52  /-- J-cost of this entry (must equal Jcost ratio) -/
  53  cost : ℝ
  54  /-- Phase (0-7) in 8-tick cycle -/
  55  phase : Fin 8
  56  /-- Constraint: cost = Jcost(ratio) -/
  57  cost_eq : cost = Jcost ratio
  58
  59/-- Create a ledger entry from a ratio and phase. -/
  60noncomputable def mkEntry (id : ℕ) (r : ℝ) (hr : 0 < r) (p : Fin 8) : LedgerEntry := {
  61  id := id
  62  ratio := r
  63  ratio_pos := hr
  64  cost := Jcost r
  65  phase := p
  66  cost_eq := rfl
  67}
  68
  69/-- The J-cost of an entry is non-negative. -/
  70theorem entry_cost_nonneg (e : LedgerEntry) : 0 ≤ e.cost := by
  71  rw [e.cost_eq]
  72  exact Jcost_nonneg e.ratio_pos
  73
  74/-- The J-cost is zero iff the ratio is 1. -/
  75theorem entry_cost_zero_iff_unity (e : LedgerEntry) : e.cost = 0 ↔ e.ratio = 1 := by

papers checked against this theorem

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