Holography Landauer Calorimeter Descent Heat Carrier Unique

The unique heat carrier

In the Recognition Science framework, a ledger is a discrete record of events, and a step in that ledger is a transition from one configuration of a cell to another. The framework's library, a machine-checked collection of formal theorems, asks a sharp question: when a step is posted, how much heat does it carry? The declaration heat_carrier_unique answers that the assignment is unique. Any function that satisfies the framework's posting rule, which ties heat to the record of which faces of a cell are closed, must equal the tautological selector tautologicalPostedHeat. The proof is one line: it unfolds the definitions and applies the premise pointwise. This is a theorem, proved in the framework's library, not a conjecture.

The theorem's force is that the heat value is not a free choice. If a step is posted, the heat is whatever the posting rule says it is, and there is no second, different assignment that also obeys the rule. The framework also shows that a truncated version, one that omits a single face channel, fails the rule on a concrete posting step, so the uniqueness is not an artifact of a loose definition. This is a structural result about the ledger, not a statement about laboratory calorimetry.

What the theorem does not claim is just as important. It does not provide an independent, external calorimeter. The heat it pins down is the heat the ledger itself posts, not a measurement from a physical device. The framework's own documentation calls this an honest residual: the aggregation of six face channels is a type-lift of the posting rule, not a new physical input. Identifying the ledger's heat with a real-world measurement remains an open target, not a proved result.

/-- Any inhabitant of the carrier premise is pointwise the tautological
selector. The six-channel construction meets that unique value by the
aggregation theorem above. -/
theorem heat_carrier_unique (q : ℝ) (heat : PhysicalStepHeat)
    (h : HeatIsPostedRecordFlux q heat) :
    heat = tautologicalPostedHeat q := by
  funext c c'
  exact h c c'

theorem five_channel_fails_unit_carrier :
    ¬ HeatIsPostedRecordFlux 1 (fiveChannelHeat 1) := by
  intro h
  have hstep := h cell0 postingStepTarget
  have hne := five_channel_sum_ne_stepHeatCell
  simp only [fiveChannelHeat] at hstep
  exact hne (by exact_mod_cast hstep)

What this page does not claim

The theorem does not claim to construct an independent external calorimeter. The theorem does not claim that the ledger's heat is a measured physical quantity. The theorem does not claim that the identification with a real-world calorimeter is proved.

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