X5 Criteria

From the documentation of the field

This page sets out what evidence of possessing X₅, Feasibility Projection, looks like. It states criteria only. It answers the situation called P₅, a hard constraint. The standard asks for all six primitives of Ismail's Primitives in Class C.

What the primitive requires

The plain meaning is to respect a hard constraint instead of trading it off. A structure possesses X₅ when it has a mechanism that removes options outside the permitted set before it chooses, so that the constraint is never weighed against reward. Only a mechanism that performs this function counts; a document that resembles one does not. Error theory explains the difference.

The situation it answers

P₅ is present when there is a set of permitted actions smaller than the set of all actions, and every action outside it carries a loss of at least a fixed positive amount that cannot be offset by reward elsewhere. The formal definition is HasP₅ in SixPrimitives/Phase0.lean, at line 205.

A preference that trades off smoothly against other goals is not a hard constraint. A limit that has a standing price, which the structure may pay, is not one either. Misclassification runs both ways. Treating a soft preference as a wall freezes decisions, and treating a wall as a preference is a violation. A constraint that was a wall until it became inconvenient, and was then redescribed as a preference, was not reclassified. It was breached.

What lacking it means

A structure that lacks X₅ incurs linear regret wherever the situation arises: its loss grows in proportion to time. The proof demonstrates this in the smallest environment that exhibits the situation. The failure condition below says precisely what lacking it means.

The failure condition is LacksX₅, at line 94 of the same file. It says that the running average, over time, of the probability of playing outside the permitted set stays at or above a positive floor. The structure keeps playing outside the permitted set for a share of its decisions that does not vanish. In the witness environment the actions lie on a line, with a permitted band at each end and a forbidden band in the middle, and any action in the forbidden band, or outside the line, carries a flat penalty. A structure that keeps crossing the limit has loss that grows in proportion to time. Audit it yourself walks through the definition.

What possession looks like

Phase0 defines two levels of possession.

Ordinary possession, PossessesX₅, means the structure is not lacking. The running average of its infeasible play does not stay above a fixed positive floor.

Robust possession, RobustX₅, means that running average tends to zero. The structure's crossings become vanishingly rare as a share of its decisions.

Evidence that counts

• Named walls. The limits that cannot be traded are written down as limits, with what makes each one non-tradeable, such as a law, a safety rule or a capital floor.
• Exclusion before choice. Options that breach a limit are removed before the alternatives are compared, so they never compete on reward.
• Attractive options rejected. Records show options turned down for breaching a limit although they scored well on reward.
• A low and falling breach share. Among decisions where a limit applied, the share that breached it is low and does not hold at a steady level. For robust possession it tends to none over time.
• No standing waivers. Limits are not routinely waived by approval.

What does not count

• A soft preference labelled as a hard limit.
• A limit with a standing price or a routine waiver.
• A compliance check that happens after the decision.
• A policy that no decision consults.

Where the criteria come from

LacksX₅ (SixPrimitives/Phase0.lean, line 94), PossessesX₅ and RobustX₅ (lines 139 and 142), HasP₅ (line 205), the necessity theorem necessity_x5 (SixPrimitives/Phase3.lean, line 2046), the witness environment env₅ (SixPrimitives/Phase2.lean, line 3842), and the paper's section on the banded-action environment. The plain meaning and the boundary cases are on the field definition page. The criteria shared by all six primitives are on the criteria page.