Encyclopedia Holography Holography Record Cost Asymmetry Record Zero Separates Readings

ARTICLE 4 claims 4 theorems

Holography Record Cost Asymmetry Record Zero Separates Readings

A boundary that distinguishes nothing holds no records: this is the record-zero principle, and it decides between two readings of black hole entropy.

Verify this page

The record-zero principle

The record-zero principle is a piece of memory accounting. In the Recognition Science framework, a ledger is a discrete record of events, and its cost is the number of distinctions it records, measured in bits. The principle states that a map which sends every input to the same output, a constant map, performs no distinctions and therefore holds zero records. The theorem record_zero_separates_readings proves this for a specific finite map, and a companion theorem, record_zero_general, proves it for any finite map.

The principle matters because it settles a fork in how to count the entropy of a black hole horizon. One reading, the record-cost reading, counts the distinctions the boundary map performs, the image of the map. The other, the microstate reading, counts the configurations that collapse to a single output, the kernel of the map. On a constant map, the record-cost reading gives zero, while the microstate reading gives a nonzero value. The theorem shows these two readings genuinely diverge, and the record-zero principle selects the record-cost reading as the one consistent with a boundary that distinguishes nothing.

This selection is not a matter of taste. The framework's library proves that the record-cost reading yields the Bekenstein-Hawking coefficient of 1/4 for horizon entropy, while the microstate reading yields 3/4. The record-zero principle is the symmetry-breaker that forces the choice between them. The remaining physical input is the identification that horizon entropy equals the record cost of the boundary closure map, stated as the premise HorizonEntropyIsRecordCost. Given that premise, the 1/4 coefficient is a theorem; without it, the microstate reading remains a coherent alternative.

In Recognition Science, the theorem upgrades a prior conditional result to a genuine selection at the floor level. The framework models the ledger cost as counting performed distinctions, and this directionality is what breaks the symmetry between image and kernel. The record-zero principle is the concrete expression of that directionality, and it is what allows the framework to derive the 1/4 coefficient rather than assume it.

THEOREM record_zero_separates_readings · IndisputableMonolith/Holography/RecordCostAsymmetry.lean
record_zero_separates_readings · IndisputableMonolith/Holography/RecordCostAsymmetry.lean:366 
/-- **Record-zero separates the readings, so the premise is minimal within the dichotomy.**
On the constant (records-nothing) map, the record cost is `0` (`record_zero_of_constant`)
while the microstate cost is nonzero (`microstate_cost_nonzero_on_constant`). So demanding
only "horizon entropy is the boundary's record content: a boundary that distinguishes
nothing holds zero entropy" already fixes the record reading within the proved dichotomy;
`HorizonEntropyIsRecordCost` adds nothing beyond that memory-bookkeeping demand, and
`HorizonEntropyIsMicrostateCost` is inconsistent with it. (Formerly
`record_is_the_landauer_reading`; the demand is Bennett memory bookkeeping, not orthodox
Landauer erasure, which charges the kernel side — see the module header.) -/
theorem record_zero_separates_readings :
    recordCost (fun _ : FaceCfg => (true : Bool)) = 0
    ∧ microstateCost (fun _ : FaceCfg => (true : Bool)) true ≠ 0 := by
  refine ⟨record_zero_of_constant _ (fun _ _ => rfl), ?_⟩
  exact microstate_cost_nonzero_on_constant (fun _ : FaceCfg => (true : Bool))
    (fun _ _ => rfl) (0 : Fin 16) (by decide)
THEOREM record_zero_general · IndisputableMonolith/Holography/RecordCostAsymmetry.lean
record_zero_general · IndisputableMonolith/Holography/RecordCostAsymmetry.lean:131 
/-- **Record-zero (general).** A finite map whose image is a subsingleton (`|image| ≤ 1`)
performs no distinction and hence holds zero record cost. A boundary that distinguishes
nothing holds no records. Holds for an ARBITRARY finite map, so it is a theorem, not an
axiom. (Formerly `landauer_zero_general`; see the naming correction in the module header —
this is Bennett memory bookkeeping, not Landauer erasure.) -/
theorem record_zero_general {α β : Type*} [Fintype α] [DecidableEq β] (f : α → β)
    (h : (Finset.univ.image f).card ≤ 1) : recordCost f = 0 :=
  log2_eq_zero_of_le_one h
THEOREM bekenstein_coefficient_of_record_cost · kappa_four_thirds_of_microstate_cost · IndisputableMonolith/Holography/RecordCostAsymmetry.lean
bekenstein_coefficient_of_record_cost · IndisputableMonolith/Holography/RecordCostAsymmetry.lean:346 
/-- **Descent (THEOREM, axiom-clean).** GIVEN the single record-cost identification, the
pixel-to-sector ratio is forced to the Bekenstein `1/4`, with no further premise. -/
theorem bekenstein_coefficient_of_record_cost (m : ℕ)
    (h : HorizonEntropyIsRecordCost m) :
    (m : ℚ) / (admissibleSectors.card : ℚ) = 1 / 4 := by
  unfold HorizonEntropyIsRecordCost at h
  rw [h, recordCost_closed, recognition_sector_count]; norm_num
kappa_four_thirds_of_microstate_cost · IndisputableMonolith/Holography/RecordCostAsymmetry.lean:354 
/-- **The premise does real work: the kernel reading forces `3/4` (`κ = 4/3`).** The closed
fiber has `2³ = 8` microstates, so `microstateCost closed true = log₂ 8 = 3`, and the ratio
is `3/4`. This is precisely the branch the record-cost premise excludes; it is exhibited here
so that the single identification is visibly the fork, not a hidden re-labeling of the
answer. -/
theorem kappa_four_thirds_of_microstate_cost (m : ℕ)
    (h : HorizonEntropyIsMicrostateCost m) :
    (m : ℚ) / (admissibleSectors.card : ℚ) = 3 / 4 := by
  unfold HorizonEntropyIsMicrostateCost at h
  have hmc : microstateCost (fun c : FaceCfg => PixelLocal.closed c) true = 3 := by decide
  rw [h, hmc, recognition_sector_count]; norm_num
THEOREM selector_forced · IndisputableMonolith/Holography/RecordCostAsymmetry.lean
selector_forced · IndisputableMonolith/Holography/RecordCostAsymmetry.lean:204 
/-- **The floor selector is forced.** Multiplicity equals the record cost (image / rank) at one
face, and differs from the microstate cost (kernel / nullity) at two faces. Since the record
cost is what the ledger floor charges (performed distinctions) while the microstate count
charges collapsed configurations the map never distinguishes, the floor multiplicity tracks
the rank branch, not the nullity branch. This is
`CoefficientBridge.selector_multiplicity_is_closure_rank` established from the asymmetric
addressing content, not from `cellLedger`'s definitional choice. -/
theorem selector_forced :
    (recordCost (fun c : FaceCfg => PixelLocal.closed c) : ℝ)
        = RecognitionMultiplicity.recognitionMultiplicity 1
    ∧ RecognitionMultiplicity.recognitionMultiplicity 2
        ≠ (microstateCost RecognitionMultiplicity.dominoLocalMap (true, true) : ℝ) := by
  refine ⟨recordCost_eq_multiplicity_one, ?_⟩
  rw [RecognitionMultiplicity.recognitionMultiplicity_eq]
  have hmc : microstateCost RecognitionMultiplicity.dominoLocalMap (true, true) = 4 := by
    decide
  rw [hmc]; norm_num

What this page does not claim

The theorem does not prove that the microstate reading is thermodynamically incoherent; it is a coherent Boltzmann alternative that the record-cost premise excludes. The theorem does not remove the need for the physical identification that horizon entropy equals record cost; it sharpens that premise but does not eliminate it. The theorem does not claim that a boundary that distinguishes nothing costs nothing to reset; it concerns the entropy held by the memory, not the work required to erase it.

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/RecordCostAsymmetry.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