Holography Landauer Calorimeter Descent Step Heat Cell Eq Sum Face Channels

The six-channel sum

In the Recognition Science framework, the ledger (a discrete record of events) tracks how a cell changes from one configuration to another. The framework's library of formal theorems contains a declaration, stepHeatCell_eq_sum_face_channels, which proves a bookkeeping identity: the heat posted to a cell equals the sum of the heats posted to its six faces. This is not an approximation or a modeling choice; it is a theorem, checked by the machine, that follows from the definitions of the cell's flux and its face channels.

The proof works by unpacking definitions. A cell's recorded flux is built from a list of six face bits, each indicating whether a particular face is closed. The theorem shows that summing the heat contributions of these six face channels, each computed by the same one-channel rule, reproduces the cell's total heat exactly. This is the mathematical content: a compositional identity, where the whole is precisely the sum of its parts, with no remainder and no double counting.

In Recognition Science, this result is used to construct a six-channel calorimeter, a device that measures the heat of a cell by adding up the heat of its faces. The proof that this calorimeter satisfies the framework's posting rule, HeatIsPostedRecordFlux, is a direct consequence of the summation theorem. It is a type-lift: the same one-channel rule, applied to each face, lifts to a valid rule for the whole cell. The theorem also shows that any other candidate heat function satisfying the posting rule must equal this sum, pointwise, so the construction is unique.

The declaration does not claim to provide an independent external calorimeter. It is an aggregation rule, a way of combining known face-level bookkeeping into a cell-level statement. It does not introduce new physics, new constants, or new postulates. The framework is explicit that identifying an independent external calorimeter, one not built from the banked posting rule, remains an open problem. The theorem is a piece of internal consistency, not a bridge to experiment.

/-- Channel aggregation: posted cell flux is exactly the sum of the six
Clausius face-channel heats. -/
theorem stepHeatCell_eq_sum_face_channels (c c' : CellCfg) :
    stepHeatCell c c' = sixChannelNativeHeat c c' := by
  unfold sixChannelNativeHeat stepHeatCell recordFlux
  rw [faceRecord_eq_faceBits c, faceRecord_eq_faceBits c', sum_fin6]
  simp [stepHeat, faceBit]
  ring

/-- The six-channel Clausius lift inhabits `HeatIsPostedRecordFlux` via
channel aggregation (not by defining heat as `q * stepHeatCell`). This is a
type-lift of the banked posting rule, not an independent external calorimeter. -/
theorem sixChannelHeat_is_posted_record_flux (q : ℝ) :
    HeatIsPostedRecordFlux q (sixChannelHeat q) := by
  intro c c'
  exact sixChannelHeat_eq_scaled_stepHeatCell q c c'

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

What this page does not claim

The theorem does not provide an independent external calorimeter. The theorem does not introduce new physical constants or postulates. The theorem does not establish that the six faces are physically distinct from the cell.

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: