Holography Landauer Calorimeter Forcing Double Posted Heat Face Additive

The face-additive heat decoy

In the Recognition Science framework, a ledger (a discrete record of events) tracks state changes of a system. The declaration doublePostedHeat_face_additive is a formal theorem about a specific candidate for measuring heat in a six-faced cell model. It establishes that a particular heat function, one that posts twice the standard heat value, can be written as a sum of six independent one-bit channel contributions. This property is called face-channel additivity.

The theorem is proved in the framework's machine-checked library of formal theorems. It shows that the doubled heat function satisfies two weak axioms: it is kernel-silent (posting zero heat when the face record is unchanged) and face-additive. However, the same library proves this doubled heat function is not equal to the unit tautological heat posting. This is the key finding: the doubled heat is a decoy that passes the weak axioms but fails to be the unique, forced heat carrier.

The proof works by unfolding definitions. The standard step heat is shown to equal a sum of face atoms, each representing a bit flip on one of six faces. The doubled heat is then just twice this sum, which trivially satisfies additivity. The theorem doublePostedHeat_ne_unit_tautological confirms the decoy is distinct from the unit posting. The library also proves that if you force each channel to post exactly ±q on a flip, the heat is definitionally equal to the tautological posting, which is a form of smuggling, not independent forcing.

What this does not claim: it does not prove that face-additivity alone forces the correct heat function. In fact, the weak axioms admit this scaled decoy. The library explicitly names the missing piece as MissingIndependentCellCalorimeter, a residual type marking an open problem. A stub protocol for logical bit reset is sketched, but no logical discharge is claimed. The result is a precise negative finding: the natural uniqueness attempt fails, and the gap remains open.

theorem doublePostedHeat_face_additive : FaceChannelAdditive doublePostedHeat := by
  refine ⟨fun _ b b' => (2 : ℝ) * (faceAtom b b' : ℝ), ?_, ?_⟩
  · intro i b; cases b <;> simp [faceAtom]
  · intro c c'
    simp only [doublePostedHeat]
    have hsum := stepHeatCell_eq_sum_faceAtom c c'
    have hcast :
        (stepHeatCell c c' : ℝ) =
          ∑ i : Fin 6, (faceAtom (faceBit c i) (faceBit c' i) : ℝ) := by
      rw [hsum, Int.cast_sum]
    rw [hcast, Finset.mul_sum]

theorem doublePostedHeat_ne_unit_tautological :
    ¬ (∀ c c' : CellCfg,
        doublePostedHeat c c' = tautologicalPostedHeat 1 c c') := by
  intro h
  have hstep := h cell0 postingStepTarget
  have hnz : (stepHeatCell cell0 postingStepTarget : ℝ) ≠ 0 := by
    exact_mod_cast postingStepTarget_posts_nonzero
  simp [doublePostedHeat, tautologicalPostedHeat] at hstep
  have h2 : (2 : ℝ) * (stepHeatCell cell0 postingStepTarget : ℝ) =
      (stepHeatCell cell0 postingStepTarget : ℝ) := hstep
  have hmul :
      (2 : ℝ) * (stepHeatCell cell0 postingStepTarget : ℝ) -
        (stepHeatCell cell0 postingStepTarget : ℝ) = 0 := by
    linarith
  have : (stepHeatCell cell0 postingStepTarget : ℝ) = 0 := by
    linarith
  exact hnz this

/-- Weak axioms (kernel silence + face additivity, no unit quantum) do not
force the unit tautological calorimeter. -/
theorem weak_axioms_admit_scaled_decoy :
    KernelSilent doublePostedHeat ∧
      FaceChannelAdditive doublePostedHeat ∧
        ¬ (∀ c c' : CellCfg,
            doublePostedHeat c c' = tautologicalPostedHeat 1 c c') :=
  ⟨doublePostedHeat_kernel_silent, doublePostedHeat_face_additive,
    doublePostedHeat_ne_unit_tautological⟩

/-- Named gap type for an independent cell calorimeter. A discharge would
supply a `PhysicalStepHeat` equal to scaled `stepHeatCell` for a reason that
does not package the six-channel posting rule into the hypothesis list.
Inhabiting this structure does not close the residual. -/
structure MissingIndependentCellCalorimeter where
  named_gap : Unit := ⟨⟩

What this page does not claim

Face-additivity alone forces the correct heat function. The doubled heat function is a valid calorimeter. A logical bit reset protocol has been constructed.

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