Pith. sign in
module module high

IndisputableMonolith.LedgerFloor

show as:
view Lean formalization →

Re-exports the defect ledger and its identification with the T0 Boolean floor. The ledger is the free commutative monoid of finitely supported multiplicities of primitive distinctions, equipped with an extensive additive cost. Anyone citing the T0 floor as a truncation of an extensive recognition cost, or the Phase-2 audit closure that links the two, lands here. The module is a thin public facade over RecognitionLedgerFloor and LedgerFloorT0Bridge.

claimThe defect ledger is the free commutative monoid of finitely supported multiplicity maps on a set $I$ of primitive distinctions, with extensive cost $C$ additive under independent superposition. The T0 Boolean floor is the rank-1 truncation of that cost: the observable floor is positive precisely when the ledger weight is positive, and the Boolean indicator is the truncation of the extensive ledger cost.

background

Recognition Science builds physics from a forcing chain T0–T8. T0 is the minimal two-state (Boolean) recognition floor: a distinction is either present or absent. The Anil critique of the T-1/T0 audit flagged two genuine gaps: the Boolean floor looked chosen rather than derived, and it was not tied to an extensive cost object.

RecognitionLedgerFloor supplies the missing extensive object. The defect ledger is the free commutative monoid on a set $I$ of primitive distinctions: finitely supported multiplicity maps, with ledger cost additive under independent superposition (ledgerCost_add). That cost is the free additive cost floor on those defects.

LedgerFloorT0Bridge then identifies the classical T0 floor with the Boolean truncation of that ledger. Before the bridge, the Boolean indicator and the extensive cost sat side by side with no formal link; the bridge states that the T0 floor is exactly the shadow of the extensive recognition ledger.

proof idea

This is a facade module: it imports RecognitionLedgerFloor and LedgerFloorT0Bridge and surfaces their definitions and theorems (DefectLedger, ledgerCost, boolean_floor_is_truncation, ledger_floor_t0_bridge, rank1_cost_is_boolean_truncation, ledger_t0_identification_certificate, and related lemmas). No independent proof burden lives here. The mathematical work is upstream: construct the free additive ledger cost, prove additivity and the observable-floor characterization, then exhibit the surjective truncation map that realizes T0 as Boolean rank-1 truncation of the ledger.

why it matters in Recognition Science

The root Shape of Logic module imports LedgerFloor so the public T-2–T8 spine can treat T0 as derived rather than postulated. Downstream, IndisputableMonolith exports the core theory of /reality; this module is the ledger-floor entry point in that export.

In the forcing chain, T0 is the first rung. Closing the Phase-2 gap ("turns T0 from a chosen Boolean indicator into the shadow of an extensive cost object") and the dual Anil gaps (free additive cost floor, Boolean truncation) is what lets later steps (J-uniqueness, phi, eight-tick octave, D=3) rest on a cost that is extensive and free rather than an ad hoc bit. Certificates such as ledger_t0_identification_certificate package that identification for audit.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (11)