IndisputableMonolith.Foundation.LedgerFloorT0Bridge
Bridges the free additive recognition ledger (finitely supported ℕ-multiplicities) to the T0 Boolean floor by a two-state shadow: false on the empty ledger, true once any recognition is posted. Anyone tracing the absolute floor back to extensive cost, or citing the ledger-floor layer of the core-theory PDF, uses this module. It defines the truncation map, proves additivity and surjectivity facts, and identifies rank-1 cost with Boolean truncation.
claimFor a defect ledger $L:I\to_0\mathbb{N}$, the Boolean shadow is the two-state truncation with $\mathrm{shadow}(\emptyset)=\bot$ and $\mathrm{shadow}(L)=\top$ whenever any multiplicity is positive. The module supplies a surjective bridge from ledgers onto the T0 floor and shows that rank-1 recognition cost is exactly this Boolean truncation of extensive multiplicity.
background
Recognition Science forces the early spine T0–T8 from the cost foundation (Recognition Composition Law). T0 is the absolute two-state floor: empty versus nonempty recognition. The extensive object underneath is the free additive ledger $\mathrm{DefectLedger},I=I\to_0\mathbb{N}$, finitely supported multiplicities with additive recognition cost.
RecognitionLedgerFloor closes the two genuine T-1/T0 audit gaps (the free additive cost floor, not mere minimality slogans). DistinctionToT4 starts the closure path from a supplied distinction witness into that early spine. UnifiedForcingChain then proves T0–T8 as inevitabilities from the cost foundation.
This module sits between those layers: it treats the Boolean floor as the shadow (truncation) of the ℕ-valued ledger rather than as an unrelated primitive.
proof idea
Definition-and-bridge module, not a single deep proof. It introduces ledgerShadow (false only on the empty ledger) and ledgerToFloor, then records elementary facts: shadow of zero, characterizations of false/true, additivity of shadow, behavior on single posts, and the zero-sum criterion for ledger addition.
Surjectivity of ledgerToFloor and the identification rank1_cost_is_boolean_truncation pin the rank-1 cost to the two-state truncation. The capstone ledger_floor_t0_bridge packages the correspondence so the public ledger-floor layer can cite T0 as that shadow. Arguments are direct case analysis on support emptiness and additive structure of finitely supported maps.
why it matters in Recognition Science
Feeds the public aggregator LedgerFloor, which exposes the ledger-floor layer the core-theory PDF cites: free additive ledger, recognition cost, and T0 as the two-state shadow of that extensive ledger.
Without the bridge, T0 in UnifiedForcingChain risks looking like an independent Boolean axiom rather than the truncation of free additive multiplicity closed in RecognitionLedgerFloor. The module therefore tightens the path from distinction witness (DistinctionToT4) through the cost floor into the forcing chain’s absolute floor, keeping the “two-state is minimal” claim tied to an explicit extensive object.
scope and limits
- Does not derive T1–T8 or the full forcing chain; only the T0 Boolean shadow link.
- Does not construct the ledger itself; that lives in RecognitionLedgerFloor.
- Does not address continuous or real-valued costs beyond ℕ-multiplicity truncation.
- Does not supply a distinction witness; DistinctionToT4 owns that path.
- Does not claim the shadow remembers multiplicity counts, only emptiness.
used by (1)
depends on (3)
declarations in this module (14)
-
def
ledgerShadow -
def
ledgerToFloor -
theorem
ledgerShadow_zero -
theorem
ledgerShadow_eq_false_iff -
theorem
ledgerShadow_eq_true_iff -
theorem
ledger_add_eq_zero_iff -
theorem
ledgerShadow_add -
theorem
ledgerShadow_single -
structure
LedgerFloorT0Bridge -
theorem
ledgerToFloor_surjective -
theorem
rank1_cost_is_boolean_truncation -
theorem
ledger_floor_t0_bridge -
structure
LedgerT0IdentificationCertificate -
theorem
ledger_t0_identification_certificate