IndisputableMonolith.Verification.CPT.ForcedFactorization
Ratio-cost scaffold for CPT factorization: a ratio-cost space, canonical cost map, cost image/code, and certificate/rigidity hypothesis packs (plus primitive variants and conversion lemmas). CPT verification authors cite it when stating forced factorization of cost structure. The module is mostly interfaces and packing lemmas over Cost and CPT.Core, not a single closed theorem.
claimA ratio-cost space carries a ratio map and a canonical cost $J$, with cost image and code data. Certificate and rigidity hypothesis packs (and primitive forms) encode the assumptions under which CPT cost structure is forced to factor through the ratio; conversion lemmas relate the primitive packs to the full packs and record that certificates depend on the ratio.
background
CPT verification sits on small reusable interfaces from CPT.Core: decision tags, procedure and resolved-set utilities, class-restricted domination, and lightweight wrappers around CPM A/B/C closure. The Cost import supplies the Recognition cost functional $J$ (the unique symmetric cost fixed by the Recognition Composition Law in the forcing chain).
This module is the ratio-cost scaffold those factorization statements need. It packages a ratio-cost space, the ratio map, a canonical cost, and the derived CostImage / CostCode views so later theorems can talk about factorization without rebuilding the geometry each time.
Hypothesis bundles CertificateHypotheses and RigidityHypotheses (with Primitive* variants) stand for the assumption packs used when proving that cost data factor through the ratio. Conversion lemmas move between primitive and full packs and record the dependence of certificates on the ratio.
proof idea
Definition and interface module, not a single end-to-end proof. It introduces RatioCostSpace, ratio, canonicalCost, CostImage, and CostCode; defines CertificateHypotheses, RigidityHypotheses and their Primitive* counterparts; then supplies packing/conversion lemmas (primitive_to_certificate, primitive_to_rigidity, certificate_depends_on_ratio). Argument structure is: fix the ratio-cost geometry from Cost, state the hypothesis packs needed for CPT factorization, and expose the conversion facts Core and Exports will call.
why it matters in Recognition Science
Feeds the CPT export surface (Verification.CPT.Exports), which re-exports citation-friendly aliases for the CPT layer: WINDOW_* (paper Thm. 4.5 / 6.5, window identifiability) and CPT_PIPELINE_* (paper P→B→A pipeline, §5/§6 composition). Without a shared ratio-cost scaffold, those factorization and pipeline theorems would each rebuild cost geometry and hypothesis packs. In the broader Recognition setting this is verification infrastructure around the unique $J$-cost (T5) rather than a new forcing step; it keeps CPT factorization statements aligned with the cost used elsewhere in the monolith.
scope and limits
- Does not prove a top-level CPT factorization theorem; only scaffolds ratio-cost and hypothesis packs.
- Does not introduce new physics constants or force phi, D=3, or the eight-tick octave.
- Does not replace CPT.Core decision tags, domination, or CPM A/B/C wrappers.
- Does not claim Exports aliases are proved here; those live in the export module.
- Does not discharge open sorry elsewhere; sibling names are interfaces and packing lemmas.
used by (1)
depends on (2)
declarations in this module (19)
-
structure
RatioCostSpace -
def
ratio -
def
canonicalCost -
def
CostImage -
abbrev
CostCode -
structure
CertificateHypotheses -
structure
RigidityHypotheses -
structure
PrimitiveCertificateHypotheses -
structure
PrimitiveRigidityHypotheses -
theorem
primitive_to_certificate -
theorem
primitive_to_rigidity -
theorem
certificate_depends_on_ratio -
theorem
exists_monotone_reparam -
theorem
existsUnique_cost_reparam -
theorem
phi_independent_of_state -
theorem
existsUnique_state_profile -
theorem
forced_factorization -
theorem
forced_factorization_unique -
theorem
forced_factorization_unique_of_primitives