Holography Record Cost Asymmetry Bekenstein Coefficient Of Record Cost

The coefficient of record cost

The Bekenstein-Hawking entropy formula states that a black hole's entropy is one quarter of its horizon area in Planck units. The factor 1/4 is among the most famous numbers in theoretical physics. In the Recognition Science framework, a machine-checked library of formal theorems contains a declaration named bekenstein_coefficient_of_record_cost that derives this coefficient from a specific counting rule.

The framework models a physical boundary as a ledger, a discrete record of events. The relevant declaration defines a quantity called recordCost: for any finite map, it is the base-2 logarithm of the number of distinct outputs, that is, the number of independent binary distinctions the map actually performs. The theorem then assumes a premise named HorizonEntropyIsRecordCost, which states that the thermodynamic entropy of a horizon equals this record cost of its boundary closure map. Under that assumption, the theorem proves that the entropy per admissible sector equals 1/4.

The proof is concrete. For the specific closure map in question, the theorem recordCost_closed computes the record cost as exactly 1. The number of admissible sectors is 4. The quotient is therefore 1/4. This is not a numerical coincidence: the declaration selector_forced shows that the record cost tracks the rank of the map, not its nullity. The alternative reading, where entropy counts the collapsed microstates behind the boundary, would give a coefficient of 3/4, as shown by kappa_four_thirds_of_microstate_cost.

The declaration does not claim that the premise HorizonEntropyIsRecordCost is itself derived. That premise is a named identification, a physical input that the framework takes as given. The theorem proves a conditional statement: if the horizon entropy is the record cost, then the coefficient is 1/4. It also proves the converse fork: if it were the microstate cost, the coefficient would be 3/4. The framework does not prove which fork nature takes; it sharpens the choice into a single, explicit premise.

What this means for a reader is that the 1/4 coefficient is not a free parameter in the framework. It is forced by a counting rule once the physical identification is made. The framework's contribution is to show that the two competing readings of horizon entropy lead to different coefficients, and that the record-cost reading, which charges zero for a boundary that distinguishes nothing, is the one that yields the standard 1/4. The alternative is not incoherent; it is simply a different, coherent choice that the framework's premise excludes.

/-- **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

/-- The one-face closure map's record cost is `1` — the rank, reusing
`CoefficientBridge.closureRank`. -/
theorem recordCost_closed : recordCost (fun c : FaceCfg => PixelLocal.closed c) = 1 := by
  decide

/-- **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

/-- **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

/-- **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

What this page does not claim

The theorem does not prove that horizon entropy is a record cost; that is an assumed premise. The theorem does not derive the Bekenstein-Hawking formula from first principles without any physical input. The framework does not claim the microstate-cost reading is thermodynamically incoherent, only that it is excluded by the record-cost premise.

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: