Encyclopedia Holography Holography Owner Indexed Horizon Cut

ARTICLE 4 claims 4 theorems

Holography Owner Indexed Horizon Cut

A ledger that assigns every committed unit to an owner and a side, and what happens when a new posting arrives.

Verify this page

The owner-indexed horizon cut

In Recognition Science, the framework that derives physical structure from a forced accounting of recognition events, a ledger is a discrete record of commitments. The owner-indexed horizon cut is a specific way to organize that record: every committed unit is assigned to an account and to a side, debit or credit. The carrier of this structure, called OwnerChannel, is the set of all such assignments, with a fiber size that counts how many units each account-side pair holds. This is a definitional choice, a model of how the ledger is read, not a derived physical law.

The results establish what happens when a posting occurs. A legal atomic tick, a single indivisible update, adds exactly one new channel whose address is the posting's account and side. The embedding that performs this insertion preserves all old channels, their identity and their readings, and is injective: no two old channels collapse into one. The heat of a legal tick, computed as the change in active bits over owner-addressed channels, is exactly one. The boundary profile, the fiber sizes of the owner structure, separates debit from credit at equal total aperture, and from the two states alone one can recover the posting. These are THEOREM-tier results, machine-checked within the model.

The key equation is the heat of a posting step: ownerStepHeat L (post L k side) = 1. This says that a legal posting changes the count of active owner channels by exactly one. The proof follows from the definition of ownerStepHeat as the difference in active bits, and the result that active bits equal committed units. A legal tick therefore has heat one, agreeing with the corpus's movingStepHeat. The results also show that a zero-heat posting is not legal, and that the boundary profile cannot be a free assignment: it is not the case that every ledger has the same fiber size for every account-side pair.

In Recognition Science, this work is a step toward a holographic principle: the boundary of the ledger, its owner structure, carries enough information to recover the posting. The physical bridge from this owner-indexed carrier to pair-kernel source normalization and RemainingPhysicalEquality remains OPEN. The ownerReading encoding, where every committed unit is an active posted bit, is a MODEL choice, now carried on an owner-structured type rather than a bare aperture. The non-acceptance binds are strict: no sourceScale, hbar, G, or Real.pi appear in the forcing path, and the axioms are limited to propext, Classical.choice, and Quot.sound.

What this establishes in plain language: if you keep a ledger where every unit is owned and sided, then a posting is a single, identifiable addition, and the boundary of the ledger, its owner profile, tells you what the posting was. The framework's library, a machine-checked collection of formal results, proves these properties for this model. The open question is whether this owner-indexed structure connects to the deeper physical equations of the framework.

THEOREM newChannel_owner · newChannel_not_mem_range · IndisputableMonolith/Holography/OwnerIndexedHorizonCut.lean
newChannel_owner · IndisputableMonolith/Holography/OwnerIndexedHorizonCut.lean:207 
theorem newChannel_owner {d : Nat} {L : LedgerState d}
    (hn : NonnegLedger (d := d) L) (k : Fin d) (side : Side) :
    (newChannel hn k side).1 = (k, side) :=
  rfl
newChannel_not_mem_range · IndisputableMonolith/Holography/OwnerIndexedHorizonCut.lean:212 
theorem newChannel_not_mem_range {d : Nat} {L : LedgerState d}
    (hn : NonnegLedger (d := d) L) (k : Fin d) (side : Side)
    (c : OwnerChannel L) :
    channelInsert hn k side c ≠ newChannel hn k side := by
  intro heq
  have ho : c.1 = (k, side) := by
    have := congrArg Sigma.fst heq
    simpa [channelInsert_preserves_owner, newChannel] using this
  have hi : (c.2 : Nat) = ownerCount L k side := by
    have := congrArg (fun x : OwnerChannel (post L k side) => (x.2 : Nat)) heq
    simpa [channelInsert_val, newChannel] using this
  have hlt : (c.2 : Nat) < ownerCount L k side := by
    have := c.2.isLt
    simpa [ho] using this
  omega
