Holography Owner Indexed Horizon Cut Mem Range Channel Insert Of Ne New

The channel insertion theorem

In the Recognition Science framework, a ledger is a discrete record of events, and a channel is an individual slot within that record where a unit of commitment is posted. The theorem mem_range_channelInsert_of_ne_new concerns what happens when a legal posting adds exactly one new channel to the ledger. It states that every channel in the updated ledger, except the newly added one, is the image of some channel from the old ledger under the insertion map. In plainer terms: the new entry is the only genuinely new thing; everything else was already there, just carried forward.

The statement is proved in the framework's machine-checked library of formal theorems. It is a theorem about the internal structure of the ledger, not about the physical world. The proof relies on the definition of the insertion map and the properties of the ledger state, and it holds for any ledger that satisfies the nonnegativity condition. The theorem does not say anything about what the new channel contains, only that it is distinct from all the carried-forward channels and that every other channel in the updated ledger comes from the old one.

What the theorem does not claim is equally important. It does not say that the new channel is the only channel whose reading is active, nor does it say that the insertion map is surjective onto the entire updated channel set. It also does not claim anything about the physical meaning of the channels, the heat computation, or the boundary profile. Those are separate results in the same file, each with its own scope and conditions. The theorem is a precise, narrow statement about the combinatorics of channel insertion, and it is proved as such.

theorem mem_range_channelInsert_of_ne_new {d : Nat} {L : LedgerState d}
    (hn : NonnegLedger (d := d) L) (k : Fin d) (side : Side)
    (c' : OwnerChannel (post L k side))
    (hne : c' ≠ newChannel hn k side) :
    ∃ c : OwnerChannel L, channelInsert hn k side c = c' := by
  classical
  rcases c' with ⟨p, j⟩
  by_cases hp : p = (k, side)
  · subst hp
    have hcnt : ownerCount (post L k side) k side = ownerCount L k side + 1 := by
      simp [ownerCount_post hn k side k side]
    have hj : j.val < ownerCount L k side + 1 :=
      Nat.lt_of_lt_of_eq j.isLt hcnt
    have hne' : j.val ≠ ownerCount L k side := by
      intro heq
      apply hne
      refine Sigma.ext rfl (heq_of_eq (Fin.ext ?_))
      simpa [newChannel] using heq
    have hlt : j.val < ownerCount L k side :=
      Nat.lt_of_le_of_ne (Nat.lt_succ_iff.mp hj) hne'
    refine ⟨⟨(k, side), ⟨j.val, hlt⟩⟩, ?_⟩
    refine Sigma.ext rfl (heq_of_eq (Fin.ext rfl))
  · have hcnt : ownerCount (post L k side) p.1 p.2 = ownerCount L p.1 p.2 := by
      simp [ownerCount_post hn k side p.1 p.2, hp]
    have hj : j.val < ownerCount L p.1 p.2 :=
      Nat.lt_of_lt_of_eq j.isLt hcnt
    refine ⟨⟨p, ⟨j.val, hj⟩⟩, ?_⟩
    refine Sigma.ext rfl (heq_of_eq (Fin.ext rfl))

What this page does not claim

The theorem does not claim that the insertion map is surjective onto all channels of the updated ledger. The theorem does not claim anything about the readings or values of the carried-forward channels. The theorem does not establish any physical bridge to pair-kernel source normalization.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Holography/OwnerIndexedHorizonCut.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: