IndisputableMonolith.Foundation.LedgerField

   1import IndisputableMonolith.Foundation.LedgerTime
   2
   3/-!
   4# LedgerField: the multi-voxel (field-level) append-only ledger
   5
   6`Foundation.LedgerTime` formalizes the append-only structure of recognition time for a
   7SINGLE carrier (one `List E`). Time-addressing at field scale needs the multi-voxel
   8generalization: a recognition FIELD is an assignment of an independent append-only ledger
   9to each voxel of a spatial index `V`. This module builds that type and lifts the
  10single-voxel theorems to it.
  11
  12The type. `LedgerField V E := V → List E`: each voxel `v : V` carries its own committed
  13history. A field commit `commitAt v e` appends `e` to voxel `v` only, leaving every other
  14voxel untouched (locality: a write at one voxel does not edit another).
  15
  16What this proves (the multi-voxel keystone for Cap3).
  17
  18* `commitAt_local` (THEOREM): a commit at voxel `v` does not change any other voxel `w ≠ v`.
  19  Locality / no spooky cross-voxel edits.
  20* `past_immutable_at` (THEOREM): committing at `v` cannot alter the committed past of `v`
  21  (truncating back to the old length returns the old ledger). The field past is immutable.
  22* `writeHeadAt_advances` (THEOREM): the per-voxel write-head advances by exactly one at the
  23  written voxel, per commit.
  24* `writeHeadAt_other` (THEOREM): and is unchanged at every other voxel.
  25* `past_addressable_at` (THEOREM): every committed past index at the written voxel reads the
  26  same value after a new commit (address-stable readout).
  27
  28Status: THEOREM (axiom-clean). MODEL only in identifying `V` with physical voxels and `E`
  29with recognition entries (argued in the companion paper, not here). The hub
  30content-emptiness (`c3_l03`) and the field-level widening cone (`c3_l04`) build on this type.
  31-/
  32
  33namespace IndisputableMonolith
  34namespace Foundation
  35namespace LedgerField
  36
  37open IndisputableMonolith.Foundation.LedgerTime
  38
  39variable {V : Type*} {E : Type*}
  40
  41/-- A recognition field: an independent append-only ledger at each voxel. -/
  42def LedgerField (V E : Type*) : Type _ := V → List E
  43
  44variable [DecidableEq V]
  45
  46/-- Commit entry `e` to voxel `v` of the field, leaving all other voxels untouched. -/
  47def commitAt (F : LedgerField V E) (v : V) (e : E) : LedgerField V E :=
  48  Function.update F v (commit (F v) e)
  49
  50/-- The per-voxel write-head (present index at voxel `v`). -/
  51def writeHeadAt (F : LedgerField V E) (v : V) : ℕ := writeHead (F v)
  52
  53/-- **Locality.** A commit at voxel `v` leaves every other voxel `w ≠ v` exactly as it was. -/
  54theorem commitAt_local (F : LedgerField V E) (v : V) (e : E) (w : V) (hw : w ≠ v) :
  55    commitAt F v e w = F w := by
  56  unfold commitAt
  57  rw [Function.update_of_ne hw]
  58
  59/-- The value of the field at the written voxel after a commit is the single-voxel commit. -/
  60theorem commitAt_self (F : LedgerField V E) (v : V) (e : E) :
  61    commitAt F v e v = commit (F v) e := by
  62  unfold commitAt
  63  rw [Function.update_self]
  64
  65/-- **Field past immutability.** Committing at `v` cannot alter the committed past of `v`. -/
  66theorem past_immutable_at (F : LedgerField V E) (v : V) (e : E) :
  67    (commitAt F v e v).take (F v).length = F v := by
  68  rw [commitAt_self]
  69  exact past_immutable (F v) e
  70
  71/-- **Write-head advance (written voxel).** The present index at `v` moves forward by one. -/
  72theorem writeHeadAt_advances (F : LedgerField V E) (v : V) (e : E) :
  73    writeHeadAt (commitAt F v e) v = writeHeadAt F v + 1 := by
  74  unfold writeHeadAt
  75  rw [commitAt_self]
  76  exact writeHead_advances (F v) e
  77
  78/-- **Write-head unchanged (other voxels).** No other voxel's present index moves. -/
  79theorem writeHeadAt_other (F : LedgerField V E) (v : V) (e : E) (w : V) (hw : w ≠ v) :
  80    writeHeadAt (commitAt F v e) w = writeHeadAt F w := by
  81  unfold writeHeadAt
  82  rw [commitAt_local F v e w hw]
  83
  84/-- **Field past addressability.** Every committed past index at the written voxel reads the
  85same value after a new commit: the field past is read-only and addressable. -/
  86theorem past_addressable_at (F : LedgerField V E) (v : V) (e : E) (i : ℕ)
  87    (hi : i < (F v).length) :
  88    (commitAt F v e v)[i]? = (F v)[i]? := by
  89  rw [commitAt_self]
  90  exact past_addressable (F v) e i hi
  91
  92/-- **Multi-voxel ledger certificate.** The field type is append-only, local (commits do not
  93edit other voxels), with an immutable addressable past and a per-voxel write-head that
  94advances by one at the written voxel and nowhere else. -/
  95structure FieldLedgerCert : Prop where
  96  local_write : ∀ {V E : Type*} [DecidableEq V] (F : LedgerField V E) (v : V) (e : E) (w : V),
  97                  w ≠ v → commitAt F v e w = F w
  98  past_immutable : ∀ {V E : Type*} [DecidableEq V] (F : LedgerField V E) (v : V) (e : E),
  99                     (commitAt F v e v).take (F v).length = F v
 100  head_advances : ∀ {V E : Type*} [DecidableEq V] (F : LedgerField V E) (v : V) (e : E),
 101                    writeHeadAt (commitAt F v e) v = writeHeadAt F v + 1
 102  head_other : ∀ {V E : Type*} [DecidableEq V] (F : LedgerField V E) (v : V) (e : E) (w : V),
 103                 w ≠ v → writeHeadAt (commitAt F v e) w = writeHeadAt F w
 104  addressable : ∀ {V E : Type*} [DecidableEq V] (F : LedgerField V E) (v : V) (e : E) (i : ℕ),
 105                  i < (F v).length → (commitAt F v e v)[i]? = (F v)[i]?
 106
 107theorem fieldLedgerCert : FieldLedgerCert where
 108  local_write := fun F v e w hw => commitAt_local F v e w hw
 109  past_immutable := fun F v e => past_immutable_at F v e
 110  head_advances := fun F v e => writeHeadAt_advances F v e
 111  head_other := fun F v e w hw => writeHeadAt_other F v e w hw
 112  addressable := fun F v e i hi => past_addressable_at F v e i hi
 113
 114end LedgerField
 115end Foundation
 116end IndisputableMonolith
 117