IndisputableMonolith.LedgerFloor

   1import IndisputableMonolith.Foundation.RecognitionLedgerFloor
   2import IndisputableMonolith.Foundation.LedgerFloorT0Bridge
   3
   4/-!
   5# Ledger Floor — the Boolean shadow of the extensive recognition ledger
   6
   7This public aggregator exposes the ledger-floor layer that the core-theory PDF
   8cites: the free additive recognition ledger `DefectLedger I = I →₀ ℕ`, its
   9recognition cost, and the identification of the T0 Boolean floor as the
  10two-state *shadow* (truncation) of that extensive ledger.
  11
  12Every declaration below is proved in Lean with no `sorry` and no project-local
  13axiom. The forced-quotient layer it stands on (`DistinctionToT4`,
  14`TMinus1ForcedFromDistinction`, the `TMinus1ToT0` Boolean recognition cost) is
  15the public core slice of the corresponding `/reality` modules.
  16
  17## Public citation targets
  18
  19* `DefectLedger` — the free commutative monoid `I →₀ ℕ` of primitive
  20  distinctions; the extensive recognition ledger.
  21* `ledgerCost` / `ledgerCost_add` — weighted recognition cost; additivity is
  22  unconditional (no gerrymandered independence relation).
  23* `two_independent_same_defects` — multiplicity is represented: two independent
  24  copies of one defect cost `2 w i`, not `w i`.
  25* `observable_floor_iff_pos_weight` — the observable equivalence is the kernel
  26  of the cost; the floor is non-vacuous iff some distinction has positive weight.
  27* `ledger_floor_t0_bridge` — for any distinction witness and strictly positive
  28  weight, the T0 floor is the surjective cost-and-join shadow of the extensive
  29  ledger.
  30* `ledger_t0_identification_certificate` — the packaged Phase-2 identification:
  31  the T0 floor is a genuine quotient (shadow) of the extensive ledger.
  32-/
  33
  34namespace IndisputableMonolith
  35namespace LedgerFloor
  36
  37open Foundation
  38
  39/-! ## The extensive recognition ledger -/
  40
  41/-- The defect ledger: finitely supported multiplicities of primitive
  42distinctions, the free commutative monoid on `I`. -/
  43abbrev DefectLedger := @Foundation.RecognitionLedgerFloor.DefectLedger
  44
  45/-- Weighted recognition cost of a ledger. -/
  46noncomputable abbrev ledgerCost := @Foundation.RecognitionLedgerFloor.ledgerCost
  47
  48/-- Unconditional additivity of the ledger cost. -/
  49abbrev ledgerCost_add := @Foundation.RecognitionLedgerFloor.ledgerCost_add
  50
  51/-- Multiplicity is represented: two independent copies of one defect cost
  52`2 w i`. -/
  53abbrev two_independent_same_defects :=
  54  @Foundation.RecognitionLedgerFloor.two_independent_same_defects
  55
  56/-- The observable equivalence is the cost kernel; the floor is non-vacuous iff
  57some distinction has positive weight. -/
  58abbrev observable_floor_iff_pos_weight :=
  59  @Foundation.RecognitionLedgerFloor.observable_floor_iff_pos_weight
  60
  61/-- The Boolean T0 floor is the unit-weight truncation of the ledger. -/
  62abbrev boolean_floor_is_truncation :=
  63  @Foundation.RecognitionLedgerFloor.boolean_floor_is_truncation
  64
  65/-! ## The T0 floor is the Boolean shadow of the ledger -/
  66
  67/-- The bundled identification: the truncation map is a surjective cost-and-join
  68homomorphism from the extensive ledger onto the distinction-generated T0 floor. -/
  69abbrev LedgerFloorT0Bridge := @Foundation.LedgerFloorT0.LedgerFloorT0Bridge
  70
  71/-- The Phase-2 identification holds for every distinction witness and every
  72strictly positive weight. -/
  73abbrev ledger_floor_t0_bridge := @Foundation.LedgerFloorT0.ledger_floor_t0_bridge
  74
  75/-- The shadow lift surjects onto the T0 floor: every floor state is the shadow
  76of some ledger. -/
  77abbrev ledgerToFloor_surjective :=
  78  @Foundation.LedgerFloorT0.ledgerToFloor_surjective
  79
  80/-- On a single primitive distinction the floor cost is the Boolean recognition
  81cost of the truncated multiplicity. -/
  82abbrev rank1_cost_is_boolean_truncation :=
  83  @Foundation.LedgerFloorT0.rank1_cost_is_boolean_truncation
  84
  85/-- The packaged Phase-2 certificate: the T0 floor is a genuine quotient
  86(shadow) of the extensive recognition ledger. -/
  87abbrev ledger_t0_identification_certificate :=
  88  Foundation.LedgerFloorT0.ledger_t0_identification_certificate
  89
  90end LedgerFloor
  91end IndisputableMonolith
  92