# Vector OP4 Finite Supported Resource-Front Theorem V1

Date: 2026-06-09

Status: accepted finite/discrete Vector OP4 resource-front V1 theorem-language note after formal review, local patch, and patch confirmation. This accepted-language status applies only to the V1 scope below.

Accepted V1 route:

```text
accepted_finite_discrete_vector_op4_theorem_language_unblocked_in_v1_scope
```

Claim class: accepted finite/discrete method theorem for resource-front accounting under frozen V1 assumptions. This note does not promote continuous fronts, randomized mixtures, engineering performance, hardware evidence, Tau-X capability, Layer-3 interpretation, or public claim clearance.

Controlling sources:

- `external-reviews/vector-op4-resource-front-pro-theorem-status-synthesis-2026-06-09.md`
- `open-theorem-working-notes/vector-op4-finite-supported-resource-front-separation-note-2026-06-06.md`
- `cct-public-replication/estimators/vector_op4_resource_front.py`
- `cct-public-replication/examples/vector_op4_resource_front_cases.csv`
- `cct-public-replication/examples/vector_op4_resource_front_tau_cases.csv`
- `external-reviews/vector-op4-finite-resource-front-formal-pro-review-2026-06-09.md`
- `external-reviews/vector-op4-finite-resource-front-postreview-patch-confirmation-heavy-review-2026-06-09.md`

## 0. Accepted V1 Statement

For a finite, declared, pure-row, gate-passing Vector OP4 strategy class `S*`, with declared baseline `b in S*`, positive finite task score `q(s)`, positive finite resource costs `z_i(s)`, declared lower-is-better resource axes, frozen support/domain/denominator/amortization/hidden-resource/equality policies, and a uniform admissible weight region `W_delta` with `0 < delta < 1/d`:

1. the finite nondominated resource front `P(S*)` exists;
2. dominated rows cannot be scalarized winners under strictly positive admissible weights;
3. support regions `Supp(s)` are finite linear-feasibility objects;
4. baseline win regions `Win_tau(c,b)` are finite linear-feasibility objects for `tau >= 1`;
5. for `tau > 1`, threshold survival requires nonempty `Supp(c) intersect Win_tau(c,b)`;
6. finite Pareto fronts do not collapse to positive weighted scalarized winners, because unsupported front points can exist.

This is the accepted finite/discrete V1 theorem language. Continuous fronts, randomized mixtures, convexified expected-resource fronts, zero-cost axes, per-axis floor vectors, hardware/engineering performance, Tau-X, Layer-3, and public-claim promotion remain separate objects.

## 1. Objects

Let:

```text
S_declared = finite nonempty declared strategy class
Gate(s) = pass/fail route predicate applied before numeric front interpretation
S* = {s in S_declared : Gate(s) = pass}
b in S* = declared incumbent baseline after gates
A = {1, ..., d} = declared resource-axis set
q(s) > 0 = declared task score, higher is better
z(s) = (z_1(s), ..., z_d(s)) in (0, infinity)^d = declared resource costs, lower is better
tau >= 1 = declared baseline-win threshold
0 < delta < 1/d = declared uniform positive floor for active resource weights
W_delta = {w in R^d : sum_i w_i = 1 and w_i >= delta for every i}
```

The public verifier currently uses the axis set:

```text
energy, latency, memory, calibration, sync_error, instability_risk, alternate_loss
```

This theorem packet uses positive `q(s)`, positive `z_i(s)`, finite nonempty `S*`, and positive admissible weights. Numeric front interpretation is over `S*`, not over raw CSV rows that fail route gates. A more general theorem could allow per-axis floors or zero costs when `w . z(s)` remains positive, but that is outside this V1 object.

Define:

```text
B_w(s) = w . z(s)
Eff_w(s) = q(s) / B_w(s)
```

Define Pareto dominance:

```text
s dominates t
iff q(s) >= q(t), z_i(s) <= z_i(t) for every i,
and at least one inequality is strict.
```

Define the finite resource front over the gate-passing class:

```text
P(S*) = {s in S* : no t in S* dominates s}
```

Define support and baseline-win regions:

```text
Supp(s) = {w in W_delta : Eff_w(s) >= Eff_w(t) for every t in S*}
Win_tau(c,b) = {w in W_delta : Eff_w(c) >= tau Eff_w(b)}
```

## 2. Frozen Assumptions

The V1 theorem object assumes:

- `S_declared` is finite, nonempty, and frozen before scoring.
- `S*` is the finite nonempty gate-passing class used for theorem interpretation.
- The declared baseline `b` lies in `S*`.
- Exactly one baseline is declared by row role or by an explicit override; if explicit CLI baseline is used, any `role=baseline` row must match it.
- Strategy closure is `pure_rows_only`.
- Every resource axis is declared with monotone direction, and lower resource cost is better.
- `q(s)` and every `z_i(s)` are positive and finite.
- `W_delta` is declared before scoring with `0 < delta < 1/d`.
- `tau >= 1`.
- Support/domain, denominator, amortization, hidden-resource, equality/tie, and axis-holdout policies are declared before front interpretation.
- The finite-front score `q(s)` is not the scalarized OP4 envelope variable `I_T(s)`.

The verifier treats support mismatch, non-pure strategy closure, incomplete denominator status, unledgered hidden resources, and claim-relevant zero-weight loopholes as route gates before numeric front interpretation. Rows that fail these gates remain auditable route outcomes, but they are not members of `S*` for the finite-front theorem.

## 3. Lemmas

### Lemma 1: Finite Front Existence And Dominance Closure

For finite nonempty `S*`, `P(S*)` is nonempty. Every dominated strategy in `S*` lies on a finite dominance chain ending at a member of `P(S*)`.

Proof sketch:

Start with any `s in S*`. If `s in P(S*)`, stop. If not, there exists `s_1` in `S*` that dominates `s`. Repeat. Strict dominance improves at least one coordinate in the finite list `(q, -z_1, ..., -z_d)` without worsening any coordinate, so the chain cannot cycle. Finiteness forces termination at a nondominated strategy.

### Lemma 2: Scalarized Winners Are Pareto-Valid

For any `w in W_delta`, every maximizer of `Eff_w` over `S*` is in `P(S*)`.

Proof sketch:

Assume `s` maximizes `Eff_w` over `S*` but is dominated by `t` in `S*`. Then `q(t) >= q(s)` and `z_i(t) <= z_i(s)` for every `i`, with at least one strict inequality. Because all weights are positive and all denominators are positive:

```text
B_w(t) <= B_w(s)
```

and at least one of numerator or denominator is strictly better. Therefore:

```text
Eff_w(t) > Eff_w(s)
```

The inequality is strict because either the numerator is strictly higher or the positive weighted denominator is strictly lower. Therefore a dominated row cannot tie or win as a scalarized maximizer. Ties are possible only among nondominated rows or identical declared performance vectors under the declared equality policy.

### Lemma 3: Support Regions Are Linear-Feasibility Objects

For fixed `s in S*`, `Supp(s)` is the intersection of `W_delta` with finitely many linear halfspaces.

Proof sketch:

Since denominators are positive:

```text
Eff_w(s) >= Eff_w(t)
```

is equivalent to:

```text
q(s) / (w . z(s)) >= q(t) / (w . z(t))
```

and therefore:

```text
sum_i w_i [q(s) z_i(t) - q(t) z_i(s)] >= 0.
```

This is a linear inequality in `w`. Intersecting the finite set of pairwise inequalities with the simplex and weight-floor constraints gives a convex polyhedral feasibility problem.

### Lemma 4: Baseline Win Regions Are Linear-Feasibility Objects

For candidate `c`, baseline `b`, and `tau >= 1`, `Win_tau(c,b)` is the intersection of `W_delta` with one linear halfspace.

Proof sketch:

Using positive denominators:

```text
Eff_w(c) >= tau Eff_w(b)
```

is equivalent to:

```text
sum_i w_i [q(c) z_i(b) - tau q(b) z_i(c)] >= 0.
```

The verifier reports whether this region is empty, partial, or all of `W_delta` by optimizing that linear margin over the declared weight region.

### Lemma 5: Pairwise Dominance Implies All-Positive-Weight Baseline Improvement At `tau = 1`

If candidate `c` dominates baseline `b`, then `Eff_w(c) > Eff_w(b)` for every `w in W_delta` at `tau = 1`, subject to the declared equality policy.

Proof sketch:

Dominance gives `q(c) >= q(b)` and `z_i(c) <= z_i(b)` for all `i`, with at least one strict improvement. Positive weights turn any strict resource improvement into a strict denominator improvement, and a strict numerator improvement is also enough. Hence `Eff_w(c) > Eff_w(b)` under every positive admissible weight vector. For `tau > 1`, dominance alone does not decide threshold survival; the linear `Win_tau` region must be checked.

### Lemma 6: Support And Threshold-Win Intersection Is Required For `tau > 1`

For a supported candidate and `tau > 1`, support and threshold survival require:

```text
Supp(c) intersect Win_tau(c,b) != empty.
```

Proof sketch:

`Supp(c)` records weights under which `c` is a scalarized front winner. `Win_tau(c,b)` records weights under which `c` beats the baseline by the declared threshold. The candidate survives both tests only on the intersection. The V1 verifier routes a supported candidate to `support_win_region_disjoint` when the two regions are separately nonempty but their intersection is empty.

## 4. No-Collapse / Incompleteness Fixtures

Scalarization is a valid projection of a declared resource front, not a full replacement for front mapping.

A canonical unsupported-front example:

```text
q(a) = q(m) = q(c) = 1
z(a) = (1, 5)
z(m) = (4, 4)
z(c) = (5, 1)
```

All three strategies are nondominated. But for any positive two-axis weight vector:

```text
B_w(m) = 4
B_w(a) = w_1 + 5w_2
B_w(c) = 5w_1 + w_2
```

Writing `w = (x, 1 - x)` gives:

```text
B_w(a) = 5 - 4x
B_w(c) = 1 + 4x
B_w(m) = 4
```

Since `B_w(a) + B_w(c) = 6`, at least one endpoint has denominator at most `3`, hence strictly below `4`, for every admissible positive `x`. Thus the middle point is a Pareto-front member but is never supported by positive weighted scalarization. The verifier carries this as `front_member_unsupported`.

A threshold-intersection example is carried in `vector_op4_resource_front_tau_cases.csv`: a candidate can be supported on one weight region and beat the baseline at `tau = 1.2` on a disjoint region. The correct route is `support_win_region_disjoint`.

## 5. Route Mapping

The theorem facts above map into verifier status columns, not into a single overloaded label:

```text
gate_route
front_status
baseline_win_route
support_win_region
route
```

The current V1 route labels include:

```text
baseline_reference
front_member_supported
front_member_unsupported
front_member_weight_sensitive
dominated_not_front
all_weights_baseline_win
some_weights_baseline_win
no_weights_baseline_win
posthoc_only_weight_win
support_win_region_disjoint
support_mismatch_defer
denominator_incomplete_defer
holdout_sensitivity_required
no_go
```

Scalarized predecessor labels remain separate:

```text
candidate_after_declared_pareto_relation
candidate_after_declared_scalarization
resource_shift_requires_scalarization
baseline_first_route
tradeoff_needs_review
```

Route labels such as `support_mismatch_defer`, `denominator_incomplete_defer`, `holdout_sensitivity_required`, and `posthoc_only_weight_win` are audit grammar. The theorem substance is finite-front existence, scalarized soundness, support-region linear feasibility, baseline-win linear feasibility, and scalarization no-collapse.

## 6. Review Questions

Formal review should check:

1. Are the finite-front and dominance-chain statements correct under the declared dominance order?
2. Does positive weighted scalarization imply Pareto-validity under the stated tie/equality policy?
3. Are `Supp(s)` and `Win_tau(c,b)` correctly reduced to linear feasibility?
4. Is the unsupported-front example enough to establish scalarization incompleteness for the finite/discrete V1 object?
5. Does `tau > 1` require support/win intersection as implemented?
6. Are the manifest freeze fields sufficient to prevent post-hoc baseline, axis, denominator, or support-region selection?
7. Are the current verifier fixtures enough for theorem-review handoff, or are more counterexamples required before accepted language?

## 7. Explicit Exclusions

This V1 object leaves the following for later work:

- continuous, asymptotic, or infinite-dimensional fronts;
- randomized mixtures or convexified expected-resource fronts;
- per-axis `delta_i` implementation;
- zero-cost resources;
- exhaustive subset-axis zero-weight sensitivity;
- hardware, bench, or mission performance;
- Tau-X capability;
- Layer-3 or observer-conditioned physics interpretation.
