IndisputableMonolith.Foundation.LedgerFieldCone

   1import IndisputableMonolith.Foundation.LedgerField
   2
   3/-!
   4# LedgerFieldCone: hub content-emptiness and the field-level widening cone
   5
   6Two field-level facts that build on `Foundation.LedgerField` (the multi-voxel ledger).
   7
   8## Hub content-emptiness (Cap3 `c3_l03`)
   9
  10The panel's honest restatement of the "time-travel" claim: the hub vantage is
  11ADDRESS-COMPLETE but CONTENT-EMPTY for a single carrier. Addressing is total (every
  12committed index of every voxel is readable), but the value AT the present write-head, the
  13open frontier, is unwritten. `hub_content_empty` proves exactly this: reading a voxel at
  14its own write-head index returns `none`. The hub supplies addressing; a field supplies
  15content. There is no committed value at the frontier to retrieve, so no information is
  16transported from the future.
  17
  18## Field-level widening cone (Cap3 `c3_l04`)
  19
  20`LedgerTime.cone_card_monotone` proves the single-carrier admissible cone never shrinks.
  21`fieldCone_card_monotone` lifts that to the field: summing admissible-continuation counts
  22over a finite voxel set, the field cone count is nondecreasing in horizon. The future cone
  23widens; it never contracts.
  24
  25Status: THEOREM (axiom-clean). MODEL only in the identification of `V`/`E` with physical
  26voxels and recognition entries.
  27-/
  28
  29namespace IndisputableMonolith
  30namespace Foundation
  31namespace LedgerFieldCone
  32
  33open IndisputableMonolith.Foundation.LedgerTime
  34open IndisputableMonolith.Foundation.LedgerField
  35open scoped BigOperators
  36
  37variable {V : Type*} {E : Type*}
  38
  39/-- **Hub content-emptiness.** Reading a voxel at its own present write-head index returns
  40`none`: the frontier is unwritten. The hub is address-complete (every committed index is
  41readable) but content-empty at the present (no committed value to retrieve from the
  42future). -/
  43theorem hub_content_empty (F : LedgerField V E) (v : V) :
  44    (F v)[writeHeadAt F v]? = none := by
  45  unfold writeHeadAt writeHead
  46  exact List.getElem?_eq_none (le_refl _)
  47
  48variable [DecidableEq V]
  49
  50/-- One step of the field-level admissible cone at a fixed voxel set, using a per-voxel
  51successor relation `next`. The cone over the field is the union of the per-voxel cones. -/
  52def fieldConeCard (next : E → Finset E) [DecidableEq E] (S : V → Finset E) (vs : Finset V) : ℕ :=
  53  ∑ v ∈ vs, (S v).card
  54
  55/-- **Field-level widening cone.** The total admissible-continuation count over a finite
  56voxel set is nondecreasing under one cone step at every voxel: the field future cone never
  57shrinks. -/
  58theorem fieldCone_card_monotone (next : E → Finset E) [DecidableEq E]
  59    (S : V → Finset E) (vs : Finset V) :
  60    fieldConeCard next S vs ≤ fieldConeCard next (fun v => coneStep next (S v)) vs := by
  61  unfold fieldConeCard
  62  apply Finset.sum_le_sum
  63  intro v _
  64  exact cone_card_monotone next (S v)
  65
  66/-- **Field time certificate.** The hub is content-empty at the frontier (no future
  67retrieval), and the field future cone is nondecreasing (it widens, never contracts). -/
  68structure FieldTimeCert : Prop where
  69  content_empty : ∀ {V E : Type*} (F : LedgerField V E) (v : V),
  70                    (F v)[writeHeadAt F v]? = none
  71  cone_widens : ∀ {V E : Type*} [DecidableEq V] (next : E → Finset E) [DecidableEq E]
  72                  (S : V → Finset E) (vs : Finset V),
  73                    fieldConeCard next S vs ≤ fieldConeCard next (fun v => coneStep next (S v)) vs
  74
  75theorem fieldTimeCert : FieldTimeCert where
  76  content_empty := fun F v => hub_content_empty F v
  77  cone_widens := by
  78    intro V E _ next _ S vs
  79    exact fieldCone_card_monotone next S vs
  80
  81end LedgerFieldCone
  82end Foundation
  83end IndisputableMonolith
  84