Holography Record Cost Asymmetry Kappa Four Thirds Of Microstate Cost

The 4/3 coefficient

The Bekenstein-Hawking entropy of a black hole horizon is usually written as one quarter of its area in Planck units. The Recognition Science framework's machine-checked library of formal theorems contains a result that explains what that 1/4 depends on. The theorem kappa_four_thirds_of_microstate_cost proves that if you instead count the number of microscopic configurations that collapse to the same record, you get a coefficient of 3/4, not 1/4. The number 4/3 is the inverse of that coefficient.

The distinction is between two ways to count. The framework models a boundary as a map from configurations to records. The record cost is the logarithm of the number of distinct records the map actually produces: it counts distinctions that are performed. The microstate cost is the logarithm of the number of configurations that map to a single record: it counts the bulk degeneracy that is collapsed. The theorem kappa_four_thirds_of_microstate_cost proves that if horizon entropy is identified with the microstate cost, the coefficient is 3/4. The companion theorem proves that if it is identified with the record cost, the coefficient is 1/4.

The two readings are separated by a concrete property. A map that sends every configuration to the same record has record cost zero: it distinguishes nothing, so it holds no records. The same map has nonzero microstate cost: merging many states into one is exactly what an eraser pays for. The theorem record_zero_separates_readings proves both facts at once. The record-cost reading satisfies the record-zero principle; the microstate reading does not.

In Recognition Science, the theorem is a selection result: given that ledger cost counts performed distinctions, the floor multiplicity tracks the record branch and provably differs from the microstate branch. The rank-versus-nullity freedom inside the floor is gone. The remaining physical input is the single identification that horizon thermodynamic entropy equals the record cost of the boundary closure map. That premise is stated as a named definition, HorizonEntropyIsRecordCost. Given it, 1/4 is a theorem; under the counterfactual microstate reading, the same machinery yields 3/4, so the premise is visibly the fork. A horizon whose area tracked unposted bulk degeneracy would falsify it.

What the theorem does not claim is just as important. It does not prove that the microstate reading is thermodynamically incoherent. The framework's own documentation retracts an earlier claim that the microstate reading violates Landauer's principle. Orthodox Landauer erasure accounting charges the eraser for merging states, so a constant map is exactly where it charges the most. The microstate reading is a coherent Boltzmann alternative that the record-cost premise excludes, not a thermodynamic impossibility. The theorem also does not remove the need for the physical identification; it sharpens it. The 4/3 result is a theorem modulo that one sharp identification, not a free-standing derivation of the Bekenstein-Hawking coefficient.

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

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

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

/-- **The one sharp identification, as an explicit named premise.** Horizon thermodynamic
entropy is measured by the *record* (image-side) cost of the boundary closure map — the count
of *performed* distinctions (the Bennett memory-reset reading) — so the plaquette
multiplicity that enters the pixel/sector ratio is `recordCost closed` (`= 1`). This is the
SOLE remaining physical input of the Bekenstein-Hawking `1/4`; everything below it is a
theorem. -/
def HorizonEntropyIsRecordCost (plaquetteMultiplicity : ℕ) : Prop :=
  plaquetteMultiplicity = recordCost (fun c : FaceCfg => PixelLocal.closed c)

/-- **Tag (b) certificate (`#print axioms`-gated).** The Bekenstein-Hawking `1/4` is a
THEOREM modulo exactly one explicit premise (`HorizonEntropyIsRecordCost`): (1) that premise
forces `1/4`; (2) the counterfactual kernel premise forces `3/4`, so the premise is the sole
fork; (3) record-zero separates the two readings, so the premise is the minimal
memory-bookkeeping demand within the dichotomy, not a tuned coefficient. -/
theorem bekenstein_tag_b_cert :
    (∀ m : ℕ, HorizonEntropyIsRecordCost m →
        (m : ℚ) / (admissibleSectors.card : ℚ) = 1 / 4)
    ∧ (∀ m : ℕ, HorizonEntropyIsMicrostateCost m →
        (m : ℚ) / (admissibleSectors.card : ℚ) = 3 / 4)
    ∧ (recordCost (fun _ : FaceCfg => (true : Bool)) = 0
        ∧ microstateCost (fun _ : FaceCfg => (true : Bool)) true ≠ 0) :=
  ⟨bekenstein_coefficient_of_record_cost, kappa_four_thirds_of_microstate_cost,
    record_zero_separates_readings⟩

What this page does not claim

The theorem does not prove that the microstate reading is thermodynamically incoherent. The theorem does not derive the Bekenstein-Hawking coefficient from first principles without a physical premise. The theorem does not claim that the 4/3 coefficient is observed in nature.

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: