Encyclopedia Foundation Foundation Ledger Floor T0 Bridge Ledger Floor T0 Bridge

ARTICLE 3 claims 3 theorems

Foundation Ledger Floor T0 Bridge Ledger Floor T0 Bridge

A ledger that counts every recognition event collapses to a simple on/off switch, and a machine-checked proof shows the switch is not a choice but a forced projection.

Verify this page

The two-state shadow

A ledger, a discrete record of events, can count how many times something happens. The Recognition Science framework starts with such a record: for each kind of distinction, the ledger stores a natural number, the multiplicity of that event. The cost of a ledger is the sum of its entries, each weighted by a positive number. This is the extensive picture, where every single posting matters.

Now imagine collapsing that ledger to a single bit of information: is the ledger empty, or is it not? This two-state shadow, called the floor, answers only yes or no. The framework's library, a machine-checked collection of formal theorems, proves that this collapse is not an arbitrary modeling decision. The theorem ledger_floor_t0_bridge establishes that the map from ledger to floor is a surjective homomorphism: it respects addition (the shadow of a sum is the Boolean OR of the shadows), it is onto (every floor state comes from some ledger), and the floor's cost is exactly the ledger's cost clamped to {0,1}. The floor is a genuine quotient, not a separate object.

The proof also pins down the kernel of this projection. Two ledgers have the same shadow exactly when they agree on having zero cost. The floor's consistency predicate, its notion of being well-formed, is precisely the statement that the underlying ledger is costless. This turns the T0 floor from a chosen Boolean indicator into the forced truncation of the extensive ledger, closing a gap in the framework's earlier development.

What this does not claim is that the ledger itself is observable. The theorem shows the floor is a shadow of the ledger, but it does not say the full multiplicity is accessible. The extensive ledger remains a theoretical object; only its two-state truncation is forced. Nor does the theorem assign any physical meaning to the weights or to the specific kinds of distinctions. Those remain modeling choices, not consequences of the proof.

THEOREM ledger_floor_t0_bridge · ledgerShadow_add · ledgerToFloor_surjective · IndisputableMonolith/Foundation/LedgerFloorT0Bridge.lean
ledger_floor_t0_bridge · IndisputableMonolith/Foundation/LedgerFloorT0Bridge.lean:207 
/-- 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Δ]
ledgerShadow_add · IndisputableMonolith/Foundation/LedgerFloorT0Bridge.lean:116 
/-- The shadow is a homomorphism from ledger addition to Boolean `OR`: posting
recognition in either summand lights the two-state floor. -/
theorem ledgerShadow_add {I : Type v} (Γ Δ : DefectLedger I) :
    ledgerShadow (Γ + Δ) = (ledgerShadow Γ || ledgerShadow Δ) := by
  unfold ledgerShadow
  by_cases hΓ : Γ = 0
  · by_cases hΔ : Δ = 0
    · simp [hΓ, hΔ]
    · simp [hΓ, hΔ]
  · have hsum : Γ + Δ ≠ 0 := fun hc => hΓ (ledger_add_eq_zero_iff.mp hc).1
    simp [hΓ, hsum]
ledgerToFloor_surjective · IndisputableMonolith/Foundation/LedgerFloorT0Bridge.lean:173 
/-- The shadow lift surjects onto the T0 floor: every floor state is the shadow
of some ledger, so the floor is a genuine quotient (shadow) of the ledger. The
single primitive distinction `i₀` witnesses the marked state. -/
theorem ledgerToFloor_surjective {K : Type*} (h : ∃ x y : K, x ≠ y)
    {I : Type v} (i₀ : I) :
    Function.Surjective (ledgerToFloor (I := I) h) := by
  intro q
  by_cases hq : forcedQuotientBoolEquiv h q = false
  · refine ⟨0, ?_⟩
    unfold ledgerToFloor
    rw [ledgerShadow_zero]
    exact (Equiv.symm_apply_eq _).mpr hq.symm
  · have hqt : forcedQuotientBoolEquiv h q = true := by
      cases hb : forcedQuotientBoolEquiv h q
      · exact absurd hb hq
      · rfl
    refine ⟨Finsupp.single i₀ 1, ?_⟩
    unfold ledgerToFloor
    have hne : Finsupp.single i₀ (1 : ℕ) ≠ 0 := by
      rw [Ne, Finsupp.single_eq_zero]; exact one_ne_zero
    rw [ledgerShadow_eq_true_iff.mpr hne]
    exact (Equiv.symm_apply_eq _).mpr hqt.symm
