Pith. sign in
module module moderate

IndisputableMonolith.Verification.CPT.ForcedFactorization

show as:
view Lean formalization →

Scaffold for ratio-cost spaces used in CPT forced-factorization arguments. It packages the ratio map, canonical cost, cost image/code, and the certificate and rigidity hypothesis bundles that factorization proofs consume. Downstream CPT export aliases import this layer so paper-facing theorems can cite a single ratio-cost interface rather than ad-hoc cost constructions.

claimA ratio-cost scaffold: a space of positive ratios $r$, a canonical cost $J$ on those ratios, the image and code of $J$, and hypothesis packs (certificate and rigidity, in both ordinary and primitive form) that state when cost data force a unique factorization compatible with CPT verification.

background

CPT verification sits on the Recognition cost $J$, the unique symmetric cost fixed by the Recognition Composition Law (T5: $J(x)=(x+x^{-1})/2-1$). The Core module supplies decision tags, procedure utilities, class-restricted domination, and thin wrappers around the CPM A/B/C closure theorems. Forced factorization needs a narrower interface: costs evaluated on ratios rather than on absolute scales.

This module introduces that interface. A ratio-cost space carries a ratio map and a canonical cost; CostImage and CostCode record the range and discrete coding of that cost. Certificate and rigidity hypothesis packs (ordinary and primitive) collect the assumptions under which cost data identify a unique factor decomposition. Bridge lemmas relate the primitive packs to the ordinary ones and record that certificates depend only on ratio data.

The setting is verification infrastructure, not a new physical law: it freezes the cost-side language that later CPT pipeline and window-identifiability theorems quote.

proof idea

Definition and interface module, not a single theorem proof. It declares the ratio-cost space and the associated cost image/code, then packages certificate and rigidity assumptions as Prop-valued hypothesis records. Thin conversion lemmas map primitive hypothesis packs to ordinary ones and show certificate data factor through the ratio map. No deep tactic scripts live here; the mathematical work is deferred to consumers that instantiate these packs.

why it matters in Recognition Science

CPT factorization statements need a stable ratio-cost language so uniqueness and rigidity claims do not rebuild $J$ ad hoc. This module is that language. It is imported by the CPT export surface, whose citation-friendly aliases cover the paper window-identifiability family (Thm. 4.5 / 6.5) and the P→B→A pipeline composition (§5 / §6). Without a shared ratio-cost scaffold, those exports would either duplicate cost hypotheses or drift from the Core domination and A/B/C wrappers. The module therefore sits between Cost/Core and the paper-facing CPT theorems, locking the cost side of forced factorization to the T5 $J$-cost and ratio geometry.

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 (19)