Holography Record Monotonicity Record Compatible Iff No Free Record

The no-free-record condition

The declaration recordCompatible_iff_no_free_record is a theorem in the machine-checked library of formal theorems of Recognition Science, a framework in which reality keeps a ledger, a discrete record of events. The theorem concerns a dynamics, a rule for how a physical state changes over time, on a small cell with six faces. It states that a dynamics is record-compatible exactly when it never creates a free record: it never manufactures a boundary distinction between two states whose difference was never posted to the ledger.

In plainer terms, the theorem says that the only way to avoid creating a free record is to respect the ledger's existing distinctions. If two configurations carry the same boundary record, a record-compatible dynamics keeps them carrying the same record. If a dynamics ever splits such a pair, it has created a distinction out of nothing, a free record. The theorem proves these two descriptions are literally the same condition.

The theorem is part of a larger argument in the framework's holography development. It is used to show that, on the forced three-dimensional cell, the bulk physical states embed injectively into the boundary record space (weak complementarity). The no-free-record condition on dynamics replaces a stronger, monolithic premise in the framework's holography manuscript.

The theorem does not claim that no-free-erasure is a physical premise. The framework proves that an erasure, a drop in record weight, is always exported as negative boundary heat, so erasure is never free. The no-free-record condition is the creation half of the ledger discipline, and it remains a physical premise, not a theorem.

/-- A bulk dynamics is **record-compatible** when it never turns an unposted difference
into a posted one: gauge-related inputs go to gauge-related outputs. -/
def RecordCompatible (U : CellCfg → CellCfg) : Prop :=
  ∀ c c', gaugeRel c c' → gaugeRel (U c) (U c')

/-- A dynamics **creates a free record** when some gauge pair (identical posted data,
zero-heat difference channel) is driven to distinct boundary records — a boundary
distinction with no posted source. -/
def CreatesFreeRecord (U : CellCfg → CellCfg) : Prop :=
  ∃ c c', gaugeRel c c' ∧ ¬ gaugeRel (U c) (U c')

/-- A bulk dynamics is **record-compatible** when it never turns an unposted difference
into a posted one: gauge-related inputs go to gauge-related outputs. -/
def RecordCompatible (U : CellCfg → CellCfg) : Prop :=
  ∀ c c', gaugeRel c c' → gaugeRel (U c) (U c')

/-- A dynamics **creates a free record** when some gauge pair (identical posted data,
zero-heat difference channel) is driven to distinct boundary records — a boundary
distinction with no posted source. -/
def CreatesFreeRecord (U : CellCfg → CellCfg) : Prop :=
  ∃ c c', gaugeRel c c' ∧ ¬ gaugeRel (U c) (U c')

/-- **WEAK COMPLEMENTARITY (quotient form, THEOREM).** The boundary record readout is
injective on physical states: distinct physical states of the bulk carry distinct
boundary records. This is the injection `bulk_phys(B) ↪ records(∂B)` the holography
manuscript assumes; here it is a theorem of the gauge quotient. -/
theorem weak_complementarity : Function.Injective physRecord := by
  intro a b
  refine Quotient.inductionOn₂ a b ?_
  intro c c' h
  exact Quotient.sound h

What this page does not claim

The theorem does not claim that no-free-erasure is a physical premise; it is a theorem of the posting rule. The theorem does not claim that the no-free-record condition is derived from first principles; it is an input hypothesis. The theorem does not claim that the injection of bulk states into boundary records is physically operational without the KernelIsGauge hypothesis.

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/RecordMonotonicity.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: