prodigy.analysis.lowerbounds.synthesis

Synthesis of EVT (occupation) sub- and superinvariants with eventually geometric templates by linear programming, with exact rational certificates.

Template. Fix a denominator D = prod_i (1 - r_i X_i^{p_i}) and tail starts B_i. A template is given by its values h_n on the fundamental box F = prod_i [0, B_i + p_i - 1] ([0, B_i] if r_i = 0); beyond F the values continue geometrically, h_{n + p_i e_i} = r_i h_n for n_i >= B_i. Its generating function H = N / D is linear in h.

Constraints. H >= 0 iff h >= 0. The residual Phi(H) - H = g + T(H) - H has a numerator over the same D that is affine in h, and its coefficient-wise sign is decided exactly by a finite box of coefficients. Hence lower certificates (H <= Phi(H), finite mass; maximise the exit mass) and upper certificates (Phi(H) <= H; minimise an objective) are linear programs.

Exactness. The LP is solved in floating point (HiGHS). The optimal vertex is then reconstructed in exact rational arithmetic (the tight constraints form a square system that is solved with FLINT) and every constraint is re-checked exactly. Only exactly verified certificates are returned.

class Certificate(kind, calc, tail_start, numerator, exit_numerator, template_size, margin, time_build, time_lp, exit_mass=None, total_mass=None, extra=dict())[source]

Bases: object

An exactly verified template certificate H = numerator / D.

Parameters:
kind: str
calc: GFCalculus
tail_start: List[int]
numerator: Dict[Tuple[int, ...], Fraction]
exit_numerator: Dict[Tuple[int, ...], Fraction]
template_size: int
margin: float | None
time_build: float
time_lp: float
exit_mass: Any = None
total_mass: Any = None
extra: dict
property den: Denominator
to_json()[source]
Return type:

dict

scaled_expansion(calc, polys, box)[source]

Coefficients of P_j / D on the box prod_i [0, box_i] for all P_j at once, as an exact integer array M[n, j] = S(n) * coeff_n(P_j / D) with positive row scales S(n) = L * prod_i b_i^floor(n_i / p_i) (r_i = a_i / b_i, L a common denominator of the coefficients), and as a floating-point array of the unscaled coefficients. Returns (M, F, S) with rows in C order of the box.

Parameters:
class TemplateLP(calc, init, guard, body, tail_start, support=None)[source]

Bases: object

The linear program for one template shape (denominator, tail starts, optional support restriction).

The constraint data are kept as exact integers: row n of A h + b is scaled by a positive integer S(n), which does not change its sign.

Parameters:
basis_num: List[Dict[Tuple[int, ...], Fraction]]
margin_used: float | None
property size: int
numerator(h)[source]
Parameters:

h (Sequence[Fraction])

Return type:

Dict[Tuple[int, ...], Fraction]

exit_functional(query=None, moment=None)[source]

Coefficients of the linear functional h -> |[not guard] H| (restricted to query) or of the moment of variable moment of the exit part.

Parameters:
Return type:

List

exit_box_functional(query=None)[source]

Like exit_functional(), but only counting the exit mass inside the fundamental box (finite even if the template has rates >= 1).

Parameters:

query (tuple | None)

Return type:

List

column_scales()[source]

Expected magnitudes prod_i r_i^(n_i / p_i) of the template values (factor 1 for truncated variables). The values of a certificate typically decrease like this across the box, over many orders of magnitude. Scaling the LP variables by these magnitudes keeps the floating-point LP well-conditioned, lets the reconstruction tell small values from zeros, and makes the safety margins relative to the values.

Return type:

ndarray

solve(kind, objective=None, margins=(0.0, 1e-09, 1e-07))[source]

Solve the LP for a lower (kind = "lower", maximise) or upper (kind = "upper", minimise) certificate and return exact template values that pass the exact check, or None.

Parameters:
Return type:

List[Fraction] | None

check(h, kind)[source]

Exact verification: h >= 0 and the residual has the right sign on the whole positivity box.

Parameters:
Return type:

bool

certificate(h, kind)[source]
Parameters:
Return type:

Certificate

verify_certificate(calc, init, guard, body, numerator, kind)[source]

Independent exact check of a certificate H = numerator / D (does not use the LP data): H >= 0, and H <= g + T(H) with |H| < inf (lower) resp. g + T(H) <= H (upper).

Parameters:
Return type:

Tuple[bool, str]