| CC-MVPK-0 (Lean conditional guard) | A Lean face checks only features it actually carries: the comparison criteria for a bounded source contrast, declared set or order semantics for an actual selection or ordering, relevant pins for numeric or plane-dependent claims, an F.9 Bridge plus bounded-use claim for a semantic crossing, and a selected ReferencePlane plus applicable rule for a plane-dependent value. | No absent selection, ordering, number, semantic crossing, or plane dependency creates a placeholder field or failed check. |
| CC‑MVPK‑2 (Functoriality) | Emit_s(id) is identity; Emit_s(g∘f) = Emit_s(g)∘Emit_s(f). | Compose two cards and diff with the card of the composite. |
| CC-MVPK-3b (Boundary claim-set integrity) | If a published arrow is a boundary, interface, or protocol and an A.6.B claim set exists (L-*, A-*, D-*, and E-*), then normative text on faces is traceable to that claim set (prefer claim-ID citations); faces do not become a second boundary specification. | Lint flags uncited normative clauses; faces reduce to {claim-ID citations + informative commentary}. |
| CC‑MVPK‑4b (Lean evidence-facing lane) | If AssuranceLane-Lite is used, presence bits for current evidence or bridge references suffice; full evidence-carrier lists remain with the exact evidence source. | Presence bits are visible, and no assurance or sufficiency claim is inferred from the lane. |
| CC-MVPK-4c (Input and Output vs publication) | When a morphism face exposes input/output information, it points to the signature-side declarations instead of duplicating them; it carries only source references and pins needed by the face. | The face has no second Input/Output specification and no unused presence-pin dossier. |
| CC-MVPK-4d (Published comparison and ordering) | A source contrast keeps its declared comparison criteria. A published selection or ordering keeps its source-defined set or order semantics and comparator, citing ComparatorSet when that formal family is used. | No hidden scalarization or decision by display order; an ordinary bounded contrast needs no invented ranking or comparator family. |
| CC-MVPK-4e (Signature names the actual object) | Use Signature on a face only for an object that is a signature under its applicable pattern. Use TechName or PlainName for the face’s name. | A cited signature remains identifiable; a face label is not presented as a signature. |
| CC‑MVPK‑4f (Numeric and optional-PC discipline) | Numeric or comparable claims retain the source pins that affect interpretation; when the optional PC profile is selected, its PC and CHR/CG references are explicit. | Cards show the material unit, scale, reference-plane, and edition pins; selected PC fields resolve without making PC classification a prerequisite for an ordinary face. |
| CC‑MVPK‑4g (No axis or dimension) | Faces avoid “axis”, “dimension”, and “plane” metaphors except ReferencePlane; use CHR terms (Characteristic, slot, or CharacteristicSpace). | Lexical check flags none; only ReferencePlane appears. |
| CC‑MVPK‑4h (Edition pins on defs) | Where maps, distances, or spaces are cited, the face pins DescriptorMapRef.edition, DistanceDefRef.edition, and CharacteristicSpaceRef.edition?. | Validation shows edition fields populated. |
| CC‑MVPK‑4i (Crossing references) | A semantic crossing cites its F.9 Bridge and separate bounded-use claim; a plane-dependent value cites its selected ReferencePlane and applicable rule. A B.3 CL/Φ(CL) reference appears only when the current assurance use consumes that integration relation. | F.9 and plane references resolve; any B.3 penalty belongs to the assurance-bearing integration relation, not to the face. |
| CC‑MVPK‑4k (Subset‑of underlier) | For views about epistemes or capabilities, PublicationScope ⊆ ClaimScope or WorkScope; reindexing does not widen it. | Subset witness passes; promotion diff shows no widening. |
| CC‑MVPK‑6 (Γ‑separation) | No cost, time, or data-spend on publication morphisms. | CI shows proof records or witness records; gate validation passes. |
| CC‑MVPK‑7 (Reindexing monotone) | If s ⪯ t, then Emit_s(x) ⪯ Emit_t(x). | TechCard ≤ InteropCard (more structure, same claims). |
CC‑MVPK‑8 (publication-face kind discipline) | Only literal publication-face kind values publication face/form or interop publication form are used; faces are named …View, …Card, or …Lane. | Token scan; no “rendering” or “presentation” as publication-face kind values. |
| CC‑MVPK‑9 (Reindexing naturality) | Conceptual-form coercions PromoteFace[s->t] exist, are total in the selected formal substrate, and commute with composition. | The local witness uses PromoteFace and is not overread as a world-side relation. |
| CC‑MVPK‑10 (Iso‑preservation) | Isomorphisms in U remain isomorphisms under each selected Emit_s. | Cards show mapped inverses or an iso‑witness. |
| CC‑MVPK‑11 (Typing & totality) | Ill-typed composites are rejected at FaceObj_s rather than weakening the selected conceptual-form rules. | Type-check fails early; no best-effort composition claim appears on cards. |
| CC‑MVPK‑12 (Crossing distinctions) | A cross-context semantic face keeps the F.9 Bridge, bounded-use claim, and reliance result distinct; a ReferencePlane-dependent face keeps its characteristic, plane, and transfer or comparison rule distinct. Optional F.9 CL and B.3 integration CL remain in their own uses. | The face exposes only the references consumed by its bounded use and grants no crossing, reliance, or assurance by display. |