Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -7,16 +7,41 @@
- Independent replay: standard-library `Fraction` clean-process checker
- Producer assurance: at most `COMPUTED`

The explicit `combinatorics` bundle includes two generic, bounded operations:
The explicit `combinatorics` bundle includes three generic, bounded operations:

- `combinatorics.recurrence.linear.evaluate`; and
- `combinatorics.recurrence.linear.evaluate`;
- `combinatorics.recurrence.p_recursive.evaluate`; and
- `combinatorics.generating_function.coefficients.compute`.

They complement rather than replace the named Fibonacci, consecutive-Fibonacci,
and Lucas capabilities. `combinatorics.recurrence.linear.verify` and
and Lucas capabilities. `combinatorics.recurrence.linear.verify`,
`combinatorics.recurrence.p_recursive.verify`, and
`combinatorics.generating_function.coefficients.verify` independently replay
the corresponding producer result when bundled checker authorization is
enabled.
the corresponding producer result when bundled checker authorization is enabled.

## Polynomial-coefficient recurrence evaluation

`combinatorics.recurrence.p_recursive.evaluate` accepts canonical ascending
coefficient vectors for polynomials \(p_0(n),\ldots,p_d(n)\) and evaluates

\[
\sum_{j=0}^{d} p_j(n)a_{n-j}=0.
\]

The initial vector is exactly \((a_0,\ldots,a_{d-1})\). Requests select a
prefix or strictly increasing indices, while the result preserves the complete
prefix through the greatest requested index, the recurrence order \(d\), and
every exact recurrence residual at the consecutive indices from \(d\) through
that endpoint. The request is rejected before execution if
the leading polynomial \(p_0(n)\) vanishes at a required recurrence step;
singular relations are not divided by zero or interpreted as conclusions.

`combinatorics.recurrence.p_recursive.verify` independently evaluates the
polynomials and replays the recurrence with standard-library `Fraction`, then
requires every bound residual to be exactly zero. This supports finite exact
evaluation and candidate checking only. It does not prove the recurrence for
all indices or establish that a supplied recurrence follows from an external
generating function or theorem.

## Constant-coefficient recurrence evaluation

Expand Down Expand Up @@ -68,6 +93,8 @@ Version 2 of the combinatorics semantics uses these fail-closed limits:
| Quantity | Limit |
| --- | ---: |
| Linear recurrence order | 16 |
| Polynomial-coefficient recurrence order | 16 |
| Coefficient polynomial degree | 16 |
| Greatest recurrence index | 512 |
| Sparse requested indices | 256 |
| Numerator or denominator degree | 32 |
Expand Down
243 changes: 243 additions & 0 deletions src/jacobian/contracts/combinatorics.py
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@
MAX_LINEAR_RECURRENCE_ORDER = 16
MAX_LINEAR_RECURRENCE_INDEX = 512
MAX_LINEAR_RECURRENCE_REQUESTED_INDICES = 256
MAX_P_RECURSIVE_POLYNOMIAL_DEGREE = 16
MAX_RATIONAL_GENERATING_FUNCTION_DEGREE = 32
MAX_RATIONAL_SERIES_TRUNCATION_ORDER = 512
MAX_COMBINATORICS_INPUT_RATIONAL_DIGITS = 64
Expand Down Expand Up @@ -193,6 +194,116 @@ def _validate_recurrence_result_budget(
)


def _validate_p_recursive_result_budget(
*,
coefficient_polynomials: tuple[tuple[CanonicalRational, ...], ...],
initial_values: tuple[CanonicalRational, ...],
coefficient_convention: str,
polynomial_convention: str,
scope: str,
requested_indices: tuple[int, ...],
) -> None:
polynomials = tuple(
tuple(value.as_fraction() for value in polynomial)
for polynomial in coefficient_polynomials
)
order = len(polynomials) - 1

def polynomial_value(polynomial: tuple[Fraction, ...], index: int) -> Fraction:
return sum(
(
coefficient * index**power
for power, coefficient in enumerate(polynomial)
),
start=Fraction(),
)

end = requested_indices[-1]
replay = [value.as_fraction() for value in initial_values[: end + 1]]
requested_index_set = set(requested_indices)
minimum_size = 1_024 + sum(
_minimum_fraction_wire_bytes(value) * (1 + (index in requested_index_set))
for index, value in enumerate(replay)
)
residuals: list[tuple[int, Fraction]] = []
while len(replay) <= end:
Comment thread
morluto marked this conversation as resolved.
index = len(replay)
coefficients = tuple(
polynomial_value(polynomial, index) for polynomial in polynomials
)
if coefficients[0] == 0:
raise ValueError(
f"leading coefficient polynomial vanishes at index {index}"
)
next_value = (
-sum(
(
coefficients[offset] * replay[index - offset]
for offset in range(1, order + 1)
),
start=Fraction(),
)
/ coefficients[0]
)
if any(
_lower_decimal_digits(component) > MAX_COMBINATORICS_RESULT_RATIONAL_DIGITS
for component in (next_value.numerator, next_value.denominator)
):
raise ValueError(
"polynomial-coefficient recurrence result exceeds the "
f"{MAX_COMBINATORICS_RESULT_RATIONAL_DIGITS}-digit bound"
)
_require_bounded_fraction(
next_value,
max_digits=MAX_COMBINATORICS_RESULT_RATIONAL_DIGITS,
label="polynomial-coefficient recurrence result",
)
minimum_size += _minimum_fraction_wire_bytes(next_value) * (
1 + (index in requested_index_set)
)
minimum_size += 32
if minimum_size > MAX_COMBINATORICS_RESULT_ARTIFACT_BYTES:
raise ValueError(
"the exact combinatorics result exceeds the durable artifact limit"
)
replay.append(next_value)
residuals.append(
(
index,
sum(
(
coefficients[offset] * replay[index - offset]
for offset in range(order + 1)
),
start=Fraction(),
),
)
)
_validate_result_artifact_size(
{
"backend": "sympy",
"backend_version": "1.14.0",
"coefficient_convention": coefficient_convention,
"polynomial_convention": polynomial_convention,
"determinism": "DETERMINISTIC",
"exactness": "EXACT_RATIONAL",
"recurrence_order": order,
"replay_prefix": [_fraction_wire(value) for value in replay],
"residuals": [
{"index": index, "value": _fraction_wire(value)}
for index, value in residuals
],
"replay_scope_end": end,
"scope": scope,
"values": [
{"index": index, "value": _fraction_wire(replay[index])}
for index in requested_indices
],
"verification": "UNVERIFIED",
}
)


def _validate_series_result_budget(
*,
numerator: tuple[CanonicalRational, ...],
Expand Down Expand Up @@ -799,6 +910,123 @@ def require_complete_replay_prefix(self) -> Self:
label="recurrence replay value",
)
indices = tuple(item.index for item in self.values)
if any(left >= right for left, right in pairwise(indices)):
raise ValueError("result indices must be strictly increasing")
if indices[-1] != self.replay_scope_end:
raise ValueError("the greatest requested index must bind replay_scope_end")
if any(item.value != self.replay_prefix[item.index] for item in self.values):
raise ValueError("indexed values must match the recurrence replay prefix")
if self.scope == "PREFIX" and indices != tuple(
range(self.replay_scope_end + 1)
):
raise ValueError(
"PREFIX results must contain consecutive indices from zero"
)
return self


class PolynomialCoefficientRecurrenceEvaluationRequest(ContractModel):
"""Evaluate a bounded exact polynomial-coefficient linear recurrence.

``coefficient_polynomials[j]`` is the ascending coefficient vector of
``p_j(n)`` in ``sum_{j=0}^d p_j(n) a[n-j] = 0``. The initial vector is
exactly ``a[0], ..., a[d-1]``.
"""

coefficient_polynomials: tuple[tuple[CanonicalRational, ...], ...] = Field(
min_length=2, max_length=MAX_LINEAR_RECURRENCE_ORDER + 1
)
initial_values: tuple[CanonicalRational, ...] = Field(
min_length=1, max_length=MAX_LINEAR_RECURRENCE_ORDER
)
coefficient_convention: Literal[
"SUM_P_J_OF_N_TIMES_A_N_MINUS_J_EQUALS_ZERO_FOR_J_FROM_0"
]
polynomial_convention: Literal["ASCENDING_POWERS_OF_N"]
scope: Literal["PREFIX", "INDICES"]
term_count: StrictInt | None = Field(
default=None, ge=1, le=MAX_LINEAR_RECURRENCE_INDEX + 1
)
indices: tuple[StrictInt, ...] = Field(
default=(), max_length=MAX_LINEAR_RECURRENCE_REQUESTED_INDICES
)

@model_validator(mode="after")
def require_bounded_regular_scope(self) -> Self:
order = len(self.coefficient_polynomials) - 1
if len(self.initial_values) != order:
raise ValueError("initial_values length must equal the recurrence order")
for polynomial in self.coefficient_polynomials:
if (
not polynomial
or len(polynomial) > MAX_P_RECURSIVE_POLYNOMIAL_DEGREE + 1
):
raise ValueError("coefficient polynomial degree is outside the bound")
_require_canonical_polynomial(
polynomial, label="recurrence polynomial coefficient"
)
for value in self.initial_values:
require_bounded_rational(
value,
max_digits=MAX_COMBINATORICS_INPUT_RATIONAL_DIGITS,
label="recurrence initial value",
)
if self.scope == "PREFIX":
if self.term_count is None or self.indices:
raise ValueError("PREFIX scope requires term_count and forbids indices")
requested = tuple(range(self.term_count))
else:
if self.term_count is not None or not self.indices:
raise ValueError(
"INDICES scope requires indices and forbids term_count"
)
if any(
index < 0 or index > MAX_LINEAR_RECURRENCE_INDEX
for index in self.indices
):
raise ValueError("indices are outside the recurrence bound")
if any(left >= right for left, right in pairwise(self.indices)):
raise ValueError("indices must be strictly increasing")
requested = self.indices
_validate_p_recursive_result_budget(
coefficient_polynomials=self.coefficient_polynomials,
initial_values=self.initial_values,
coefficient_convention=self.coefficient_convention,
polynomial_convention=self.polynomial_convention,
scope=self.scope,
requested_indices=requested,
)
return self


class PolynomialCoefficientRecurrenceEvaluationResult(ContractModel):
coefficient_convention: Literal[
"SUM_P_J_OF_N_TIMES_A_N_MINUS_J_EQUALS_ZERO_FOR_J_FROM_0"
]
polynomial_convention: Literal["ASCENDING_POWERS_OF_N"]
scope: Literal["PREFIX", "INDICES"]
recurrence_order: StrictInt = Field(ge=1, le=MAX_LINEAR_RECURRENCE_ORDER)
values: tuple[IndexedRationalValue, ...] = Field(
min_length=1, max_length=MAX_LINEAR_RECURRENCE_INDEX + 1
)
replay_prefix: tuple[CanonicalRational, ...] = Field(
min_length=1, max_length=MAX_LINEAR_RECURRENCE_INDEX + 1
)
residuals: tuple[IndexedRationalValue, ...] = Field(
max_length=MAX_LINEAR_RECURRENCE_INDEX + 1
)
replay_scope_end: StrictInt = Field(ge=0, le=MAX_LINEAR_RECURRENCE_INDEX)
exactness: Literal["EXACT_RATIONAL"] = "EXACT_RATIONAL"
determinism: Literal["DETERMINISTIC"] = "DETERMINISTIC"
backend: Literal["sympy"] = "sympy"
backend_version: Literal["1.14.0"] = "1.14.0"
verification: Literal["UNVERIFIED"] = "UNVERIFIED"

@model_validator(mode="after")
def require_complete_replay(self) -> Self:
if len(self.replay_prefix) != self.replay_scope_end + 1:
raise ValueError("replay_prefix must cover the complete bounded scope")
indices = tuple(item.index for item in self.values)
if any(left >= right for left, right in pairwise(indices)):
raise ValueError("result indices must be strictly increasing")
if indices[-1] != self.replay_scope_end:
Expand All @@ -809,6 +1037,21 @@ def require_complete_replay_prefix(self) -> Self:
raise ValueError(
"PREFIX results must contain consecutive indices from zero"
)
for value in self.replay_prefix:
require_bounded_rational(
value,
max_digits=MAX_COMBINATORICS_RESULT_RATIONAL_DIGITS,
label="polynomial-coefficient recurrence replay value",
)
residual_indices = tuple(item.index for item in self.residuals)
if residual_indices != tuple(
range(self.recurrence_order, self.replay_scope_end + 1)
):
raise ValueError(
"residuals must cover every recurrence step through replay_scope_end"
)
if any(item.value.as_fraction() != 0 for item in self.residuals):
raise ValueError("every recurrence residual must be exactly zero")
Comment thread
morluto marked this conversation as resolved.
return self


Expand Down
10 changes: 10 additions & 0 deletions src/jacobian/domains/combinatorics/checkers.py
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
CyclicPerfectDifferenceSetRequest,
IntegerSidonRequest,
LinearRecurrenceEvaluationRequest,
PolynomialCoefficientRecurrenceEvaluationRequest,
RationalGeneratingFunctionCoefficientsRequest,
)

Expand Down Expand Up @@ -61,6 +62,15 @@
replay_method="standard-library Fraction recurrence replay",
reason=_REASON,
),
ExactReplayCheckerDeclaration(
"combinatorics.recurrence.p_recursive.evaluate",
PolynomialCoefficientRecurrenceEvaluationRequest,
"check_polynomial_coefficient_recurrence_evaluation",
"combinatorics.p-recursive.fraction-residual-replay",
entrypoint_module=_ENTRYPOINT,
replay_method="standard-library Fraction polynomial recurrence replay",
reason=_REASON,
),
ExactReplayCheckerDeclaration(
"combinatorics.generating_function.coefficients.compute",
RationalGeneratingFunctionCoefficientsRequest,
Expand Down
Loading
Loading