Pith. sign in
module module high

IndisputableMonolith.Foundation.RecognitionLedgerFloor

show as:
view Lean formalization →

Defines the free additive recognition ledger: finitely supported multiplicity maps from a type of primitive distinctions to natural numbers, together with the extensive recognition cost obtained by summing those multiplicities. Supplies the monoid laws, nonnegativity, and the Boolean observable floor (positive weight versus zero). Downstream T0-bridge and factorization modules import this as the extensive cost object whose two-state shadow is the T0 indicator.

claimA defect ledger on a type $I$ of primitive distinctions is a finitely supported map $\ell : I \to_0 \mathbb{N}$. Its recognition cost is $\mathrm{cost}(\ell) = \sum_{i \in I} \ell(i)$. Two ledgers are observably the same when they have the same support of positive weight. The cost vanishes if and only if the ledger is identically zero; cost is additive under pointwise sum of ledgers.

background

Recognition Science treats distinction as the operational primitive. The upstream Cost-from-Distinction module formalises the T-1 to T0 bridge paper: recognition work is the unit cost of performing a single distinction, and that primitive is claimed to force the cost framework.

This module packages the free commutative monoid on a type $I$ of primitive distinctions. A defect ledger is a finitely supported multiplicity map $I \to_0 \mathbb{N}$. The ledger cost is the sum of those multiplicities (extensive recognition work). The Boolean observable floor collapses each ledger to whether its total weight is positive, recovering the two-state T0 indicator as a truncation rather than an independent postulate.

Sibling material includes additivity and nonnegativity of cost, constancy of cost on observable equivalence classes, and the characterisation that cost is zero exactly on the zero ledger.

proof idea

Definition-and-lemma module, not a single theorem. DefectLedger is the Mathlib finsupp type $I \to_0 \mathbb{N}$. ledgerCost is the sum of the multiplicity function. Zero, additivity, single-generator, and nonnegativity lemmas are routine finsupp arithmetic. ObservablySame and the induced setoid identify ledgers with the same positive-weight support; cost is constant on classes. The zero-cost characterisation and the two-independent-same-defects lemma close the elementary algebra needed by the T0 bridge.

why it matters in Recognition Science

Closes the Phase-2 gap flagged in the strict T-1-to-T8 audit: T0 must be the Boolean shadow of an extensive cost object, not a chosen indicator. LedgerFloorT0Bridge imports this module to identify the T0 floor with the truncation of the free ledger. LedgerToFactorization uses unconditional ledger additivity as the algebraic input for the T4-to-T5 bridge condition. The public LedgerFloor aggregator re-exports the same layer for the core-theory PDF. Holography.RecognitionMultiplicity encodes selector data as a T-1 ledger against this floor (conditionally, per the adversarial retag). In the forcing chain this sits at the T-1/T0 interface before J-uniqueness (T5) and the phi fixed point (T6).

scope and limits

used by (4)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (21)