IndisputableMonolith.Foundation.LedgerFloorT0Bridge

   1import Mathlib
   2import IndisputableMonolith.Foundation.RecognitionLedgerFloor
   3import IndisputableMonolith.Foundation.DistinctionToT4
   4import IndisputableMonolith.Foundation.UnifiedForcingChain
   5
   6/-!
   7# The T0 floor IS the Boolean truncation of the extensive recognition ledger
   8
   9This module closes the Phase 2 gap flagged in the strict T-1-to-T8 audit
  10(the colleague checklist: *"turns T0 from a chosen Boolean indicator into the
  11shadow of an extensive cost object"*).
  12
  13Before this module, two worlds sat side by side with no formal connection:
  14
  15* `DistinctionToT4` builds the **T0 floor** as the recognition-work cost on the
  16  observable quotient `ForcedQuotient h` forced by a distinction
  17  `h : ∃ x y : K, x ≠ y`; that quotient is two-state (`≃ Bool`) and its cost is
  18  the Boolean indicator `boolRecognitionCost`;
  19* `RecognitionLedgerFloor` builds the **extensive ledger** `DefectLedger I = I →₀ ℕ`
  20  with additive cost `ledgerCost w`, but it is never identified with the T0
  21  floor; the original `FloorBridgeStrict` fields only proved facts about the
  22  ledger in isolation (a unit-weight multiplicity identity on an unrelated
  23  carrier, an `ℕ → Bool` OR lemma, and a `rfl` cost-kernel).
  24
  25Here we exhibit the explicit **truncation map** that makes the T0 floor the
  26two-state *shadow* of the extensive ledger:
  27
  28```
  29ledgerToFloor h Γ := (forcedQuotientBoolEquiv h).symm (ledgerShadow Γ),
  30ledgerShadow Γ    := if Γ = 0 then false else true.
  31```
  32
  33The bundled theorem `LedgerFloorT0Bridge` proves this map is:
  34
  35* a **monoid homomorphism** onto the T0 join: `ledgerToFloor 0 = emp` and
  36  `ledgerToFloor (Γ + Δ) = join (ledgerToFloor Γ) (ledgerToFloor Δ)` (the
  37  additive ledger projects onto the Boolean OR of the floor);
  38* a **cost truncation**: the T0 recognition cost of the shadow is the clamp of
  39  the extensive ledger cost to `{0,1}` (`cost_is_truncated_ledger`); on a single
  40  primitive distinction this is literally `boolRecognitionCost ∘ booleanTruncation`
  41  of the natural-number multiplicity (`rank1_cost_is_boolean_truncation`);
  42* **surjective**: every floor state is the shadow of some ledger, so the floor
  43  is a genuine quotient (shadow) of the ledger, nothing is unhit
  44  (`ledgerToFloor_surjective`);
  45* a **kernel identification**: two ledgers share a shadow exactly when they
  46  agree on having zero extensive cost (`kernel_is_cost_kernel`), and the floor's
  47  consistency predicate is exactly "the ledger is costless"
  48  (`consistent_iff_costless`).
  49
  50Together these turn T0 from a chosen Boolean indicator into the forced two-state
  51truncation of the extensive recognition ledger.
  52
  53Status: 0 sorry, 0 new axiom.
  54-/
  55
  56namespace IndisputableMonolith
  57namespace Foundation
  58namespace LedgerFloorT0
  59
  60open CostFromDistinction
  61open RecognitionLedgerFloor
  62open DistinctionToT4
  63open UnifiedForcingChain
  64
  65universe u v
  66
  67/-! ## The two-state shadow of a ledger and its lift to the forced quotient -/
  68
  69open Classical in
  70/-- The Boolean two-state **shadow** of a ledger: `false` on the empty ledger,
  71`true` as soon as any recognition has been posted. This is the truncation of the
  72extensive `ℕ`-valued multiplicity to the two-state floor. -/
  73noncomputable def ledgerShadow {I : Type v} (Γ : DefectLedger I) : Bool :=
  74  if Γ = 0 then false else true
  75
  76/-- The lift of the ledger shadow to the T0 floor forced by a distinction. This
  77is the truncation map whose target is the distinction-generated observable
  78quotient, not an unrelated carrier. -/
  79noncomputable def ledgerToFloor {K : Type*} (h : ∃ x y : K, x ≠ y)
  80    {I : Type v} (Γ : DefectLedger I) : ForcedQuotient h :=
  81  (forcedQuotientBoolEquiv h).symm (ledgerShadow Γ)
  82
  83@[simp] theorem ledgerShadow_zero {I : Type v} :
  84    ledgerShadow (0 : DefectLedger I) = false := by
  85  unfold ledgerShadow; exact if_pos rfl
  86
  87theorem ledgerShadow_eq_false_iff {I : Type v} {Γ : DefectLedger I} :
  88    ledgerShadow Γ = false ↔ Γ = 0 := by
  89  unfold ledgerShadow
  90  by_cases hΓ : Γ = 0 <;> simp [hΓ]
  91
  92theorem ledgerShadow_eq_true_iff {I : Type v} {Γ : DefectLedger I} :
  93    ledgerShadow Γ = true ↔ Γ ≠ 0 := by
  94  unfold ledgerShadow
  95  by_cases hΓ : Γ = 0 <;> simp [hΓ]
  96
  97/-- The free ledger is `0` exactly when both summands are `0`: in `I →₀ ℕ` there
  98are no negative entries to cancel a posting. -/
  99theorem ledger_add_eq_zero_iff {I : Type v} {Γ Δ : DefectLedger I} :
 100    Γ + Δ = 0 ↔ Γ = 0 ∧ Δ = 0 := by
 101  constructor
 102  · intro hsum
 103    refine ⟨?_, ?_⟩ <;> ext i
 104    · have hi : Γ i + Δ i = 0 := by
 105        have := congrArg (fun f : DefectLedger I => f i) hsum
 106        simpa [Finsupp.add_apply] using this
 107      have : Γ i = 0 := by omega
 108      simpa using this
 109    · have hi : Γ i + Δ i = 0 := by
 110        have := congrArg (fun f : DefectLedger I => f i) hsum
 111        simpa [Finsupp.add_apply] using this
 112      have : Δ i = 0 := by omega
 113      simpa using this
 114  · rintro ⟨h1, h2⟩; rw [h1, h2, add_zero]
 115
 116/-- The shadow is a homomorphism from ledger addition to Boolean `OR`: posting
 117recognition in either summand lights the two-state floor. -/
 118theorem ledgerShadow_add {I : Type v} (Γ Δ : DefectLedger I) :
 119    ledgerShadow (Γ + Δ) = (ledgerShadow Γ || ledgerShadow Δ) := by
 120  unfold ledgerShadow
 121  by_cases hΓ : Γ = 0
 122  · by_cases hΔ : Δ = 0
 123    · simp [hΓ, hΔ]
 124    · simp [hΓ, hΔ]
 125  · have hsum : Γ + Δ ≠ 0 := fun hc => hΓ (ledger_add_eq_zero_iff.mp hc).1
 126    simp [hΓ, hsum]
 127
 128/-- On a single primitive distinction the shadow is exactly the Boolean
 129truncation of the natural-number multiplicity. -/
 130theorem ledgerShadow_single {I : Type v} (i₀ : I) (n : ℕ) :
 131    ledgerShadow (Finsupp.single i₀ n) = booleanTruncation n := by
 132  by_cases hn : n = 0
 133  · subst hn
 134    rw [Finsupp.single_zero, ledgerShadow_zero, booleanTruncation_zero]
 135  · have hne : Finsupp.single i₀ n ≠ 0 := by
 136      rw [Ne, Finsupp.single_eq_zero]; exact hn
 137    rw [ledgerShadow_eq_true_iff.mpr hne, booleanTruncation_pos hn]
 138
 139/-! ## The identification bundle -/
 140
 141/-- **The T0 floor is the Boolean truncation of the extensive recognition
 142ledger.** For any distinction witness `h` and strictly positive per-distinction
 143weight `w`, the lift `ledgerToFloor h` is a surjective cost-and-join
 144homomorphism from the extensive ledger onto the distinction-generated T0 floor,
 145under which the floor cost is the two-state clamp of the extensive ledger cost. -/
 146structure LedgerFloorT0Bridge {K : Type*} (h : ∃ x y : K, x ≠ y)
 147    {I : Type v} (w : I → ℝ) : Prop where
 148  /-- The empty ledger maps to the consistent (empty) floor state. -/
 149  shadow_emp :
 150    ledgerToFloor h (0 : DefectLedger I) = (ConfigSpace.emp : ForcedQuotient h)
 151  /-- Ledger addition projects onto the Boolean `OR` join of the floor. -/
 152  shadow_join :
 153    ∀ Γ Δ : DefectLedger I,
 154      ledgerToFloor h (Γ + Δ) =
 155        ConfigSpace.join (ledgerToFloor h Γ) (ledgerToFloor h Δ)
 156  /-- The T0 recognition cost of the shadow is the truncation (clamp to `{0,1}`)
 157  of the extensive ledger cost. -/
 158  cost_is_truncated_ledger :
 159    ∀ Γ : DefectLedger I,
 160      (forcedQuotientRecognitionCost h).C (ledgerToFloor h Γ) =
 161        (if ledgerCost w Γ = 0 then (0 : ℝ) else 1)
 162  /-- The floor's consistency predicate is exactly "the ledger is costless". -/
 163  consistent_iff_costless :
 164    ∀ Γ : DefectLedger I,
 165      ConfigSpace.IsConsistent (ledgerToFloor h Γ) ↔ ledgerCost w Γ = 0
 166  /-- Two ledgers have the same shadow exactly when they agree on having zero
 167  extensive cost: the floor's identity is the truncated cost kernel. -/
 168  kernel_is_cost_kernel :
 169    ∀ Γ Δ : DefectLedger I,
 170      ledgerToFloor h Γ = ledgerToFloor h Δ ↔
 171        (ledgerCost w Γ = 0 ↔ ledgerCost w Δ = 0)
 172
 173/-- The shadow lift surjects onto the T0 floor: every floor state is the shadow
 174of some ledger, so the floor is a genuine quotient (shadow) of the ledger. The
 175single primitive distinction `i₀` witnesses the marked state. -/
 176theorem ledgerToFloor_surjective {K : Type*} (h : ∃ x y : K, x ≠ y)
 177    {I : Type v} (i₀ : I) :
 178    Function.Surjective (ledgerToFloor (I := I) h) := by
 179  intro q
 180  by_cases hq : forcedQuotientBoolEquiv h q = false
 181  · refine ⟨0, ?_⟩
 182    unfold ledgerToFloor
 183    rw [ledgerShadow_zero]
 184    exact (Equiv.symm_apply_eq _).mpr hq.symm
 185  · have hqt : forcedQuotientBoolEquiv h q = true := by
 186      cases hb : forcedQuotientBoolEquiv h q
 187      · exact absurd hb hq
 188      · rfl
 189    refine ⟨Finsupp.single i₀ 1, ?_⟩
 190    unfold ledgerToFloor
 191    have hne : Finsupp.single i₀ (1 : ℕ) ≠ 0 := by
 192      rw [Ne, Finsupp.single_eq_zero]; exact one_ne_zero
 193    rw [ledgerShadow_eq_true_iff.mpr hne]
 194    exact (Equiv.symm_apply_eq _).mpr hqt.symm
 195
 196/-- On a single primitive distinction with unit weight, the T0 floor cost is
 197literally the Boolean recognition cost of the truncated natural-number
 198multiplicity: `C = boolRecognitionCost ∘ booleanTruncation`. -/
 199theorem rank1_cost_is_boolean_truncation {K : Type*} (h : ∃ x y : K, x ≠ y)
 200    {I : Type v} (i₀ : I) (n : ℕ) :
 201    (forcedQuotientRecognitionCost h).C (ledgerToFloor h (Finsupp.single i₀ n)) =
 202      TMinus1ToT0.boolRecognitionCost.C (booleanTruncation n) := by
 203  rw [forcedQuotientRecognitionCost_transport]
 204  unfold ledgerToFloor
 205  rw [Equiv.apply_symm_apply, ledgerShadow_single]
 206
 207/-- The Phase-2 identification holds for every distinction witness and every
 208strictly positive weight. -/
 209theorem ledger_floor_t0_bridge {K : Type*} (h : ∃ x y : K, x ≠ y)
 210    {I : Type v} (w : I → ℝ) (hw : ∀ i, 0 < w i) :
 211    LedgerFloorT0Bridge h w where
 212  shadow_emp := by
 213    unfold ledgerToFloor
 214    rw [ledgerShadow_zero]
 215    rfl
 216  shadow_join := by
 217    intro Γ Δ
 218    apply (forcedQuotientBoolEquiv h).injective
 219    rw [forcedQuotientBoolEquiv_join]
 220    unfold ledgerToFloor
 221    rw [Equiv.apply_symm_apply, Equiv.apply_symm_apply, Equiv.apply_symm_apply]
 222    exact ledgerShadow_add Γ Δ
 223  cost_is_truncated_ledger := by
 224    intro Γ
 225    rw [forcedQuotientRecognitionCost_transport]
 226    unfold ledgerToFloor
 227    rw [Equiv.apply_symm_apply]
 228    by_cases hΓ : Γ = 0
 229    · subst hΓ
 230      rw [ledgerShadow_zero, ledgerCost_zero]
 231      simp [TMinus1ToT0.boolRecognitionCost]
 232    · have hc : ledgerCost w Γ ≠ 0 :=
 233        fun he => hΓ ((ledgerCost_eq_zero_iff w hw Γ).mp he)
 234      rw [ledgerShadow_eq_true_iff.mpr hΓ]
 235      simp [TMinus1ToT0.boolRecognitionCost, hc]
 236  consistent_iff_costless := by
 237    intro Γ
 238    show forcedQuotientBoolEquiv h (ledgerToFloor h Γ) = false ↔ ledgerCost w Γ = 0
 239    unfold ledgerToFloor
 240    rw [Equiv.apply_symm_apply, ledgerShadow_eq_false_iff,
 241      ledgerCost_eq_zero_iff w hw Γ]
 242  kernel_is_cost_kernel := by
 243    intro Γ Δ
 244    have hinj : (ledgerToFloor h Γ = ledgerToFloor h Δ) ↔
 245        (ledgerShadow Γ = ledgerShadow Δ) := by
 246      unfold ledgerToFloor
 247      exact (forcedQuotientBoolEquiv h).symm.injective.eq_iff
 248    rw [hinj, ledgerCost_eq_zero_iff w hw Γ, ledgerCost_eq_zero_iff w hw Δ]
 249    by_cases hΓ : Γ = 0 <;> by_cases hΔ : Δ = 0 <;>
 250      simp [ledgerShadow, hΓ, hΔ]
 251
 252/-! ## Citeable certificate -/
 253
 254/-- The full Phase-2 identification, packaged for the strict T-1-to-T8 audit.
 255Specialised to a single primitive distinction (`Unit`) under unit weight, this
 256exhibits the T0 floor as the surjective two-state truncation of the extensive
 257recognition ledger. -/
 258structure LedgerT0IdentificationCertificate : Prop where
 259  /-- The truncation map is a surjective cost-and-join homomorphism from the
 260  extensive ledger onto the distinction-generated T0 floor. -/
 261  bridge :
 262    ∀ {K : Type} (h : ∃ x y : K, x ≠ y),
 263      LedgerFloorT0Bridge h (fun _ : Unit => (1 : ℝ))
 264  /-- On the single primitive distinction the floor cost is the Boolean
 265  recognition cost of the truncated multiplicity. -/
 266  rank1_cost_is_truncation :
 267    ∀ {K : Type} (h : ∃ x y : K, x ≠ y) (n : ℕ),
 268      (forcedQuotientRecognitionCost h).C
 269          (ledgerToFloor h (Finsupp.single (() : Unit) n)) =
 270        TMinus1ToT0.boolRecognitionCost.C (booleanTruncation n)
 271  /-- The T0 floor is a genuine quotient (shadow) of the extensive ledger. -/
 272  floor_is_quotient_of_ledger :
 273    ∀ {K : Type} (h : ∃ x y : K, x ≠ y),
 274      Function.Surjective (ledgerToFloor (I := Unit) h)
 275
 276/-- The Phase-2 ledger-to-T0 identification is a theorem. -/
 277theorem ledger_t0_identification_certificate :
 278    LedgerT0IdentificationCertificate where
 279  bridge := fun h => ledger_floor_t0_bridge h _ (fun _ => one_pos)
 280  rank1_cost_is_truncation := fun h n => rank1_cost_is_boolean_truncation h () n
 281  floor_is_quotient_of_ledger := fun h => ledgerToFloor_surjective h ()
 282
 283end LedgerFloorT0
 284end Foundation
 285end IndisputableMonolith
 286