A.6.7:4.6 Examples

Example 1 — compare two offers and retain the nondominated set. The question is whether either offer can be discarded without accepting a worse cost or quality. This is a stipulated mathematical use; the following specifications and applications are case facts, not empirical measurements or dated Work claims.

Selected contracts and specifications. The baseline OfferChoiceB1 selects Dcmp = A.19.CPM §4.1 and Dsel = A.19.SelectorMechanism §4.1, including their operation-local declarations, application/binding predicates, identity and extent rules, in the same publication edition as this case. These references mean that edition’s content, not a later revision. Resolve another publication’s references again before reuse. Their effective scheme is the CHR reference scheme declared there.

The case’s independently stipulated specification editions are:

These definitions are the cited case specifications, outside the suite description. OfferBasis@1 gives position cost the price Characteristic and EUR ratio scale, and position quality the declared defect-free proportion Characteristic and a dimensionless ratio scale. The already admitted measure profiles are A=(10 EUR, 0.8), B=(12 EUR, 0.9). Both use these positions, with complete exact stipulated values.

Filled suite description. OfferChoiceSuiteDescription has mech_suite_id = OfferChoiceSuite, membership {Dcmp, Dsel}, required spec references {OfferCN@1, OfferCG@1}, and required policy/comparator references {OfferSelection@1, OfferPareto@1}. Its shared obligations are tri-state eligibility with unknown never passing, explicit numeric admissibility, set-valued comparison/selection without hidden scalarization or totalization, and gate-decision separation. The one protocol contains four required steps:

The protocol invariant requires both members to use the same admitted profiles, scope, slices, scheme, plane and evaluation point, and Select to consume the actual returned Compare binding. The audit obligation is to recover those effective arguments, eligibility judgments and output bindings, including token provenance. There is no public naming, semantic/kind/plane correspondence, flow crossing, gate, implementation export or planned-launch claim in this use, so it requires none of their conditional anchors. The description supplies no operation law or runtime output of its own.

Application and result. Outside the description, stipulate one completed application of each of the four selected operations, in the listed order. Each takes up the following arguments and ends at its own return; those four invocation episodes are distinct from the evaluation point they share. OfferScope@1 delimits the comparison and selection of A and B for this offer question; {OfferSlice@1} is its selected A.2.6 context-slice set. Both members bind that scope and set, the CHR reference scheme, the concept reference plane, and evaluation point 2030-01-01T00:00Z in UTC. No additional CharacteristicSpacePredicate or MinimalEvidence override is used. Normalization has no dependency because OfferCN@1 compares the original matched scales.

The comparator guard uses A as LeftProfileSlot and B as RightProfileSlot, with OfferCN@1, OfferCG@1 and OfferPareto@1, and returns pass: both profiles are complete, admitted and scale-compatible. Application c1 then returns ComparisonResultSlot = {A ∥ B}. Its returned binding, not an equal saved token, supplies the selection basis.

The selector guard binds CandidateSetSlot={A,B}, comparisonBasis={c1}, requiredComparisons={(A,B,OfferPareto@1)}, tokenProvenance={A ∥ B ↦ c1’s returned binding}, and ComparisonResultSlot={A ∥ B}. CriteriaSlot contains the single clause “retain all nondominated candidates”; selectorPolicy is OfferSelection@1; TaskSignatureSlot is absent because no default is obtained from it. CN, CG and the common use arguments are those above. Coverage is complete and the guard returns pass. Select consumes that exact eligibility result and returns SelectionSlot = {A,B}. Incomparability is retained; neither offer is silently chosen as the winner.

Changed condition and stop. If B’s quality is unknown, OfferCG@1’s evidence condition fails: CompareEligibility returns abstain, no Compare result is fabricated, and the selector has no complete comparison basis. Its guard returns abstain, with no Select application or selected-set result. Changing only the selected comparator declaration to an unresolved edition also stops at protocol resolution before calculation. A suite-shaped record cannot cure either missing basis.

The description answers which contracts can be jointly used and under what conditions. The four stipulated applications answer what happened in this case. A gate decision, dated Work account or published result would need its own independently established basis.

Declaration-change case. The CHR normalize stage resolves to apply in a selected UNM declaration edition. Let D1 admit pass and policy-supported degrade, as A.19.UNM §4.1 does. Suppose a separately proposed D2 changes the operation guard to pass only. For the same input whose eligibility is degrade, D1 permits the qualified output and D2 does not. Merely pinning both sources or writing UNM + normalize cannot decide which contract governs. A step selecting D1 remains on D1; substituting D2 changes the member contract and requires the new guard to pass. These are illustrative edition names, not claims that both editions are published.

Two different realizers of D1 still use one member. UNM and the independently identified UINDM declaration are different members. A differently formatted publication of D1 can preserve the declaration identity. A new declaration about an independently established same family is still a new contract when its content changes; any family-continuity claim remains separate. Thus the protocol can resolve exactly even where family continuity is irrelevant or unresolved.

Example 2 (non-conformant). Misusing a family as a suite:

CHRMechanismFamily : MechFamilyDescription := { UNM, UINDM, USCM, ... }

This is a level error: MechFamilyDescription is reserved for realizations of a single mechanism declaration.

Example 3 (non-conformant). Turning a suite into a hidden gate:

• The suite declares GateDecision values or embeds a DecisionLog.
• The suite defines acceptance thresholds (“pass score ≥ 0.7”) as part of suite obligations.
• The suite embeds Φ/CL tables or invents an additional graph edge kind beyond E.18 U.Transfer.

All violate the separation between mechanism/suite descriptions and gate-level operational control.