THEOREM ownerStepHeat_legalAtomicTick · IndisputableMonolith/Holography/OwnerIndexedHorizonCut.lean
ownerStepHeat_legalAtomicTick · IndisputableMonolith/Holography/OwnerIndexedHorizonCut.lean:125 
theorem ownerStepHeat_legalAtomicTick {d : Nat} {L L' : LedgerState d}
    (hn : NonnegLedger (d := d) L)
    (h : LegalAtomicTick (d := d) L L') :
    ownerStepHeat L L' = 1 := by
  obtain ⟨k, side, rfl⟩ := legalAtomicTick_implies_PostingStep (d := d) h
  exact ownerStepHeat_post hn k side
THEOREM boundaryProfile_separates_debit_credit · postingOfProfiles_of_post · IndisputableMonolith/Holography/OwnerIndexedHorizonCut.lean
boundaryProfile_separates_debit_credit · IndisputableMonolith/Holography/OwnerIndexedHorizonCut.lean:307 
/-- Debit vs credit from the same state yield different boundary profiles
at equal total aperture. -/
theorem boundaryProfile_separates_debit_credit (d : Nat) [NeZero d] :
    let L0 : LedgerState d := { debit := fun _ => 0, credit := fun _ => 0 }
    let k : Fin d := ⟨0, Nat.pos_of_ne_zero (NeZero.ne d)⟩
    let Ld := post L0 k Side.debit
    let Lc := post L0 k Side.credit
    ledgerCommittedUnits Ld = ledgerCommittedUnits Lc ∧
      boundaryProfile Ld ≠ boundaryProfile Lc := by
  intro L0 k Ld Lc
  have hn : NonnegLedger (d := d) L0 := ⟨fun _ => le_rfl, fun _ => le_rfl⟩
  have hz := ownerCount_post_zero (d := d)
  refine ⟨by rw [hz.2.2.1, hz.2.2.2], ?_⟩
  intro heq
  have hD : boundaryProfile Ld (k, Side.debit) = 1 := by
    simpa [boundaryProfile, Ld] using hz.1
  have hC : boundaryProfile Lc (k, Side.debit) = 0 := by
    have hcnt : ownerCount Lc k Side.debit = ownerCount L0 k Side.debit := by
      simp [Lc, ownerCount_post hn k Side.credit k Side.debit]
    change ownerCount Lc k Side.debit = 0
    rw [hcnt]
    change Int.natAbs (L0.debit k) = 0
    simp [L0]
  have : boundaryProfile Ld (k, Side.debit) = boundaryProfile Lc (k, Side.debit) :=
    congrFun heq (k, Side.debit)
  omega
postingOfProfiles_of_post · IndisputableMonolith/Holography/OwnerIndexedHorizonCut.lean:347 
theorem postingOfProfiles_of_post {d : Nat} [NeZero d] {L : LedgerState d}
    (hn : NonnegLedger (d := d) L) (k : Fin d) (side : Side) :
    postingOfProfiles L (post L k side) = (k, side) := by
  classical
  have hprop :
      boundaryProfile (post L k side) (k, side) =
          boundaryProfile L (k, side) + 1 ∧
        (∀ q : Fin d × Side, q ≠ (k, side) →
          boundaryProfile (post L k side) q = boundaryProfile L q) := by
    constructor
    · simp [boundaryProfile, ownerCount_post hn k side k side]
    · intro q hne
      simp [boundaryProfile, ownerCount_post hn k side q.1 q.2, hne]
  have hε :=
    Classical.epsilon_spec
      (p := fun p : Fin d × Side =>
        boundaryProfile (post L k side) p = boundaryProfile L p + 1 ∧
          (∀ q, q ≠ p → boundaryProfile (post L k side) q = boundaryProfile L q))
      ⟨(k, side), hprop⟩
  set p := postingOfProfiles L (post L k side)
  have hform := ownerCount_post hn k side p.1 p.2
  by_cases heq : p = (k, side)
  · exact heq
  · have h1 : boundaryProfile (post L k side) p = boundaryProfile L p := by
      simpa [boundaryProfile, heq] using hform
    have h2 : boundaryProfile (post L k side) p = boundaryProfile L p + 1 := hε.1
    omega
THEOREM channelInsert_injective · channelInsert_preserves_owner · channelInsert_preserves_reading · IndisputableMonolith/Holography/OwnerIndexedHorizonCut.lean
channelInsert_injective · IndisputableMonolith/Holography/OwnerIndexedHorizonCut.lean:181 
theorem channelInsert_injective {d : Nat} {L : LedgerState d}
    (hn : NonnegLedger (d := d) L) (k : Fin d) (side : Side) :
    Function.Injective (channelInsert hn k side) := by
  intro c₁ c₂ heq
  have ho : c₁.1 = c₂.1 := by
    have := congrArg Sigma.fst heq
    simpa [channelInsert_preserves_owner] using this
  have hi : (c₁.2 : Nat) = (c₂.2 : Nat) := by
    have := congrArg (fun c : OwnerChannel (post L k side) => (c.2 : Nat)) heq
    simpa [channelInsert_val] using this
  refine Sigma.ext ho ?_
  cases c₁ with
  | mk p1 i1 =>
    cases c₂ with
    | mk p2 i2 =>
      cases ho
      exact heq_of_eq (Fin.ext hi)
channelInsert_preserves_owner · IndisputableMonolith/Holography/OwnerIndexedHorizonCut.lean:160 
theorem channelInsert_preserves_owner {d : Nat} {L : LedgerState d}
    (hn : NonnegLedger (d := d) L) (k : Fin d) (side : Side)
    (c : OwnerChannel L) :
    (channelInsert hn k side c).1 = c.1 := by
  cases c
  rfl
channelInsert_preserves_reading · IndisputableMonolith/Holography/OwnerIndexedHorizonCut.lean:174 
theorem channelInsert_preserves_reading {d : Nat} {L : LedgerState d}
    (hn : NonnegLedger (d := d) L) (k : Fin d) (side : Side)
    (c : OwnerChannel L) :
    ownerReading (post L k side) (channelInsert hn k side c) =
      ownerReading L c := by
  simp [ownerReading]

What this page does not claim

The physical bridge to pair-kernel source normalization is not established. The ownerReading encoding is a model choice, not a derived physical law. The module does not introduce any new physical constants or axioms beyond the standard three.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND