Foundation Pair Kernel Posting Boundary Record Free Empty Cut Satisfies Bare Hea

The empty cut's heat

In the Recognition Science framework, a ledger is a discrete record of events, and a recognition is a forced cost of registering one. A cut is a proposed boundary that would separate one part of the record from another. The theorem free_empty_cut_satisfies_bare_heat_not_occurrence concerns the simplest possible cut: one that contains no accounts at all. It proves that the heat associated with moving this empty cut by one step is exactly 1, and that this value equals the boundary flux of any real posting, a single transfer between two distinct accounts.

The proof is a short chain of equalities. The heat of the moving empty cut is shown to equal the posted bit value, which is 1. The boundary flux of any posting, defined as the sum of flows across the boundary of the debit region, is also shown to equal 1 by a separate theorem. The result is that the empty cut and any actual posting are indistinguishable by this scalar heat measurement. A companion theorem then shows that this scalar equality does not identify the underlying poles: two different postings can have the same flux value of 1, so the heat reading alone cannot tell them apart.

The theorem's purpose is to close a specific door in the framework's construction. The framework had proposed a bridge, PostingRecordIsMovingCutRecord, that would identify a posting record with a moving cut record. The theorem postingRecordIsMovingCutRecord_uninhabited_on_bit_carrier proves this bridge is impossible: any cut bit that recovers the posting boundary record must be constant, but the bridge requires a non-constant bit. The empty cut theorem supplies the key step, showing that the recovered bit is forced to the constant value 1. The bridge is therefore left as an open target, not a proved result.

In Recognition Science, this result does not claim that heat is a useless quantity. It claims that on this particular carrier, the bit-level information of a posting cannot be recovered from a moving cut. The framework's library, a machine-checked collection of formal theorems, proves this with no unproved assumptions. The theorem is a precise negative result: it rules out one proposed identification, and it does so by showing that the simplest possible cut already produces the same reading as any real event.

/-- Bare numerical forward join (scalar coincidence). -/
theorem free_empty_cut_satisfies_bare_heat_not_occurrence
    {n : ℕ} (source sink : Fin n) (_h : source ≠ sink) :
    (movingStepHeat emptyCut (extendCut emptyCut 1) : ℝ) =
      postingBoundaryRecord source sink := by
  rw [movingStepHeat_extendCut, postedBitValue_one,
    postingBoundaryRecord_forward source sink _h]
  norm_cast

/-- Scalar-coincidence decoy: equal unit fluxes do not identify poles. -/
theorem scalar_flux_eq_does_not_force_same_poles
    {n : ℕ} (hn : 3 ≤ n) :
    ∃ r₁ r₂ : OrientedPostingBoundaryRecord n,
      r₁.flux = r₂.flux ∧ r₁ ≠ r₂ := by
  have hpos : 0 < n := lt_of_lt_of_le (by decide : (0 : ℕ) < 3) hn
  have h1 : 1 < n := lt_of_lt_of_le (by decide : (1 : ℕ) < 3) hn
  have h2 : 2 < n := lt_of_lt_of_le (by decide : (2 : ℕ) < 3) hn
  let a : Fin n := ⟨0, hpos⟩
  let b : Fin n := ⟨1, h1⟩
  let c : Fin n := ⟨2, h2⟩
  have hab : a ≠ b := by
    intro h; exact (by decide : (0 : ℕ) ≠ 1) (congrArg Fin.val h)
  have hac : a ≠ c := by
    intro h; exact (by decide : (0 : ℕ) ≠ 2) (congrArg Fin.val h)
  refine ⟨⟨a, b, hab⟩, ⟨a, c, hac⟩, ?_, ?_⟩
  · simp [OrientedPostingBoundaryRecord.flux,
      postingBoundaryRecord_forward a b hab,
      postingBoundaryRecord_forward a c hac]
  · intro hEq
    have hsink :=
      (orientedPostingBoundaryRecord_eq_iff_same_poles
        ⟨a, b, hab⟩ ⟨a, c, hac⟩).mp hEq
    exact (by decide : (1 : ℕ) ≠ 2) (congrArg Fin.val hsink.2)

theorem postingRecordIsMovingCutRecord_uninhabited_on_bit_carrier :
    ¬ PostingRecordIsMovingCutRecord := by
  rintro ⟨attach, hrec, hnonconst⟩
  exact hnonconst (recovers_implies_constant attach hrec)

What this page does not claim

The theorem does not claim that heat measurements are useless in general. The theorem does not claim that the moving cut bridge is impossible on all carriers. The theorem does not claim that the empty cut is a real posting.

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/Foundation/PairKernelPostingBoundaryRecord.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: