Foundation Ledger Floor T0 Bridge Rank1 Cost Is Boolean Truncation

The Boolean shadow

The declaration rank1_cost_is_boolean_truncation is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It concerns the most basic kind of recognition event: a single primitive distinction, one act of noticing that two things differ. The theorem says that the cost of recognizing such a distinction is exactly a Boolean truncation: the cost is either zero or one, with no intermediate values. In plain terms, a single distinction is either recognized or it is not, and the framework's cost function cannot assign it a fractional or graded value.

The theorem is a special case of a broader identification, proved in the same module, between two ways the framework describes the earliest stages of recognition. One description, the ledger (a discrete record of events, here a count of how many times each distinction has been posted), tracks extensive cost: it records natural-number multiplicities, so a distinction can be posted once, twice, or many times. The other description, the T0 floor, is a two-state object that only knows whether a distinction has been posted at all. The theorem proves that on a single primitive distinction, the T0 floor cost is literally the Boolean recognition cost of the truncated natural-number multiplicity. The map from ledger to floor sends any positive count to true and zero to false, and the cost of that shadow is the clamp of the extensive ledger cost to the set {0, 1}.

The theorem is not an isolated fact. It is the rank-one case of a surjective cost-and-join homomorphism, proved in the same module, from the extensive ledger onto the distinction-generated T0 floor. That homomorphism respects the algebraic structure: the empty ledger maps to the consistent empty floor state, and ledger addition projects onto Boolean OR. It is also surjective, so every floor state is the shadow of some ledger, and it identifies the kernel: two ledgers share a shadow exactly when they agree on having zero extensive cost. The bundled certificate packages all of this as a single theorem, closing a gap in the framework's strict T-1-to-T8 audit by turning T0 from a chosen Boolean indicator into the forced two-state truncation of the extensive recognition ledger.

What the theorem does not claim is as important as what it proves. It does not say that a single distinction has a cost of one in any absolute sense; it only says the cost is the Boolean truncation of the ledger multiplicity, which is a structural statement about how the two descriptions relate. It does not extend to multiple distinctions or to weighted costs; the rank-one case is exactly the case of a single primitive distinction with unit weight. And it does not by itself establish the full forcing chain from cost to the golden ratio, the eight-tick cycle, or three spatial dimensions. It is one link in that chain, proved in isolation, and the broader physical claims depend on the rest of the framework's development.

/-- On a single primitive distinction with unit weight, the T0 floor cost is
literally the Boolean recognition cost of the truncated natural-number
multiplicity: `C = boolRecognitionCost ∘ booleanTruncation`. -/
theorem rank1_cost_is_boolean_truncation {K : Type*} (h : ∃ x y : K, x ≠ y)
    {I : Type v} (i₀ : I) (n : ℕ) :
    (forcedQuotientRecognitionCost h).C (ledgerToFloor h (Finsupp.single i₀ n)) =
      TMinus1ToT0.boolRecognitionCost.C (booleanTruncation n) := by
  rw [forcedQuotientRecognitionCost_transport]
  unfold ledgerToFloor
  rw [Equiv.apply_symm_apply, ledgerShadow_single]

/-- On a single primitive distinction with unit weight, the T0 floor cost is
literally the Boolean recognition cost of the truncated natural-number
multiplicity: `C = boolRecognitionCost ∘ booleanTruncation`. -/
theorem rank1_cost_is_boolean_truncation {K : Type*} (h : ∃ x y : K, x ≠ y)
    {I : Type v} (i₀ : I) (n : ℕ) :
    (forcedQuotientRecognitionCost h).C (ledgerToFloor h (Finsupp.single i₀ n)) =
      TMinus1ToT0.boolRecognitionCost.C (booleanTruncation n) := by
  rw [forcedQuotientRecognitionCost_transport]
  unfold ledgerToFloor
  rw [Equiv.apply_symm_apply, ledgerShadow_single]

/-- The Boolean two-state **shadow** of a ledger: `false` on the empty ledger,
`true` as soon as any recognition has been posted. This is the truncation of the
extensive `ℕ`-valued multiplicity to the two-state floor. -/
noncomputable def ledgerShadow {I : Type v} (Γ : DefectLedger I) : Bool :=
  if Γ = 0 then false else true

/-- The Phase-2 identification holds for every distinction witness and every
strictly positive weight. -/
theorem ledger_floor_t0_bridge {K : Type*} (h : ∃ x y : K, x ≠ y)
    {I : Type v} (w : I → ℝ) (hw : ∀ i, 0 < w i) :
    LedgerFloorT0Bridge h w where
  shadow_emp := by
    unfold ledgerToFloor
    rw [ledgerShadow_zero]
    rfl
  shadow_join := by
    intro Γ Δ
    apply (forcedQuotientBoolEquiv h).injective
    rw [forcedQuotientBoolEquiv_join]
    unfold ledgerToFloor
    rw [Equiv.apply_symm_apply, Equiv.apply_symm_apply, Equiv.apply_symm_apply]
    exact ledgerShadow_add Γ Δ
  cost_is_truncated_ledger := by
    intro Γ
    rw [forcedQuotientRecognitionCost_transport]
    unfold ledgerToFloor
    rw [Equiv.apply_symm_apply]
    by_cases hΓ : Γ = 0
    · subst hΓ
      rw [ledgerShadow_zero, ledgerCost_zero]
      simp [TMinus1ToT0.boolRecognitionCost]
    · have hc : ledgerCost w Γ ≠ 0 :=
        fun he => hΓ ((ledgerCost_eq_zero_iff w hw Γ).mp he)
      rw [ledgerShadow_eq_true_iff.mpr hΓ]
      simp [TMinus1ToT0.boolRecognitionCost, hc]
  consistent_iff_costless := by
    intro Γ
    show forcedQuotientBoolEquiv h (ledgerToFloor h Γ) = false ↔ ledgerCost w Γ = 0
    unfold ledgerToFloor
    rw [Equiv.apply_symm_apply, ledgerShadow_eq_false_iff,
      ledgerCost_eq_zero_iff w hw Γ]
  kernel_is_cost_kernel := by
    intro Γ Δ
    have hinj : (ledgerToFloor h Γ = ledgerToFloor h Δ) ↔
        (ledgerShadow Γ = ledgerShadow Δ) := by
      unfold ledgerToFloor
      exact (forcedQuotientBoolEquiv h).symm.injective.eq_iff
    rw [hinj, ledgerCost_eq_zero_iff w hw Γ, ledgerCost_eq_zero_iff w hw Δ]
    by_cases hΓ : Γ = 0 <;> by_cases hΔ : Δ = 0 <;>
      simp [ledgerShadow, hΓ, hΔ]

What this page does not claim

The theorem does not assign an absolute cost of one to a single distinction; it only relates the T0 floor cost to the truncated ledger multiplicity. The theorem does not extend to multiple distinctions or to weighted costs beyond the single primitive distinction with unit weight. The theorem does not by itself establish the golden ratio, the eight-tick cycle, or three spatial dimensions.

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