Encyclopedia Holography Holography Record Cost Asymmetry Microstate Cost Nonzero On Constant

ARTICLE 5 claims 5 theorems

Holography Record Cost Asymmetry Microstate Cost Nonzero On Constant

A boundary that distinguishes nothing holds zero records, even though merging its states cost plenty: the theorem that separates memory from erasure.

Verify this page

The two costs of a constant map

In information theory, a constant map sends every input to the same output. Think of a boundary that registers every incoming configuration as the same single state: it performs no distinctions. The Recognition Science framework's ledger, a discrete record of performed distinctions, charges nothing for such a map. Its theorem recordCost proves that any map whose image has at most one element has zero record cost, a boundary that distinguishes nothing holds no records.

The same constant map, however, carries a different price tag. The framework's microstateCost, the log of the number of input states merged into one output, is nonzero for any constant map with at least two inputs. The theorem microstate_cost_nonzero_on_constant states this precisely: if a function is constant and its domain has at least two elements, then its microstate cost is not zero. This is the cost of erasure, the thermodynamic price paid to reset many states to one.

The two numbers answer different questions. Record cost asks what a memory holds; microstate cost asks what was merged to create it. A boundary that distinguishes nothing holds zero entropy, even though resetting it cost the eraser plenty. This distinction, formalized in the framework's library of machine-checked theorems, separates the Bennett memory bookkeeping from the Landauer erasure accounting, two equally standard pieces of the same ledger.

In Recognition Science, this asymmetry selects which cost function governs horizon entropy. The framework's library proves that if horizon entropy equals record cost, the Bekenstein-Hawking coefficient is 1/4; if it equals microstate cost, the coefficient is 3/4. The theorem record_zero_separates_readings shows the two readings diverge exactly on constant maps. The choice is not a matter of taste: the record-cost reading satisfies the record-zero principle, the microstate reading does not.

The theorem does not claim that the microstate reading is thermodynamically incoherent. It is a coherent Boltzmann alternative, one that charges bulk degeneracy to the boundary. The framework's claim is narrower: given that ledger cost counts performed distinctions, the record-cost reading is the one that follows. The microstate reading remains a coherent counterfactual, excluded by the premise, not by thermodynamics.

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 microstate_cost_nonzero_on_constant · IndisputableMonolith/Holography/RecordCostAsymmetry.lean
microstate_cost_nonzero_on_constant · IndisputableMonolith/Holography/RecordCostAsymmetry.lean:237 
/-- **The separation fact.** On a constant map over a domain of size `n ≥ 2`, every
configuration lands in the single fiber, so `microstateCost = log₂ n ≥ 1 ≠ 0` — while
`recordCost = 0` (`record_zero_of_constant`). So the two functionals provably disagree
exactly where a boundary distinguishes nothing, and the record-zero demand ("a boundary
that distinguishes nothing holds zero entropy") selects the record reading uniquely within
this dichotomy.

Honest scope (formerly overclaimed as `microstate_cost_violates_landauer_zero`): this does
NOT show the microstate reading violates Landauer — orthodox Landauer erasure charges the
kernel side, which is exactly what `microstateCost` counts, and a constant map is where
erasure cost peaks. What it shows is that the microstate reading assigns positive *boundary*
entropy to a boundary holding no records, i.e. it books the merged bulk degeneracy on the
boundary. That is a coherent Boltzmann alternative; it is excluded here by the record-cost
premise (Bennett memory bookkeeping), and it yields `κ = 4/3` — the falsifier. -/
theorem microstate_cost_nonzero_on_constant
    {α β : Type*} [Fintype α] [DecidableEq α] [DecidableEq β]
    (f : α → β) (hconst : ∀ x y, f x = f y) (a₀ : α)
    (hcard : 2 ≤ (Finset.univ : Finset α).card) :
    microstateCost f (f a₀) ≠ 0 := by
  have hfiber : (Finset.univ.filter (fun c => f c = f a₀)) = Finset.univ := by
    apply Finset.filter_true_of_mem
    intro x _
    exact hconst x a₀
  unfold microstateCost
  rw [hfiber]
  have : 1 ≤ Nat.log2 (Finset.univ : Finset α).card := one_le_log2_of_two_le hcard
  omega
THEOREM bekenstein_coefficient_of_record_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
THEOREM kappa_four_thirds_of_microstate_cost · IndisputableMonolith/Holography/RecordCostAsymmetry.lean
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 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)

What this page does not claim

The microstate reading is thermodynamically incoherent; it is a coherent alternative excluded by the record-cost premise. The theorem proves which cost function governs real horizons; that requires the additional identification that horizon entropy equals record cost. The theorem applies to continuous or infinite systems; it is stated for finite maps.

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