THEOREM ledgerShadow_eq_false_iff · ledgerShadow_eq_true_iff · IndisputableMonolith/Foundation/LedgerFloorT0Bridge.lean
ledgerShadow_eq_false_iff · IndisputableMonolith/Foundation/LedgerFloorT0Bridge.lean:87 
theorem ledgerShadow_eq_false_iff {I : Type v} {Γ : DefectLedger I} :
    ledgerShadow Γ = false ↔ Γ = 0 := by
  unfold ledgerShadow
  by_cases hΓ : Γ = 0 <;> simp [hΓ]
ledgerShadow_eq_true_iff · IndisputableMonolith/Foundation/LedgerFloorT0Bridge.lean:92 
theorem ledgerShadow_eq_true_iff {I : Type v} {Γ : DefectLedger I} :
    ledgerShadow Γ = true ↔ Γ ≠ 0 := by
  unfold ledgerShadow
  by_cases hΓ : Γ = 0 <;> simp [hΓ]
THEOREM LedgerFloorT0Bridge · IndisputableMonolith/Foundation/LedgerFloorT0Bridge.lean
LedgerFloorT0Bridge · IndisputableMonolith/Foundation/LedgerFloorT0Bridge.lean:141 
/-- **The T0 floor is the Boolean truncation of the extensive recognition
ledger.** For any distinction witness `h` and strictly positive per-distinction
weight `w`, the lift `ledgerToFloor h` is a surjective cost-and-join
homomorphism from the extensive ledger onto the distinction-generated T0 floor,
under which the floor cost is the two-state clamp of the extensive ledger cost. -/
structure LedgerFloorT0Bridge {K : Type*} (h : ∃ x y : K, x ≠ y)
    {I : Type v} (w : I → ℝ) : Prop where
  /-- The empty ledger maps to the consistent (empty) floor state. -/
  shadow_emp :
    ledgerToFloor h (0 : DefectLedger I) = (ConfigSpace.emp : ForcedQuotient h)
  /-- Ledger addition projects onto the Boolean `OR` join of the floor. -/
  shadow_join :
    ∀ Γ Δ : DefectLedger I,
      ledgerToFloor h (Γ + Δ) =
        ConfigSpace.join (ledgerToFloor h Γ) (ledgerToFloor h Δ)
  /-- The T0 recognition cost of the shadow is the truncation (clamp to `{0,1}`)
  of the extensive ledger cost. -/
  cost_is_truncated_ledger :
    ∀ Γ : DefectLedger I,
      (forcedQuotientRecognitionCost h).C (ledgerToFloor h Γ) =
        (if ledgerCost w Γ = 0 then (0 : ℝ) else 1)
  /-- The floor's consistency predicate is exactly "the ledger is costless". -/
  consistent_iff_costless :
    ∀ Γ : DefectLedger I,
      ConfigSpace.IsConsistent (ledgerToFloor h Γ) ↔ ledgerCost w Γ = 0
  /-- Two ledgers have the same shadow exactly when they agree on having zero
  extensive cost: the floor's identity is the truncated cost kernel. -/
  kernel_is_cost_kernel :
    ∀ Γ Δ : DefectLedger I,
      ledgerToFloor h Γ = ledgerToFloor h Δ ↔
        (ledgerCost w Γ = 0 ↔ ledgerCost w Δ = 0)

What this page does not claim

The theorem does not claim the extensive ledger itself is observable or directly measurable. It does not assign physical meaning to the weights or to the specific kinds of distinctions. It does not prove that the floor is the only possible truncation of the ledger.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND