Toolkit
Provide the building blocks of Sage scripts that assemble Lean proofs.
A script sees the Lean goal as a Problem, finds what the proof needs with the toolkit's search primitives, and
writes the proof with its Lean emitters. Importing this package imports SageMath.
Condition(text, expr, kind, discharged_by=None, bound=None)
dataclass
Hold a domain condition a symbolic expression of the problem needs.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
text
|
str
|
The Lean text of the condition, such as |
required |
expr
|
Expression | Matrix | None
|
The constrained expression, in Sage's symbolic ring, or |
required |
kind
|
str
|
|
required |
discharged_by
|
str | None
|
The hypothesis that states it, or |
None
|
bound
|
Expression | Matrix | None
|
The upper bound of an |
None
|
Coordinates(n)
dataclass
The coordinates operators act in: n Sage variables, rendered in Lean as y (one) or y i (several).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
n
|
int
|
The number of coordinates. |
required |
symbols
property
Return the Sage coordinates x0, x1, ….
multiplication(e)
Return the operator of multiplication by a polynomial in the coordinates.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
e
|
object
|
The polynomial (a Sage expression in |
required |
Returns:
| Type | Description |
|---|---|
Operator
|
The operator. |
Source code in src/veriphy/toolkit/_operators.py
103 104 105 106 107 108 109 110 111 112 113 | |
partial(i)
Return the partial derivative along the coordinate i (deriv in one variable).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
i
|
int
|
The coordinate. |
required |
Returns:
| Type | Description |
|---|---|
Operator
|
The operator. |
Source code in src/veriphy/toolkit/_operators.py
115 116 117 118 119 120 121 122 123 124 125 126 127 | |
render(e)
Return a polynomial in the coordinates as Lean text in the bound variable y.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
e
|
object
|
A polynomial with rational coefficients in the coordinates. |
required |
Returns:
| Type | Description |
|---|---|
str
|
The text. |
Source code in src/veriphy/toolkit/_operators.py
79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 | |
scalar(c)
Return multiplication by a rational constant.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
c
|
object
|
The constant. |
required |
Returns:
| Type | Description |
|---|---|
Operator
|
The operator. |
Source code in src/veriphy/toolkit/_operators.py
129 130 131 132 133 134 135 136 137 138 | |
Definition(function, var, body, hyp, text)
dataclass
Hold an explicit definition of an unknown function, from a hypothesis x = fun s => body.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
function
|
str
|
The function's Sage name. |
required |
var
|
Expression
|
The variable of the body, a Sage symbol. |
required |
body
|
Expression | None
|
The body, in |
required |
hyp
|
str
|
The hypothesis stating the definition. |
required |
text
|
str
|
The Lean text of the function (the lambda). |
required |
Derivative(var, body, point, function, at)
dataclass
Hold a derivative the translation met, deriv f point.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
var
|
Expression
|
The variable of differentiation, a Sage symbol. |
required |
body
|
Expression | None
|
The function's body, in |
required |
point
|
Expression | None
|
The point, over the problem's variables. |
required |
function
|
str
|
The Lean text of the function. |
required |
at
|
str
|
The Lean text of the point. |
required |
ExistsFunction(function, lean, conjuncts)
dataclass
Hold a goal ∃ x, C₁ ∧ C₂ ∧ … over an unknown function.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
function
|
str
|
The function's Sage name. |
required |
lean
|
str
|
The binder's Lean name. |
required |
conjuncts
|
tuple[tuple[Expression | None, Expression | None], ...]
|
Each conjunct as its universally quantified variable ( |
required |
FieldContext(generator, modulus, fact, setup)
dataclass
How a field's generator appears in Lean.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
generator
|
str
|
The generator's Lean text, such as |
required |
modulus
|
Polynomial | None
|
Its minimal polynomial over ℚ, in |
required |
fact
|
str | None
|
The name of the Lean fact |
required |
setup
|
Lean | None
|
The tactic establishing the fact, or nothing when the goal's hypotheses already state it. |
required |
Fusion(labels, dual, rules, f_values=field(default_factory=dict), r_values=field(default_factory=dict), field='rational')
dataclass
Multiplicity-free fusion data on labels 0 … n-1, the unit first.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
labels
|
list[str]
|
Names of the simple objects. |
required |
dual
|
list[int]
|
The dual of each label. |
required |
rules
|
dict[tuple[int, int], list[int]]
|
|
required |
f_values
|
dict[Key, FieldElement]
|
|
field(default_factory=dict)
|
r_values
|
dict[Triple, FieldElement]
|
|
field(default_factory=dict)
|
field
|
str
|
|
'rational'
|
size
property
Return the number of labels.
f(*labels)
Return (F^{abc}_d)_{ef} for the labels a, b, c, d, e, f, zero when inadmissible.
Source code in src/veriphy/toolkit/_fusion.py
59 60 61 62 63 64 | |
n(a, b, c)
Return the multiplicity of c in a ⊗ b.
Source code in src/veriphy/toolkit/_fusion.py
55 56 57 | |
r(a, b, c)
Return R^{ab}_c, zero when inadmissible.
Source code in src/veriphy/toolkit/_fusion.py
66 67 68 | |
Hyp(name, poly, rel, text='', expr=None)
dataclass
Hold one hypothesis or goal of a problem, as scripts see it.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
name
|
str | None
|
The Lean hypothesis name, or |
required |
poly
|
MPolynomial | None
|
The polynomial |
required |
rel
|
str | None
|
The relation tag, one of |
required |
text
|
str
|
The Lean text of the proposition. |
''
|
expr
|
Expression | Matrix | None
|
The symbolic form |
None
|
Lean(text, kind)
dataclass
Hold a piece of Lean source text and its syntactic category.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
text
|
str
|
The Lean source. |
required |
kind
|
str
|
|
required |
Examples:
>>> Lean('ring1', 'tactic')
Lean(text='ring1', kind='tactic')
__post_init__()
Reject an unknown syntactic category.
Source code in src/veriphy/toolkit/_lean.py
32 33 34 35 36 | |
__str__()
Return the Lean source.
Source code in src/veriphy/toolkit/_lean.py
38 39 40 | |
MatrixIndex(rows, cols, text)
dataclass
Hold the index type of a matrix indexed by sums of Fin types, such as Fin 1 ⊕ Fin 3.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
rows
|
tuple[int, ...]
|
The sizes of the row index's summands, in order. |
required |
cols
|
tuple[int, ...]
|
The sizes of the column index's summands, in order. |
required |
text
|
str
|
The matrix type's Lean text. |
required |
Operator(act, lean, order)
dataclass
A linear differential operator, with its action on Sage expressions and on Lean function texts.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
act
|
Callable[[Expression], Expression]
|
The action on a Sage expression in the coordinates. |
required |
lean
|
Callable[[str], str]
|
The action on the Lean text of a function, returning the Lean text of a function. |
required |
order
|
int
|
The highest derivative order it applies. |
required |
__add__(other)
Return the sum.
Source code in src/veriphy/toolkit/_operators.py
42 43 44 45 46 47 48 | |
__mul__(other)
Return the composition self ∘ other.
Source code in src/veriphy/toolkit/_operators.py
38 39 40 | |
__sub__(other)
Return the difference.
Source code in src/veriphy/toolkit/_operators.py
50 51 52 53 54 55 56 | |
Problem(ring, hyps, goal_kind, goal=None, binders=list(), body=list(), atoms=dict(), carrier='', lhs=None, rhs=None, atom_types=dict(), domain=list(), symbols=dict(), tables=(lambda: (load_core_table(),))(), typed=list(), derivatives=list(), functions=dict(), definitions=list(), exists_function=None, matrix_indices=list())
dataclass
Hold a serialized Lean problem bound to Sage objects.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
ring
|
MPolynomialRing_base
|
The polynomial ring over the problem's atoms. |
required |
hyps
|
list[Hyp]
|
The hypotheses. |
required |
goal_kind
|
str
|
One of |
required |
goal
|
Hyp | None
|
The goal of a |
None
|
binders
|
list[MPolynomial]
|
The generators bound by an |
list()
|
body
|
list[Hyp]
|
The constraints of an |
list()
|
atoms
|
dict[str, str]
|
The Lean text of each variable, by variable name. |
dict()
|
carrier
|
str
|
The Lean text of the type the problem's polynomials live in (such as |
''
|
lhs
|
Side | None
|
The left side of a relation goal, when the goal has a polynomial form. |
None
|
rhs
|
Side | None
|
The right side of a relation goal, when the goal has a polynomial form. |
None
|
atom_types
|
dict[str, str]
|
The Lean type of each variable ( |
dict()
|
domain
|
list[Condition]
|
The domain conditions the problem's symbolic expressions need. |
list()
|
symbols
|
dict[str, Expression]
|
The variables as symbolic-ring variables, by name, for symbolic work. |
dict()
|
tables
|
tuple[Table, ...]
|
The translation tables in force, core first. |
(lambda: (load_core_table(),))()
|
typed
|
list[tuple[Expression, str]]
|
The sub-expressions Lean computes at another type ( |
list()
|
derivatives
|
list[Derivative]
|
The derivatives the translation met, in the order it met them. |
list()
|
functions
|
dict[str, tuple[str, int]]
|
The unknown functions, by Sage name: their Lean name and arity. |
dict()
|
definitions
|
list[Definition]
|
Explicit definitions of unknown functions from the hypotheses. |
list()
|
exists_function
|
ExistsFunction | None
|
The goal's existential over an unknown function, when it is one. |
None
|
matrix_indices
|
list[MatrixIndex]
|
The index types of the matrices indexed by sums of |
list()
|
find_hyp(name, allowed, family)
Find the hypothesis named name, checking its relation is usable by family.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
name
|
str
|
The hypothesis name. |
required |
allowed
|
tuple[str, ...]
|
The relation tags |
required |
family
|
str
|
The proof shape asking, named in errors. |
required |
Returns:
| Type | Description |
|---|---|
Hyp
|
The hypothesis. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If no hypothesis has that name, or its relation is not in |
Source code in src/veriphy/toolkit/_problem.py
361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 | |
to_namespace()
Return the names a script sees.
Returns:
| Type | Description |
|---|---|
dict[str, object]
|
|
dict[str, object]
|
|
Source code in src/veriphy/toolkit/_problem.py
385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 | |
RewriteCandidate(lemma, reverse, side, namespace)
dataclass
Hold a rewrite the problem's tables offer for its goal, with side conditions filled in where they could be.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
lemma
|
str
|
The lemma name. |
required |
reverse
|
bool
|
Rewrite right to left. |
required |
side
|
tuple[str, ...]
|
The side conditions as Lean text over the goal's atoms. |
required |
namespace
|
str
|
The table the entry came from. |
required |
emit(problem, proofs=None, at=None)
Return the rewrite step, passing each side condition as (by assumption) or a supplied proof.
Sage orders the arguments of a commutative pattern its own way, so a stated side condition is passed as
(by assumption), which Lean runs after unifying the lemma with the goal and which therefore finds the
right hypothesis whatever the order.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
problem
|
Problem
|
The problem. |
required |
proofs
|
Mapping[str, Lean | str] | None
|
A tactic proving a side condition no hypothesis states, by its text. |
None
|
at
|
str | None
|
A hypothesis to rewrite instead of the goal. |
None
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If a side condition is neither stated nor supplied, naming it. |
Source code in src/veriphy/toolkit/_symbolic_emit.py
491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 | |
Side(poly, text)
dataclass
Hold one side of a relation goal, as scripts see it.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
poly
|
MPolynomial
|
The side as a polynomial of the problem's ring. |
required |
text
|
str
|
The side's Lean text, exactly as the goal writes it. |
required |
Table(namespace, functions=(), constants=(), coercions=(), rewrites=(), conventions=())
dataclass
Hold one namespace's entries.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
namespace
|
str
|
|
required |
functions
|
tuple[FunctionEntry, ...]
|
The function entries. |
()
|
constants
|
tuple[ConstantEntry, ...]
|
The constant entries. |
()
|
coercions
|
tuple[str, ...]
|
The coercions translated as their argument. |
()
|
rewrites
|
tuple[RewriteEntry, ...]
|
The rewrite entries. |
()
|
conventions
|
tuple[tuple[str, str], ...]
|
The conventions the namespace fixes, as |
()
|
adjoint_matrices(table)
Return the matrices of ad eᵢ in the basis: column l holds the coordinates of ⁅eᵢ, eₗ⁆.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
table
|
Table
|
Structure constants, as |
required |
Returns:
| Type | Description |
|---|---|
list[Matrix]
|
One matrix per basis element. |
Source code in src/veriphy/toolkit/_lie.py
73 74 75 76 77 78 79 80 81 82 83 84 | |
associativity_violations(data)
Return the label tuples where the fusion rules fail associativity.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
data
|
Fusion
|
The fusion data. |
required |
Returns:
| Type | Description |
|---|---|
list[tuple[int, int, int, int]]
|
The failing |
Source code in src/veriphy/toolkit/_fusion.py
186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 | |
block_matrix_rows(blocks)
Stack matrices of the same width vertically.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
blocks
|
Sequence[Matrix]
|
The matrices. |
required |
Returns:
| Type | Description |
|---|---|
Matrix
|
The stacked matrix. |
Source code in src/veriphy/toolkit/_representation.py
193 194 195 196 197 198 199 200 201 202 | |
bound_proof(function, point, bound, *, upper=True)
Return a proof of f(point) < bound (or bound < f(point) with upper=False).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
function
|
str
|
|
required |
point
|
Rational | int
|
A rational point ( |
required |
bound
|
Rational | int
|
The rational bound. |
required |
upper
|
bool
|
Whether the bound is above the value. |
True
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the function has no remainder bound in mathlib, the point is out of range, or the bound does not hold (with the enclosure Sage computed). |
Examples:
>>> print(bound_proof('exp', 1, QQ(27183) / 10000))
exact lt_trans Real.exp_one_lt_d9 (by norm_num)
>>> try:
... bound_proof('gamma', QQ(1) / 3, 3)
... except CertificateError as error:
... print(str(error).split(';')[0])
no remainder bound is available for gamma in mathlib
Source code in src/veriphy/toolkit/_numerics.py
87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 | |
bracket_relations(basis, names, *, carrier='ℚ', definitions=True, pairs=None, entrywise_limit=0)
Return have facts ⁅eᵢ, eⱼ⁆ = Σ cᵢⱼₖ • eₖ for the basis, each proved in Lean.
Over ℤ or ℚ the kernel checker VeriphyCheck.bracket_eq_of_check proves each relation from the matrices (which
it unfolds); otherwise the proof is entrywise. The coefficients must be rational.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
basis
|
Sequence[Matrix]
|
The basis matrices. |
required |
names
|
Sequence[str]
|
The Lean terms naming them, in the same order (definitions, or matrix literals). |
required |
carrier
|
str
|
The Lean type of the entries. |
'ℚ'
|
definitions
|
bool
|
Whether the names are definitions an entrywise proof must unfold. |
True
|
pairs
|
Sequence[tuple[int, int]] | None
|
The pairs |
None
|
entrywise_limit
|
int
|
Prove entrywise up to this dimension even over ℤ or ℚ. |
0
|
Returns:
| Type | Description |
|---|---|
Lean
|
The facts, named |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If a structure constant is not rational. |
Examples:
>>> e, f, h = matrix(QQ, [[0, 1], [0, 0]]), matrix(QQ, [[0, 0], [1, 0]]), matrix(QQ, [[1, 0], [0, -1]])
>>> print(bracket_relations([e, f, h], ['e', 'f', 'h'], pairs=[(2, 0)]))
have hb_2_0 : ⁅h, e⁆ = 2 • e := VeriphyCheck.bracket_eq_of_check (by decide +kernel)
Source code in src/veriphy/toolkit/_lie.py
197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 | |
by_cases(name, proposition, positive, negative)
Split on a proposition, with one tactic block per branch.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
name
|
str
|
The hypothesis name in each branch (use |
required |
proposition
|
Lean
|
The proposition split on, a term. |
required |
positive
|
Lean
|
The block for the branch where it holds. |
required |
negative
|
Lean
|
The block for the branch where it fails. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Examples:
>>> print(by_cases('hx', term('x ≤ 0'), tactic('nlinarith'), tactic('positivity')))
by_cases hx : x ≤ 0
· nlinarith
· positivity
Source code in src/veriphy/toolkit/_emit.py
327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 | |
calc_chain(start, steps, problem)
Build a calc chain from start through each step's expression, every step with its own tactic.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
start
|
object
|
The first expression, a Lean term or a polynomial of the problem. |
required |
steps
|
Sequence[tuple[str, object, Lean]]
|
Triples of a relation ( |
required |
problem
|
Problem
|
The problem. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Raises:
| Type | Description |
|---|---|
VeriphyError
|
If there are no steps. |
Examples:
>>> from veriphy.toolkit import read_problem
>>> prob = read_problem({'vars': ['x0'], 'atoms': ['x'], 'goal': {'kind': 'false'}})
>>> print(calc_chain('(x0 + 1)^2', [('=', 'x0^2 + 2*x0 + 1', tactic('ring'))], prob))
calc x ^ 2 + 2 * x + 1
_ = x ^ 2 + 2 * x + 1 := by ring
Source code in src/veriphy/toolkit/_emit.py
294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 | |
canonical_commutator(left, right, hbar=None)
Return [A, B] as a multiple of the identity, for combinations of one coordinate's x and p.
With [x, x] = [p, p] = 0 and [x, p] = iℏ, [αₓ x + αₚ p, βₓ x + βₚ p] = iℏ (αₓ βₚ - αₚ βₓ).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
left
|
dict[str, object]
|
The coefficients of |
required |
right
|
dict[str, object]
|
Those of |
required |
hbar
|
object
|
The reduced Planck constant; the symbol |
None
|
Returns:
| Type | Description |
|---|---|
object
|
The scalar, simplified. |
Examples:
>>> lowering, raising = ladder_operators()
>>> canonical_commutator(lowering, raising)
1
>>> canonical_commutator(lowering, {'x': 1})
1/2*sqrt(2)*xi
Source code in src/veriphy/toolkit/_operators.py
405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 | |
cartan_matrix(cartan_type)
Return the Cartan matrix of a type in mathlib's convention (CartanMatrix.E 8, CartanMatrix.F₄, …).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
cartan_type
|
str
|
The type, as |
required |
Returns:
| Type | Description |
|---|---|
Matrix
|
The integer matrix. |
Examples:
>>> cartan_matrix('F4')
[ 2 -1 0 0]
[-1 2 -2 0]
[ 0 -1 2 -1]
[ 0 0 -1 2]
Source code in src/veriphy/toolkit/_lie.py
337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 | |
casimir(basis, form=None)
Return the quadratic Casimir Σᵢⱼ (B⁻¹)ᵢⱼ eᵢ eⱼ of the representation, for an invariant form B.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
basis
|
Sequence[Matrix]
|
The representation matrices, a basis of the Lie algebra. |
required |
form
|
Matrix | None
|
The invariant form's matrix in that basis; the Killing form when |
None
|
Returns:
| Type | Description |
|---|---|
Matrix
|
The Casimir matrix. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the form is degenerate (the Killing form of an algebra that is not semisimple). |
Examples:
>>> e, f, h = matrix(QQ, [[0, 1], [0, 0]]), matrix(QQ, [[0, 0], [1, 0]]), matrix(QQ, [[1, 0], [0, -1]])
>>> casimir([e, f, h])
[3/8 0]
[ 0 3/8]
Source code in src/veriphy/toolkit/_lie.py
120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 | |
change_of_basis_facts(p, rho, blocks)
Return facts ρ(x) * P = P * B(x) (block diagonal B) and P * P⁻¹ = 1.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
p
|
Matrix
|
The change of basis. |
required |
rho
|
Rep
|
The representation. |
required |
blocks
|
Rep
|
The block-diagonal matrices. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The facts |
Source code in src/veriphy/toolkit/_representation.py
471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 | |
characteristic_polynomial(m)
Return det(x I - M) of a rational matrix, whose roots are its eigenvalues.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
m
|
Matrix
|
The matrix. |
required |
Returns:
| Type | Description |
|---|---|
Polynomial
|
The polynomial in |
Source code in src/veriphy/toolkit/_numerics.py
242 243 244 245 246 247 248 249 250 251 | |
check_matrix_identity(lhs, rhs)
Check in Sage that two matrices over a field agree, before Lean does.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
lhs
|
Matrix
|
The left side. |
required |
rhs
|
Matrix
|
The right side. |
required |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If they differ, showing the difference. |
Source code in src/veriphy/toolkit/_number_field.py
311 312 313 314 315 316 317 318 319 320 321 322 323 | |
christoffel_proof(g, *, metric, unfold=())
Return a proof of a goal christoffel G k i j x = Γ for an explicit metric G at a point.
A constant metric's symbols vanish: the derivatives of its components are zero. Otherwise the proof states the
inverse metric, rewrites with it, expands the partial derivatives and closes by field_simp and ring; the
hypotheses that the inverse needs (a component nonzero) must be in the context.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
g
|
Matrix
|
The metric's matrix of expressions in the coordinates. |
required |
metric
|
str
|
The Lean term of the metric as the goal writes it (a definition name or |
required |
unfold
|
Sequence[str]
|
Definitions to unfold (the metric's name). |
()
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the metric is degenerate. |
Source code in src/veriphy/toolkit/_geometry.py
99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 | |
christoffel_symbols(g)
Return the nonzero Christoffel symbols Γᵏᵢⱼ of a metric, computed by SageManifolds.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
g
|
Matrix
|
The metric's matrix of expressions in the coordinates |
required |
Returns:
| Type | Description |
|---|---|
dict[tuple[int, int, int], object]
|
The symbols by |
Source code in src/veriphy/toolkit/_geometry.py
72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 | |
clebsch_gordan(two_j1, two_j2)
Return the Clebsch-Gordan change of basis T : Vⱼ₁ ⊗ Vⱼ₂ → ⊕ⱼ Vⱼ, in the Chevalley normalization.
The rows of each block J (from j1 + j2 down to |j1 - j2|) are the coefficients of the basis vectors
fᵏ v_J / k! of V_J on the product basis, so T intertwines the product representation with the direct sum
of spin representations.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
two_j1
|
int
|
Twice the first spin. |
required |
two_j2
|
int
|
Twice the second spin. |
required |
Returns:
| Type | Description |
|---|---|
tuple[Matrix, list[int]]
|
|
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the matrix built does not intertwine (a defect in its construction, checked in Sage). |
Examples:
>>> t, spins = clebsch_gordan(2, 1)
>>> spins, t.dimensions()
([3, 1], (6, 6))
Source code in src/veriphy/toolkit/_representation.py
493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 | |
clifford_facts(gammas, eta)
Return kernel-checked facts: the Clifford relation, four-gamma traces and two contractions.
The contractions are γ^μ γ_μ = 4 and γ^μ γ^ν γ_μ = -2 γ^ν.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
gammas
|
Sequence[Matrix]
|
The gamma matrices (Sage checks the Clifford relation first). |
required |
eta
|
Matrix
|
The metric. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The facts |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the Clifford relation fails. |
Source code in src/veriphy/toolkit/_clifford.py
155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 | |
clifford_violations(gammas, eta)
Return the index pairs where {γ^μ, γ^ν} = 2 η^{μν} fails.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
gammas
|
Sequence[Matrix]
|
The gamma matrices. |
required |
eta
|
Matrix
|
The metric. |
required |
Returns:
| Type | Description |
|---|---|
list[tuple[int, int]]
|
The failing pairs. |
Source code in src/veriphy/toolkit/_clifford.py
88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 | |
coefficients(x, which)
Return a value's rational coefficients on the power basis 1, ζ, … of its field, trailing zeros dropped.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
x
|
FieldElement | int
|
An element of |
required |
which
|
str
|
|
required |
Returns:
| Type | Description |
|---|---|
list[FieldElement]
|
The coefficients; empty for zero. |
Examples:
>>> coefficients(SQRT5.gen() / 2 - 1, 'sqrt5')
[-1, 1/2]
>>> coefficients(ZETA16.gen() ** 3, 'zeta16')
[0, 0, 0, 1]
Source code in src/veriphy/toolkit/_fusion.py
246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 | |
combination(weighted, problem)
Build the weighted sum w₁ * p₁ + … + wₖ * pₖ of proof terms, dropping zero weights.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
weighted
|
Sequence[tuple[object, Lean]]
|
Pairs of a weight (a rational or a polynomial of the problem) and a proof term. |
required |
problem
|
Problem
|
The problem whose atoms the weights are written over. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The sum, a term. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If every weight is zero. |
Examples:
>>> from veriphy.toolkit import read_problem
>>> prob = read_problem({'vars': ['x0'], 'atoms': ['a'], 'goal': {'kind': 'false'}})
>>> str(combination([(1, term('h1')), (0, term('h2')), (QQ(-1) / 2, term('h3')), ('x0', term('h4'))], prob))
'h1 + (-1 / 2) * h3 + (a) * h4'
Source code in src/veriphy/toolkit/_emit.py
87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 | |
commutation_facts(element, names, *, size, carrier='ℚ', definitions=True, entrywise_limit=0)
Return have facts C * eᵢ = eᵢ * C: the element (a Casimir) commutes with each basis matrix.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
element
|
str
|
The Lean term of the commuting matrix (a definition, or a literal). |
required |
names
|
Sequence[str]
|
The Lean terms of the basis matrices. |
required |
size
|
int
|
The matrices' dimension. |
required |
carrier
|
str
|
The Lean type of the entries. |
'ℚ'
|
definitions
|
bool
|
Whether the terms are definitions an entrywise proof must unfold. |
True
|
entrywise_limit
|
int
|
Prove entrywise up to this dimension even over ℤ or ℚ. |
0
|
Returns:
| Type | Description |
|---|---|
Lean
|
The facts, named |
Examples:
>>> print(commutation_facts('C', ['e'], size=2))
have hc_0 : C * e = e * C := VeriphyCheck.commute_of_check (by decide +kernel)
Source code in src/veriphy/toolkit/_lie.py
254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 | |
commutator(a, b)
Return [a, b] = a b - b a.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
a
|
Operator
|
An operator. |
required |
b
|
Operator
|
Another. |
required |
Returns:
| Type | Description |
|---|---|
Operator
|
The commutator. |
Source code in src/veriphy/toolkit/_operators.py
141 142 143 144 145 146 147 148 149 150 151 | |
complex_matrix_term(m)
Return a matrix over ℚ(i) as a Lean !![…] literal over ℂ.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
m
|
Matrix
|
The matrix, with entries in |
required |
Returns:
| Type | Description |
|---|---|
str
|
The literal. |
Examples:
>>> i = QuadraticField(-1, 'i').gen()
>>> complex_matrix_term(matrix([[0, -i], [i, 0]]))
'(!![0, (-1 * Complex.I); (Complex.I), 0] : Matrix (Fin 2) (Fin 2) ℂ)'
Source code in src/veriphy/toolkit/_operators.py
270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 | |
contraction_proof(names)
Return the proof of a contraction of explicit component arrays: expand the sums and close by ring.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
names
|
Sequence[str]
|
The |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Source code in src/veriphy/toolkit/_geometry.py
232 233 234 235 236 237 238 239 240 241 | |
contragredient_superalgebra(even_ops, factors, omega, coefficients=None)
Return the structure constants and parities of g₀ ⊕ V with the moment-map odd bracket.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
even_ops
|
Sequence[Matrix]
|
A basis of |
required |
factors
|
Sequence[int]
|
The simple factor of each basis element. |
required |
omega
|
Matrix
|
An invariant antisymmetric form on |
required |
coefficients
|
Sequence[RingElement] | None
|
The moment-map coefficients |
None
|
Returns:
| Type | Description |
|---|---|
tuple[Table, list[int]]
|
The table (even basis first, then the basis of |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the coefficients are not unique (a family; pass them), or no bracket exists. |
Source code in src/veriphy/toolkit/_superalgebra.py
309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 | |
coordinates(n)
Return the Sage coordinates x0, … of an n-dimensional chart.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
n
|
int
|
The dimension. |
required |
Returns:
| Type | Description |
|---|---|
list[object]
|
The symbols. |
Source code in src/veriphy/toolkit/_geometry.py
25 26 27 28 29 30 31 32 33 34 | |
create_ring(names)
Create the multivariate polynomial ring QQ[names], multivariate even for one name.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
names
|
list[str]
|
The variable names, valid identifiers. |
required |
Returns:
| Type | Description |
|---|---|
MPolynomialRing_base
|
The polynomial ring. |
Examples:
>>> create_ring(['x0', 'x1']).gens()
(x0, x1)
Source code in src/veriphy/toolkit/_problem.py
65 66 67 68 69 70 71 72 73 74 75 76 77 78 | |
cyclic_submodule(rho, v)
Return a basis (as columns) of the submodule the representation generates from v.
From a highest weight vector this is the irreducible module of that weight, inside the representation.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
rho
|
Rep
|
The representation's matrices. |
required |
v
|
Sequence[object]
|
The generating vector. |
required |
Returns:
| Type | Description |
|---|---|
Matrix
|
The basis, as the columns of a matrix. |
Source code in src/veriphy/toolkit/_representation.py
125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 | |
cyclotomic_context(n, zeta='ζ', primitive='hζ', name='hΦ')
Return ℚ(ζₙ) for a primitive root ζ with primitive : IsPrimitiveRoot ζ n among the hypotheses.
The fact Φₙ(ζ) = 0 is derived from mathlib's IsPrimitiveRoot.isRoot_cyclotomic and, for a prime power n,
the explicit Polynomial.cyclotomic_prime_pow_eq_geom_sum. For other n, state Φₙ(ζ) = 0 as a hypothesis
named name and pass primitive=None.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
n
|
int
|
The order of the root. |
required |
zeta
|
str
|
The root's Lean text. |
'ζ'
|
primitive
|
str | None
|
The name of the hypothesis |
'hζ'
|
name
|
str
|
The name of the fact |
'hΦ'
|
Returns:
| Type | Description |
|---|---|
FieldContext
|
The context. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If |
Examples:
>>> print(cyclotomic_context(16).modulus)
x^8 + 1
Source code in src/veriphy/toolkit/_number_field.py
118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 | |
d21_alpha(alpha)
Return D(2,1;α): sl2³ on 2 ⊗ 2 ⊗ 2, with moment-map coefficients (1, α, -1 - α).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
alpha
|
RingElement
|
The parameter (rational, or an element of a field of rational functions). |
required |
Returns:
| Type | Description |
|---|---|
tuple[Table, list[int]]
|
The structure constants (17-dimensional, 9 even and 8 odd) and the parities. |
Examples:
>>> table, parities = d21_alpha(QQ(2))
>>> len(table), sum(parities), super_jacobi_violations(table, parities)
(17, 8, [])
Source code in src/veriphy/toolkit/_superalgebra.py
347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 | |
decide()
Call decide, for decidable goals over finite domains.
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Examples:
>>> str(decide())
'decide'
Source code in src/veriphy/toolkit/_emit.py
259 260 261 262 263 264 265 266 267 268 269 | |
decomposition(rho, summands)
Return the change of basis to a direct sum of invariant subspaces, and the block-diagonal matrices.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
rho
|
Rep
|
The representation. |
required |
summands
|
Sequence[Matrix]
|
Bases (as columns) of invariant subspaces whose sum is the whole space. |
required |
Returns:
| Type | Description |
|---|---|
tuple[Matrix, Rep]
|
|
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the subspaces are not invariant or do not form a direct sum of the whole space. |
Source code in src/veriphy/toolkit/_representation.py
438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 | |
defining_representation(cartan_type)
Return Sage's defining representation of a simple Lie algebra: its Chevalley generators eᵢ, fᵢ, hᵢ.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
cartan_type
|
str
|
The type, as |
required |
Returns:
| Type | Description |
|---|---|
tuple[Rep, list[str]]
|
The generator matrices and their labels. |
Examples:
>>> rho, labels = defining_representation('A2')
>>> labels, rho[0].nrows()
(['e1', 'e2', 'f1', 'f2', 'h1', 'h2'], 3)
Source code in src/veriphy/toolkit/_representation.py
31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 | |
derivative_chain(body, var, order, problem, *, function_text=None, proofs=None)
Return facts dₖ : deriv (fun s => Bₖ₋₁) = fun s => Bₖ for k = 1 … order, and their names.
Each fact is proved at an arbitrary point by a composed HasDerivAt term. function_text states the first
function as the goal writes it, so that rewriting with d1 matches the goal.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
body
|
Expression
|
The function's body |
required |
var
|
Expression
|
The variable, a Sage symbol ending in |
required |
order
|
int
|
How many derivatives. |
required |
problem
|
Problem
|
The problem whose atoms name the parameters. |
required |
function_text
|
str | None
|
The Lean text of the first function, rendered from |
None
|
proofs
|
Mapping[str, str] | None
|
Tactics proving nonzero conditions no hypothesis states, by their Lean text. |
None
|
Returns:
| Type | Description |
|---|---|
tuple[list[Lean], list[str]]
|
The facts and their names. |
Source code in src/veriphy/toolkit/_ode.py
57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 | |
derivative_order(expr, function)
Return the highest order to which expr differentiates the unknown function named function.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
expr
|
Expression
|
A symbolic expression. |
required |
function
|
str
|
The Sage name of the unknown function. |
required |
Returns:
| Type | Description |
|---|---|
int
|
The order, 0 when the function is not differentiated. |
Examples:
>>> from sage.all import function
>>> t = SR.var('t'); f = function('F_x')
>>> derivative_order(diff(f(t), t, 2) + f(t), 'F_x')
2
Source code in src/veriphy/toolkit/_ode.py
25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 | |
det_certificate(m)
Return a proof term of A.det = d for an integer matrix, by an LU factorization over ℚ the kernel checks.
The factorization is Sage's, without pivoting; Cartan matrices (and any matrix whose leading minors are
nonzero) have one. The goal's matrix may be a definition (CartanMatrix.E 8) or a literal: the kernel unfolds it.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
m
|
Matrix
|
The integer matrix, as the goal states it. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The term, for |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the matrix is not square and integral, or needs pivoting. |
Examples:
>>> proof = str(det_certificate(matrix(ZZ, [[2, -1], [-1, 2]])))
>>> proof.startswith('VeriphyCheck.det_eq_of_lu_int (d := 3) (L := (!![1, 0; -1 / 2, 1] : ')
True
>>> '(U := (!![2, -1; 0, 3 / 2] : Matrix (Fin 2) (Fin 2) ℚ))' in proof
True
Source code in src/veriphy/toolkit/_lie.py
416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 | |
diagonalizable_exponential(a, parameter='t')
Return exp (t • A) for A diagonalizable over ℚ, and a proof of the goal exp (t • A) = E.
The goal's right side may be written with Real.exp, Real.cosh or Real.sinh: the entries are compared after
unfolding cosh and sinh into exponentials.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
a
|
Matrix
|
A rational matrix with rational eigenvalues and a basis of eigenvectors. |
required |
parameter
|
str
|
The Lean name of the real parameter |
't'
|
Returns:
| Type | Description |
|---|---|
tuple[Matrix, Lean]
|
The closed form (over Sage's symbolic ring, in a variable named as the parameter) and the tactic. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If |
Examples:
>>> e, proof = diagonalizable_exponential(matrix(QQ, [[0, 1], [1, 0]]), 'φ')
>>> e[0, 0]
1/2*e^(-φ) + 1/2*e^φ
Source code in src/veriphy/toolkit/_exponential.py
94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 | |
eigen_projectors(c)
Return the projectors onto the eigenspaces of a diagonalizable matrix with rational eigenvalues (a Casimir).
Each is Pₖ = Πₗ≠ₖ (C - λₗ) / (λₖ - λₗ).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
c
|
Matrix
|
The matrix. |
required |
Returns:
| Type | Description |
|---|---|
list[tuple[object, Matrix]]
|
|
Raises:
| Type | Description |
|---|---|
CertificateError
|
If an eigenvalue is irrational or the matrix is not diagonalizable. |
Source code in src/veriphy/toolkit/_representation.py
205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 | |
eigenvalue_proof(m, matrix_lean, a, b)
Return a proof of ∃ x : ℝ, (a < x ∧ x < b) ∧ (x • 1 - M).det = 0: an eigenvalue of a 3 by 3 matrix there.
The determinant is expanded to the characteristic polynomial, whose root on the interval root_proof certifies.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
m
|
Matrix
|
The rational 3 by 3 matrix. |
required |
matrix_lean
|
str
|
The matrix as the goal writes it (a literal over ℝ). |
required |
a
|
object
|
The interval's left end (from |
required |
b
|
object
|
The interval's right end. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the matrix is not 3 by 3, or the interval does not isolate a simple root. |
Source code in src/veriphy/toolkit/_numerics.py
254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 | |
exact_form_proof(f, n)
Return a proof of ∀ i x, extDeriv F ![i] x = ω i x for the 0-form F of a primitive f.
The goal's F is fun _ x => f x and its ω the component functions; each component's partial derivative is
expanded by simp and closed by ring.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
f
|
object
|
The primitive (only its existence matters to the proof; Sage checks it). |
required |
n
|
int
|
The dimension. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Source code in src/veriphy/toolkit/_geometry.py
188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 | |
exterior_square(rho)
Return the representation on Λ²V, in the basis eᵢ ∧ eⱼ (i < j).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
rho
|
Rep
|
The representation on |
required |
Returns:
| Type | Description |
|---|---|
tuple[Rep, list[tuple[int, int]]]
|
The matrices and the index pairs of the basis. |
Examples:
>>> wedge, pairs = exterior_square(defining_representation('A4')[0])
>>> wedge[0].nrows(), pairs[:2]
(10, [(0, 1), (0, 2)])
Source code in src/veriphy/toolkit/_representation.py
93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 | |
f4()
Return F(4): so(7) ⊕ sl2 on 8 ⊗ 2, the spinor tensor the doublet (40-dimensional, 24 even, 16 odd).
Returns:
| Type | Description |
|---|---|
tuple[Table, list[int]]
|
The structure constants and parities. |
Source code in src/veriphy/toolkit/_superalgebra.py
417 418 419 420 421 422 423 424 425 426 | |
fibonacci()
Return the Fibonacci category's fusion data, with F-symbols in a gauge over ℚ(√5).
The only nontrivial F-matrix is F^{τττ}_τ; its entries are solved from the pentagon equations with the gauge
fixed by (F^{τττ}_τ)_{1τ} = 1.
Returns:
| Type | Description |
|---|---|
Fusion
|
The data. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the pentagon equations have no solution in |
Source code in src/veriphy/toolkit/_fusion.py
106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 | |
field_identity(context, max_power=None)
Return a proof of a scalar identity over the field: the generator's fact, then field_reduce.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
context
|
FieldContext
|
The field's context. |
required |
max_power
|
int | None
|
The largest power of the generator after normalizing the goal. |
None
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Source code in src/veriphy/toolkit/_number_field.py
279 280 281 282 283 284 285 286 287 288 289 290 291 | |
field_invariant(f, eta)
Return F_{μν} F^{μν} for a field strength with lower indices and a constant metric.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
f
|
Matrix
|
The matrix |
required |
eta
|
Matrix
|
The metric (its own inverse up to the sign conventions of a diagonal |
required |
Returns:
| Type | Description |
|---|---|
object
|
The contraction, expanded. |
Examples:
>>> from sage.all import diagonal_matrix
>>> e1, b3 = var('E1 B3')
>>> f = matrix(SR, [[0, -e1, 0, 0], [e1, 0, -b3, 0], [0, b3, 0, 0], [0, 0, 0, 0]])
>>> field_invariant(f, diagonal_matrix(SR, [1, -1, -1, -1]))
2*B3^2 - 2*E1^2
Source code in src/veriphy/toolkit/_geometry.py
210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 | |
field_matrix_identity(context, max_power=None)
Return an entrywise proof of an identity between explicit matrices over the field (A * B = C, A = B, …).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
context
|
FieldContext
|
The field's context. |
required |
max_power
|
int | None
|
The largest power of the generator in a normalized entry (by default that of a product of two
reduced elements, enough for |
None
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Source code in src/veriphy/toolkit/_number_field.py
294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 | |
field_matrix_term(m, context)
Render a matrix over the field as a Lean !![…] literal.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
m
|
Matrix
|
The matrix. |
required |
context
|
FieldContext
|
The field's context. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The term. |
Source code in src/veriphy/toolkit/_number_field.py
220 221 222 223 224 225 226 227 228 229 230 231 | |
field_reduce(context, max_power=None)
Return a tactic closing a true identity over the field: normalize, reduce the generator's powers, normalize.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
context
|
FieldContext
|
The field's context, whose fact is in scope. |
required |
max_power
|
int | None
|
The largest power of the generator the normalized goal can contain (twice the degree minus two for a product of two reduced elements, the default). |
None
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Examples:
>>> reduce = str(field_reduce(quadratic_context(2)))
>>> reduce.startswith('(try ring_nf) <;> (set_option linter.unusedSimpArgs false in try simp only [show (')
True
>>> reduce.endswith('^ 2 = 2 by linear_combination (1) * hs]) <;> ring_nf')
True
Source code in src/veriphy/toolkit/_number_field.py
250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 | |
field_simp(lemmas=())
Call field_simp, optionally with extra simp lemmas (such as nonzero-denominator facts).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
lemmas
|
Sequence[str]
|
Lemma or hypothesis names. |
()
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Examples:
>>> str(field_simp(['hx']))
'field_simp [hx]'
Source code in src/veriphy/toolkit/_emit.py
226 227 228 229 230 231 232 233 234 235 236 237 238 239 | |
field_simp_clearing(problem, proofs=None)
Clear the problem's denominators with field_simp, passing a fact for every nonzero-denominator condition.
A denominator condition neither discharged nor supplied raises CertificateError, as in require_domain.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
problem
|
Problem
|
The problem. |
required |
proofs
|
Mapping[str, Lean | str] | None
|
A tactic proving a denominator condition no hypothesis discharges, by the condition's text. |
None
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic, preceded by a |
Examples:
>>> from veriphy.toolkit import read_problem
>>> prob = read_problem({'vars': ['x0', 'x1'], 'atoms': ['y', 'x'], 'goal': {'kind': 'false'},
... 'domain': [{'expr': 'x0', 'kind': 'ne', 'text': 'y ≠ 0', 'discharged_by': 'hy'},
... {'expr': 'x1^2 + 1', 'kind': 'ne', 'text': 'x ^ 2 + 1 ≠ 0'}]})
>>> print(field_simp_clearing(prob, proofs={'x ^ 2 + 1 ≠ 0': 'positivity'}))
have hd : x ^ 2 + 1 ≠ 0 := by positivity
field_simp [hy, hd]
Source code in src/veriphy/toolkit/_symbolic_emit.py
393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 | |
fierz_basis(gammas, eta)
Return the 16 matrices 1, γ^μ, γ^μ γ^ν (μ < ν), γ^μ γ⁵, γ⁵ and their classes S, V, T, A, P (0 … 4).
σ^{μν} = (i/2)[γ^μ, γ^ν] = i γ^μ γ^ν for μ ≠ ν; the factor i is dropped, which rescales the tensor class.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
gammas
|
Sequence[Matrix]
|
The gamma matrices. |
required |
eta
|
Matrix
|
The metric. |
required |
Returns:
| Type | Description |
|---|---|
tuple[list[Matrix], list[int]]
|
The basis and the class of each element. |
Source code in src/veriphy/toolkit/_clifford.py
192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 | |
fierz_coefficients(gammas, eta)
Return the 5×5 Fierz matrix C with Σ_{A∈X} (Γ_A)ᵢⱼ (Γ^A)ₖₗ = Σ_Y C_XY Σ_{B∈Y} (Γ_B)ᵢₗ (Γ^B)ₖⱼ.
Γ^A is the inverse of Γ_A (each squares to ±1).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
gammas
|
Sequence[Matrix]
|
The gamma matrices. |
required |
eta
|
Matrix
|
The metric. |
required |
Returns:
| Type | Description |
|---|---|
Matrix
|
The coefficients. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the rearrangement has no solution (the basis is not complete). |
Examples:
>>> c = fierz_coefficients(*gamma_matrices())
>>> 4 * c[0]
(1, 1, 1, 1, 1)
Source code in src/veriphy/toolkit/_clifford.py
212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 | |
fierz_fact(gammas, eta)
Return the Fierz coefficients and a fact proving the rearrangement for every index and class.
The fact is stated with 4 C (integers) and checked by the kernel over ℤ[i].
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
gammas
|
Sequence[Matrix]
|
The gamma matrices. |
required |
eta
|
Matrix
|
The metric. |
required |
Returns:
| Type | Description |
|---|---|
tuple[Matrix, Lean]
|
|
Source code in src/veriphy/toolkit/_clifford.py
255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 | |
find_gauge(reference, target)
Return a gauge taking the reference data to the target's, or None when they are not gauge equivalent.
The unknowns u^{ab}_c (one per admissible triple, nonzero) satisfy polynomial equations; gauge freedom left over
(gauges fixing the data) is spent by setting unknowns to 1 while the system stays consistent, and the remaining
finite system is solved in the data's field.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
reference
|
Fusion
|
The data in Sage's gauge. |
required |
target
|
Fusion
|
The data in the goal's gauge, same labels and rules. |
required |
Returns:
| Type | Description |
|---|---|
Gauge | None
|
The gauge, on the admissible triples where it is not 1. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the fusion rules differ. |
Examples:
>>> fib = fibonacci()
>>> u = find_gauge(fib, gauge_transform(fib, {(1, 1, 1): 2}))
>>> gauge_transform(fib, u).f_values == gauge_transform(fib, {(1, 1, 1): 2}).f_values
True
Source code in src/veriphy/toolkit/_fusion.py
560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 | |
fresh_name(problem, base, taken=())
Choose a hypothesis name unused in the problem.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
problem
|
Problem
|
The problem whose hypothesis names are taken. |
required |
base
|
str
|
The preferred name. |
required |
taken
|
Sequence[str]
|
Further names to avoid. |
()
|
Returns:
| Type | Description |
|---|---|
str
|
|
Examples:
>>> from veriphy.toolkit import read_problem
>>> prob = read_problem({'vars': ['x0'], 'hyps': [{'name': 'h', 'text': 'True'}], 'goal': {'kind': 'false'}})
>>> fresh_name(prob, 'h'), fresh_name(prob, 'k')
('h_1', 'k')
Source code in src/veriphy/toolkit/_emit.py
35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 | |
fusion_data_term(data)
Return the data as a Lean FusionData.RepData n term, values as coefficient lists.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
data
|
Fusion
|
The fusion data. |
required |
Returns:
| Type | Description |
|---|---|
str
|
The term. |
Source code in src/veriphy/toolkit/_fusion.py
290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 | |
fusion_facts(data, *, braided, symbols=True)
Return the fact that the data form a fusion category (and a braided one), checked in Sage, then by the kernel.
The kernel checks the equations once on coefficient lists, on admissible labels; the asset's theorems give them
in every ℚ-algebra at every ζ with ζ ^ m = r (ζ² = 5 for ℚ(√5), ζ⁸ = -1 for ℚ(ζ₁₆)), so the fact
applies over ℝ or ℂ and at every Galois conjugate.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
data
|
Fusion
|
The fusion data. |
required |
braided
|
bool
|
Whether to state the hexagons too. |
required |
symbols
|
bool
|
Whether to state the pentagon ( |
True
|
Returns:
| Type | Description |
|---|---|
Lean
|
The fact |
Lean
|
ring axioms of the rules alone. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If associativity, the pentagon or (when braided) the hexagons fail in Sage. |
Source code in src/veriphy/toolkit/_fusion.py
469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 | |
fusion_proof(data, *, braided, root=True)
Return a proof of a goal FusionData.IsFusion (RepData.toData E ζ) (or IsBraidedFusion) for explicit E.
Sage checks the data first, naming what fails; the kernel then checks the goal's own E (a definition or the
literal of fusion_data_term), so the data must be Sage's in the goal's gauge (see gauge_mismatch).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
data
|
Fusion
|
The fusion data the goal states. |
required |
braided
|
bool
|
Whether the goal is |
required |
root
|
bool
|
Whether |
True
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If associativity, the pentagon or (when braided) the hexagons fail. |
Source code in src/veriphy/toolkit/_fusion.py
376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 | |
fusion_rules(cartan_type, level)
Return the fusion rules of a quantum group at a root of unity, from Sage's FusionRing.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
cartan_type
|
str
|
The type, as |
required |
level
|
int
|
The level. |
required |
Returns:
| Type | Description |
|---|---|
Fusion
|
The fusion data with rules and duals (F- and R-symbols to be supplied). |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If a fusion multiplicity exceeds 1: the asset covers multiplicity-free categories only. |
Examples:
>>> ising = fusion_rules('A1', 2)
>>> ising.labels, ising.rules[(1, 1)]
(['A12(0)', 'A12(1)', 'A12(2)'], [0, 2])
Source code in src/veriphy/toolkit/_fusion.py
71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 | |
g3()
Return G(3): G₂ ⊕ sl2 on 7 ⊗ 2 (31-dimensional, 17 even and 14 odd).
Returns:
| Type | Description |
|---|---|
tuple[Table, list[int]]
|
The structure constants and parities. |
Source code in src/veriphy/toolkit/_superalgebra.py
370 371 372 373 374 375 376 377 378 379 | |
gamma5(gammas, eta)
Return γ⁵, the product γ⁰ γ¹ γ² γ³ times i or 1, whichever squares to the identity.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
gammas
|
Sequence[Matrix]
|
The gamma matrices. |
required |
eta
|
Matrix
|
The metric (unused: both signatures give |
required |
Returns:
| Type | Description |
|---|---|
Matrix
|
|
Examples:
>>> gammas, eta = gamma_matrices()
>>> g5 = gamma5(gammas, eta)
>>> g5 * g5 == 1, all(g5 * g + g * g5 == 0 for g in gammas)
(True, True)
Source code in src/veriphy/toolkit/_clifford.py
67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 | |
gamma_matrices(representation='dirac', signature='mostly_minus')
Return γ⁰ … γ³ and the metric η, over ℚ(i).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
representation
|
str
|
|
'dirac'
|
signature
|
str
|
|
'mostly_minus'
|
Returns:
| Type | Description |
|---|---|
tuple[list[Matrix], Matrix]
|
The four matrices and |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the representation or signature is unknown. |
Examples:
>>> gammas, eta = gamma_matrices()
>>> clifford_violations(gammas, eta)
[]
Source code in src/veriphy/toolkit/_clifford.py
31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 | |
gauge_facts(reference, target, u)
Return the fact that the target is the reference in the gauge u, checked in Sage, then by the kernel.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
reference
|
Fusion
|
The data in Sage's gauge. |
required |
target
|
Fusion
|
The data in the goal's gauge. |
required |
u
|
Gauge
|
The gauge (from |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The fact |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If |
Source code in src/veriphy/toolkit/_fusion.py
659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 | |
gauge_mismatch(reference, target)
Return a report on how the target's F- and R-symbols differ from the reference's, and the gauge relating them.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
reference
|
Fusion
|
The data in Sage's gauge. |
required |
target
|
Fusion
|
The data in the goal's gauge. |
required |
Returns:
| Type | Description |
|---|---|
str
|
The report: the differing symbols, then the gauge (or that none exists in the field: then the target is a |
str
|
different category, or needs a field extension). |
Examples:
>>> fib = fibonacci()
>>> print(gauge_mismatch(fib, gauge_transform(fib, {(1, 1, 1): 2})).splitlines()[-1])
gauge: u[(1, 1, 1)] = 2
Source code in src/veriphy/toolkit/_fusion.py
626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 | |
gauge_proof(reference, target, u, *, root=True)
Return a proof of a goal FusionData.GaugeRelated (E.toData ζ) (E'.toData ζ) (eval U) (eval Uinv).
The goal's gauge functions are fun a b c => FusionData.Coeffs.eval ζ (U a b c) with U the lookup that
gauge_term(u, data) prints; Sage checks that u relates the data, the kernel checks the goal's.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
reference
|
Fusion
|
The data in Sage's gauge. |
required |
target
|
Fusion
|
The data in the goal's gauge. |
required |
u
|
Gauge
|
The gauge (from |
required |
root
|
bool
|
Whether |
True
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If |
Source code in src/veriphy/toolkit/_fusion.py
407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 | |
gauge_term(u, data, *, inverse=False)
Return a gauge (or its inverse) as a Lean Fin n → Fin n → Fin n → List ℚ, 1 where unlisted.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
u
|
Gauge
|
The gauge. |
required |
data
|
Fusion
|
The data it acts on (for the labels and the field). |
required |
inverse
|
bool
|
Whether to return the inverse gauge. |
False
|
Returns:
| Type | Description |
|---|---|
str
|
The term. |
Examples:
>>> term = gauge_term({(1, 1, 1): 2}, fibonacci(), inverse=True)
>>> '(((1 : Fin 2), (1 : Fin 2), (1 : Fin 2)), [(1 / 2)])' in term, term.endswith('.getD [1]')
(True, True)
Source code in src/veriphy/toolkit/_fusion.py
437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 | |
gauge_transform(data, u)
Return the data in another gauge.
(F'^{abc}_d)_{ef} = u^{ab}_e u^{ec}_d / (u^{bc}_f u^{af}_d) (F^{abc}_d)_{ef} and
R'^{ab}_c = u^{ba}_c / u^{ab}_c R^{ab}_c; unlisted u are 1.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
data
|
Fusion
|
The fusion data. |
required |
u
|
Gauge
|
The gauge, on admissible triples. |
required |
Returns:
| Type | Description |
|---|---|
Fusion
|
The transformed data, which satisfies the same pentagon and hexagon equations. |
Examples:
>>> fib = fibonacci()
>>> other = gauge_transform(fib, {(1, 1, 1): 2})
>>> other.f(1, 1, 1, 1, 1, 0) == 4 * fib.f(1, 1, 1, 1, 1, 0), pentagon_violations(other)
(True, 0)
Source code in src/veriphy/toolkit/_fusion.py
519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 | |
gaussian_matrix_term(m)
Return a matrix over ℤ[i] as a Lean !![…] literal over GaussianInt.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
m
|
Matrix
|
The matrix. |
required |
Returns:
| Type | Description |
|---|---|
str
|
The literal. |
Examples:
>>> gaussian_matrix_term(PAULI[1])
'(!![0, ⟨0, -1⟩; ⟨0, 1⟩, 0] : Matrix (Fin 2) (Fin 2) GaussianInt)'
Source code in src/veriphy/toolkit/_clifford.py
116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 | |
gosper_closed_form(f)
Return Σ_{k<n} f(k) in closed form by Gosper's algorithm.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
f
|
Expr
|
The summand in |
required |
Returns:
| Type | Description |
|---|---|
Expr
|
The closed form in |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the sum is not Gosper-summable. |
Examples:
>>> sp.combsimp(gosper_closed_form(K * sp.factorial(K)))
factorial(n) - 1
Source code in src/veriphy/toolkit/_summation.py
165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 | |
gosper_proof()
Return the induction proving ∑ k ∈ Finset.range n, f k = S n once Sage has checked S is the antidifference.
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic: induction on |
Source code in src/veriphy/toolkit/_summation.py
188 189 190 191 192 193 194 195 196 197 198 | |
graded_commutator(x, y, px, py)
Return x y - (-1)^(|x||y|) y x.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
x
|
Matrix
|
A homogeneous supermatrix. |
required |
y
|
Matrix
|
Another. |
required |
px
|
int
|
The parity of |
required |
py
|
int
|
The parity of |
required |
Returns:
| Type | Description |
|---|---|
Matrix
|
The graded commutator. |
Source code in src/veriphy/toolkit/_superalgebra.py
32 33 34 35 36 37 38 39 40 41 42 43 44 | |
guess_recurrence(terms, order=2)
Guess a holonomic recurrence for a sequence from its first terms, with ore_algebra.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
terms
|
Sequence[object]
|
The first terms of the sequence. |
required |
order
|
int
|
The order of the recurrence sought. |
2
|
Returns:
| Type | Description |
|---|---|
object
|
The guessed operator (an |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If |
Source code in src/veriphy/toolkit/_summation.py
266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 | |
has_deriv_at(expr, var, point, problem, proofs=None)
Build a proof term of HasDerivAt (fun var => expr) _ point from mathlib's derivative lemmas.
The term composes hasDerivAt_const, hasDerivAt_id', .add, .mul, .div, .const_mul, .pow, .sqrt,
.rpow_const, .exp, .log, .sin and .cos. The derivative it proves is mathlib's unsimplified form, which
a proof states as Sage's derivative by HasDerivAt.congr_deriv and ring_nf or field_simp. A quotient, log,
sqrt or real power needs its argument nonzero at the point: a hypothesis stating it, or a tactic in proofs.
Any other variable of the expression is a constant, so the same term proves partial derivatives.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
expr
|
object
|
The function's body, an expression in |
required |
var
|
Expression
|
The variable of differentiation, a Sage symbol. |
required |
point
|
object
|
The point, an expression over the problem's atoms. |
required |
problem
|
Problem
|
The problem whose atoms name the variables. |
required |
proofs
|
Mapping[str, str] | None
|
Tactics proving side conditions no hypothesis states, by their Lean text. |
None
|
A side condition neither stated nor supplied, or a function with no derivative lemma, raises CertificateError
naming it.
Returns:
| Type | Description |
|---|---|
Lean
|
The proof term. |
Examples:
>>> from sage.all import exp, log
>>> from veriphy.toolkit import read_problem
>>> prob = read_problem({'vars': ['x0'], 'atoms': ['a'], 'goal': {'kind': 'false'}})
>>> t = SR.var('t')
>>> str(has_deriv_at(t**2 * exp(t), t, 1, prob))
"(((hasDerivAt_id' (1 : ℝ)).pow 2).mul ((hasDerivAt_id' (1 : ℝ)).exp))"
>>> has_deriv_at(log(t), t, prob.symbols['x0'], prob)
Traceback (most recent call last):
...
veriphy.core._errors.CertificateError: the derivative needs 'a ≠ 0', which no hypothesis states; pass its proof
Source code in src/veriphy/toolkit/_derivative.py
179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 | |
has_deriv_at_proof(expr, var, point, value, problem, *, proofs=None, name='hd', function=None, at=None)
Build have name : HasDerivAt (fun var => expr) value point, proved from the composed term.
The step converts the term of has_deriv_at to the stated derivative (Sage's), unfolds the pointwise operations
the term introduced, and closes the algebra by ring or field_simp. name.deriv then rewrites deriv.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
expr
|
object
|
The function's body, an expression in |
required |
var
|
Expression
|
The variable of differentiation; a symbol ending in |
required |
point
|
object
|
The point, an expression over the problem's atoms. |
required |
value
|
object
|
The derivative at the point, as Sage computed it. |
required |
problem
|
Problem
|
The problem whose atoms name the variables. |
required |
proofs
|
Mapping[str, str] | None
|
Tactics proving side conditions no hypothesis states, by their Lean text. |
None
|
name
|
str
|
The name of the fact. |
'hd'
|
function
|
str | None
|
The function's Lean text, stated instead of the rendered body (so it matches a goal's |
None
|
at
|
str | None
|
The point's Lean text, stated instead of the rendered point. |
None
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic block. |
Examples:
>>> from sage.all import exp
>>> from veriphy.toolkit import read_problem
>>> prob = read_problem({'vars': ['x0'], 'atoms': ['a'], 'carrier': 'ℝ', 'goal': {'kind': 'false'}})
>>> t = SR.var('t_')
>>> first, second, closing = str(has_deriv_at_proof(t**2 * exp(t), t, 1, 3 * exp(1), prob)).splitlines()
>>> print(first); print(second)
have hd : HasDerivAt (fun t => ((t ^ 2) * (Real.exp t) : ℝ)) ((3 * (Real.exp 1) : ℝ)) (1 : ℝ) := by
convert (((hasDerivAt_id' (1 : ℝ)).pow 2).mul ((hasDerivAt_id' (1 : ℝ)).exp)) using 1
>>> closing.split(' | (simp only')[0]
' all_goals first | rfl | (funext y; simp only [Pi.mul_apply, Pi.pow_apply]; ring_nf; done)'
Source code in src/veriphy/toolkit/_derivative.py
224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 | |
hexagon_violations(data)
Return the number of hexagon equations (both kinds) the R- and F-symbols fail.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
data
|
Fusion
|
The fusion data. |
required |
Returns:
| Type | Description |
|---|---|
int
|
The count. |
Source code in src/veriphy/toolkit/_fusion.py
216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 | |
hyp(problem, name)
Reference a hypothesis of the problem by name.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
problem
|
Problem
|
The problem. |
required |
name
|
str
|
The hypothesis name. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The reference, a term. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the problem has no hypothesis of that name. |
Examples:
>>> from veriphy.toolkit import read_problem
>>> prob = read_problem({'vars': ['x0'], 'hyps': [{'name': 'h1', 'text': 'True'}], 'goal': {'kind': 'false'}})
>>> str(hyp(prob, 'h1'))
'h1'
Source code in src/veriphy/toolkit/_emit.py
61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 | |
integral_rescaling(table, parities)
Rescale the basis (even elements by μ, odd by λ) so that every structure constant is an integer.
With eᵢ' = sᵢ eᵢ the constants become sᵢ sⱼ / sₖ cᵢⱼₖ: even-even and even-odd ones scale by μ, odd-odd ones
by λ² / μ. Integer constants make the kernel check faster.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
table
|
Table
|
Rational structure constants. |
required |
parities
|
Sequence[int]
|
The basis parities. |
required |
Returns:
| Type | Description |
|---|---|
tuple[Table, tuple[int, int]]
|
The rescaled table and |
Source code in src/veriphy/toolkit/_superalgebra.py
466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 | |
intertwiners(rho, sigma)
Return a basis of the matrices T with T ρ(x) = σ(x) T for every basis element x.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
rho
|
Rep
|
The source representation. |
required |
sigma
|
Rep
|
The target representation. |
required |
Returns:
| Type | Description |
|---|---|
list[Matrix]
|
The intertwiners (empty when the representations share no irreducible summand). |
Source code in src/veriphy/toolkit/_representation.py
172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 | |
intertwining_facts(t, rho, sigma, name=None)
Return facts T * ρ(x) = σ(x) * T for each basis element, and T * T⁻¹ = 1 for an invertible T.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
t
|
Matrix
|
The intertwiner (square). |
required |
rho
|
Rep
|
The source representation. |
required |
sigma
|
Rep
|
The target representation. |
required |
name
|
str | None
|
A Lean name for |
None
|
Returns:
| Type | Description |
|---|---|
Lean
|
The facts |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If |
Source code in src/veriphy/toolkit/_representation.py
326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 | |
invariant_forms(ops, *, symmetric)
Return a basis of the bilinear forms B with Tᵀ B + B T = 0 for every T, symmetric or antisymmetric.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
ops
|
Sequence[Matrix]
|
Matrices acting on one space. |
required |
symmetric
|
bool
|
Whether to look for symmetric (otherwise antisymmetric) forms. |
required |
Returns:
| Type | Description |
|---|---|
list[Matrix]
|
The forms. |
Source code in src/veriphy/toolkit/_superalgebra.py
215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 | |
inverse_certificate()
Return a proof term of A⁻¹ = B for explicit matrices: the kernel checks A * B = 1.
Returns:
| Type | Description |
|---|---|
Lean
|
The term, for |
Examples:
>>> print(inverse_certificate())
VeriphyCheck.inv_eq_of_check (by decide +kernel)
Source code in src/veriphy/toolkit/_lie.py
453 454 455 456 457 458 459 460 461 462 463 | |
ising()
Return the Ising category's fusion data, with F- and R-symbols over ℚ(ζ₁₆).
The labels and rules are SU(2) at level 2 (1, σ, ψ); F^{σσσ}_σ = (1/√2) [[1, 1], [1, -1]] and
F^{σψσ}_ψ = F^{ψσψ}_σ = -1; R^{σσ}_1 = ζ₁₆⁻¹, R^{σσ}_ψ = ζ₁₆³, R^{σψ}_σ = R^{ψσ}_σ = -i, R^{ψψ}_1 = -1.
(SU(2) at level 2 itself has the opposite sign of F^{σσσ}_σ and other R-symbols: a different braided category
with the same fusion rules.)
Returns:
| Type | Description |
|---|---|
Fusion
|
The data. |
Examples:
>>> data = ising()
>>> pentagon_violations(data), hexagon_violations(data)
(0, 0)
Source code in src/veriphy/toolkit/_fusion.py
137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 | |
isolate_roots(p)
Return disjoint rational intervals (a, b), each holding exactly one simple real root of p.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
p
|
Polynomial
|
A polynomial over ℚ. |
required |
Returns:
| Type | Description |
|---|---|
list[tuple[QQ, QQ]]
|
The intervals, with |
Examples:
>>> x = PolynomialRing(QQ, 'x').gen()
>>> isolate_roots(x**3 - 2*x - 1)[-1]
(3/2, 3)
Source code in src/veriphy/toolkit/_numerics.py
164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 | |
jacobi_certificate(table, name='hjacobi')
Return a fact that the bracket the structure constants define satisfies the Jacobi identity.
VeriphyCheck.jacobi_of_check reduces it, by trilinearity, to the Jacobi identity on basis triples, which the
kernel checks. With antisymmetry (VeriphyCheck.bracket_self_of_check) this certifies a Lie algebra.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
table
|
Table
|
Rational structure constants. |
required |
name
|
str
|
The fact's name. |
'hjacobi'
|
Returns:
| Type | Description |
|---|---|
Lean
|
The fact |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If a structure constant is not rational. |
Examples:
>>> fact = str(jacobi_certificate([[[0, 0], [0, 1]], [[0, -1], [0, 0]]]))
>>> fact.startswith('have hjacobi := VeriphyCheck.jacobi_of_check (c := (![![![0, 0], ![0, 1]], ')
True
Source code in src/veriphy/toolkit/_lie.py
295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 | |
jordan_certificate(a)
Return the Jordan form J = P⁻¹ A P of a rational matrix with rational eigenvalues, with facts proving it.
A diagonalizable matrix gets a diagonal J: this is its diagonalization.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
a
|
Matrix
|
A square rational matrix whose eigenvalues are rational. |
required |
Returns:
| Type | Description |
|---|---|
tuple[Matrix, Matrix, Lean]
|
|
Raises:
| Type | Description |
|---|---|
CertificateError
|
If an eigenvalue is not rational (work over a number field instead). |
Examples:
>>> j, p, facts = jordan_certificate(matrix(QQ, [[2, 1], [0, 2]]))
>>> j
[2 1]
[0 2]
Source code in src/veriphy/toolkit/_normal_form.py
50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 | |
killing_form(table)
Return the Killing form's matrix, K[i][j] = tr(ad eᵢ ad eⱼ).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
table
|
Table
|
Structure constants. |
required |
Returns:
| Type | Description |
|---|---|
Matrix
|
The symmetric matrix of the form. |
Examples:
>>> e, f, h = matrix(QQ, [[0, 1], [0, 0]]), matrix(QQ, [[0, 0], [1, 0]]), matrix(QQ, [[1, 0], [0, -1]])
>>> killing_form(structure_constants([e, f, h]))
[0 4 0]
[4 0 0]
[0 0 8]
Source code in src/veriphy/toolkit/_lie.py
87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 | |
killing_proof(*, unfold=())
Return a proof of CoordinateGeometry.IsKilling G X for an explicit metric and vector field.
Every component of the Lie derivative is expanded (simp with derivative lemmas) and closed by ring.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
unfold
|
Sequence[str]
|
Definitions to unfold (the metric's and the field's names). |
()
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Source code in src/veriphy/toolkit/_geometry.py
138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 | |
ladder_combination(coefficients, xi=None, hbar=None)
Return a combination of a, a†, x and p (one coordinate) as coefficients of x and p.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
coefficients
|
dict[str, object]
|
The coefficients of |
required |
xi
|
object
|
The length scale |
None
|
hbar
|
object
|
The reduced Planck constant; the symbol |
None
|
Returns:
| Type | Description |
|---|---|
dict[str, object]
|
The coefficients of |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If a name is not one of |
Examples:
>>> ladder_combination({'a': 1, 'a†': 1})
{'x': sqrt(2)/xi, 'p': 0}
Source code in src/veriphy/toolkit/_operators.py
431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 | |
ladder_commutator_proof(index='i', oscillator='Q')
Return a proof of ⁅A, B⁆ = c • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ) for Physlib's ladder operators.
A and B are combinations of Q.loweringCLM i, Q.raisingCLM i, 𝐱 i and 𝐩 i. The proof unfolds the
ladder operators, expands the bracket by bilinearity with Physlib's commutation lemmas, and closes the scalar
identity by field_simp and ring, with i² = -1 and (√2)² = 2. The goal's file must make the bracket a
Lie ring, as Physlib does: attribute [local instance 100] LieRing.ofAssociativeRing.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
index
|
str
|
The coordinate index of the goal. |
'i'
|
oscillator
|
str
|
The |
'Q'
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Source code in src/veriphy/toolkit/_operators.py
461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 | |
ladder_matrices(levels)
Return the annihilation and creation operators truncated to levels states, over Sage's symbolic ring.
a |n⟩ = √n |n - 1⟩; on the truncated space [a, a†] = 1 - levels · |levels - 1⟩⟨levels - 1|.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
levels
|
int
|
The number of states. |
required |
Returns:
| Type | Description |
|---|---|
tuple[Matrix, Matrix]
|
|
Examples:
>>> a, ad = ladder_matrices(3)
>>> (a * ad - ad * a).diagonal()
[1, 1, -2]
Source code in src/veriphy/toolkit/_operators.py
324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 | |
ladder_operators(xi=None, hbar=None)
Return the lowering and raising operators as combinations of one coordinate's position and momentum.
a = (x/ξ + i ξ p/ℏ)/√2 and a† = (x/ξ - i ξ p/ℏ)/√2, Physlib's convention for the harmonic oscillator.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
xi
|
object
|
The length scale |
None
|
hbar
|
object
|
The reduced Planck constant; the symbol |
None
|
Returns:
| Type | Description |
|---|---|
tuple[dict[str, object], dict[str, object]]
|
The coefficients of |
Examples:
>>> lowering, raising = ladder_operators()
>>> lowering['p']
1/2*I*sqrt(2)*xi/hbar
Source code in src/veriphy/toolkit/_operators.py
380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 | |
lemma_rewrite(lemma, problem, *, reverse=False, side=(), proofs=None, at=None)
Rewrite with a named mathlib lemma, passing its side conditions as arguments.
Each side condition is the Lean text of a proposition. It is passed as the hypothesis or domain fact that states
it, or as (by <proof>) from proofs.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
lemma
|
str
|
The lemma name, such as |
required |
problem
|
Problem
|
The problem. |
required |
reverse
|
bool
|
Rewrite right to left ( |
False
|
side
|
Sequence[str]
|
The lemma's side conditions, in argument order. |
()
|
proofs
|
Mapping[str, Lean | str] | None
|
A tactic proving a side condition no hypothesis states, by its text. |
None
|
at
|
str | None
|
A hypothesis to rewrite instead of the goal. |
None
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If a side condition is neither stated nor supplied, naming it. |
Examples:
>>> from veriphy.toolkit import read_problem
>>> prob = read_problem({'vars': ['x0'], 'atoms': ['u'], 'goal': {'kind': 'false'},
... 'hyps': [{'name': 'hu', 'poly': '-x0', 'rel': 'le', 'text': '0 ≤ u'}]})
>>> str(lemma_rewrite('Real.exp_add', prob, reverse=True))
'rw [← Real.exp_add]'
>>> str(lemma_rewrite('Real.sqrt_mul_self', prob, side=['0 ≤ u'], at='h'))
'rw [Real.sqrt_mul_self hu] at h'
>>> lemma_rewrite('Real.log_exp', prob, side=['0 < u'])
Traceback (most recent call last):
...
veriphy.core._errors.CertificateError: side condition '0 < u' of Real.log_exp is not stated; pass its proof
Source code in src/veriphy/toolkit/_symbolic_emit.py
418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 | |
lift(x)
Return the representative of a number-field element as a polynomial over ℚ in x.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
x
|
NumberFieldElement | int
|
An element of a number field with one generator, or a rational. |
required |
Returns:
| Type | Description |
|---|---|
Polynomial
|
The polynomial of degree below the field's degree. |
Examples:
>>> from sage.all import QuadraticField
>>> lift(QuadraticField(2, 's').gen() / 2 + 1)
1/2*x + 1
Source code in src/veriphy/toolkit/_number_field.py
176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 | |
linear_combination(weighted, problem)
Close an equality or inequality goal by linear_combination of weighted proofs.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
weighted
|
Sequence[tuple[object, Lean]]
|
Pairs of a weight and a proof term, as for |
required |
problem
|
Problem
|
The problem. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Examples:
>>> from veriphy.toolkit import read_problem
>>> prob = read_problem({'vars': ['x0'], 'atoms': ['a'], 'goal': {'kind': 'false'}})
>>> str(linear_combination([('x0 + 3', term('h')), (-2, term("h'"))], prob))
"linear_combination (a + 3) * h + (-2) * h'"
Source code in src/veriphy/toolkit/_emit.py
119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 | |
load_core_table()
cached
Return the core (mathlib) table shipped with the toolkit.
Returns:
| Type | Description |
|---|---|
Table
|
The core table. |
Examples:
>>> core = load_core_table()
>>> core.namespace, [f.lean for f in core.functions if f.sage == 'exp']
('mathlib', ['Real.exp', 'Complex.exp'])
Source code in src/veriphy/toolkit/_table.py
284 285 286 287 288 289 290 291 292 293 294 295 296 297 | |
load_pack(name)
cached
Return a library pack shipped with the toolkit, by its namespace.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
name
|
str
|
The pack's namespace, such as |
required |
Returns:
| Type | Description |
|---|---|
Table
|
The pack's table. |
Raises:
| Type | Description |
|---|---|
TableError
|
If no pack has that name. |
Examples:
>>> physlib = load_pack('physlib')
>>> [f.lean for f in physlib.functions], dict(physlib.conventions)['metric_signature']
(['Time.deriv', 'Space.deriv'], '+---')
Source code in src/veriphy/toolkit/_table.py
300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 | |
matrix_goal_proof(kind, size, carrier, entrywise_limit=ENTRYWISE_LIMIT)
Return a proof of a matrix goal stated with explicit matrices: entrywise when small, by a checker when large.
The checker reads the goal's own matrices, so it needs no data from the script. Kernel evaluation needs decidable equality of entries, so goals over ℝ or ℂ always get the entrywise proof.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
kind
|
str
|
The goal's shape: |
required |
size
|
int
|
The matrices' dimension. |
required |
carrier
|
str
|
The type of the entries. |
required |
entrywise_limit
|
int
|
The largest dimension proved entry by entry. |
ENTRYWISE_LIMIT
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the kind is unknown. |
Examples:
>>> print(matrix_goal_proof('mul', 2, 'ℚ'))
ext i j
fin_cases i <;> fin_cases j <;> norm_num
>>> print(matrix_goal_proof('commute', 12, 'ℤ'))
exact VeriphyCheck.commute_of_check (by decide +kernel)
>>> print(matrix_goal_proof('commute', 12, 'ℝ'))
ext i j
fin_cases i <;> fin_cases j <;> norm_num
Source code in src/veriphy/toolkit/_reflect.py
26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 | |
matrix_identity_proof()
Return the entrywise proof of an identity between explicit matrices over ℝ or ℂ (√k, Complex.I entries).
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Source code in src/veriphy/toolkit/_operators.py
371 372 373 374 375 376 377 | |
matrix_term(m, problem, index=None)
Render a Sage matrix as a Lean !![…] literal over the problem's atoms, or by blocks for a sum index.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
m
|
Matrix
|
A Sage matrix with entries Sage's symbolic ring converts. |
required |
problem
|
Problem
|
The problem whose atoms name the variables. |
required |
index
|
MatrixIndex | None
|
The index type of a matrix indexed by |
None
|
Returns:
| Type | Description |
|---|---|
Lean
|
The term. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the matrix's size does not match the index type. |
Examples:
>>> from veriphy.toolkit import read_problem
>>> from sage.all import matrix
>>> prob = read_problem({'vars': ['x0'], 'atoms': ['c'], 'goal': {'kind': 'false'}})
>>> str(matrix_term(matrix(SR, [[1, prob.symbols['x0']], [0, 1/2]]), prob))
'!![1, c; 0, 1 / 2]'
>>> sum_index = MatrixIndex((1, 2), (1, 2), 'Matrix (Fin 1 ⊕ Fin 2) (Fin 1 ⊕ Fin 2) ℚ')
>>> str(matrix_term(matrix(SR, [[1, 0, 0], [0, -1, 0], [0, 0, -1]]), prob, sum_index))
'(Matrix.fromBlocks !![1] !![0, 0] !![0; 0] !![-1, 0; 0, -1] : Matrix (Fin 1 ⊕ Fin 2) (Fin 1 ⊕ Fin 2) ℚ)'
Source code in src/veriphy/toolkit/_symbolic_emit.py
298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 | |
metric_term(g)
Return a metric's components as a Lean Fin n → Fin n → (Fin n → ℝ) → ℝ.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
g
|
Matrix
|
The metric's matrix of expressions in the coordinates. |
required |
Returns:
| Type | Description |
|---|---|
str
|
The term. |
Examples:
>>> from sage.all import sin
>>> x0, x1 = coordinates(2)
>>> term = metric_term(matrix(SR, [[1, 0], [0, sin(x0)**2]]))
>>> 'fun x => ((Real.sin (x 0)) ^ 2 : ℝ)' in term, term.endswith(': Fin 2 → Fin 2 → (Fin 2 → ℝ) → ℝ)')
(True, True)
Source code in src/veriphy/toolkit/_geometry.py
51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 | |
moment_coefficients(even_ops, factors, omega)
Return a basis of the coefficients kₛ for which the moment-map bracket satisfies super-Jacobi on V.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
even_ops
|
Sequence[Matrix]
|
A basis of |
required |
factors
|
Sequence[int]
|
The simple factor of each basis element. |
required |
omega
|
Matrix
|
An invariant antisymmetric form on |
required |
Returns:
| Type | Description |
|---|---|
list[list[RingElement]]
|
The solutions (one for |
Source code in src/veriphy/toolkit/_superalgebra.py
282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 | |
mul_nonneg(left, right)
Build the proof term mul_nonneg left right from two nonnegativity proofs.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
left
|
Lean
|
A proof of |
required |
right
|
Lean
|
A proof of |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
A proof of |
Examples:
>>> str(mul_nonneg(term('ha'), term('sq_nonneg b')))
'mul_nonneg ha (sq_nonneg b)'
Source code in src/veriphy/toolkit/_emit.py
157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 | |
mul_pos(left, right)
Build the proof term mul_pos left right from two positivity proofs.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
left
|
Lean
|
A proof of |
required |
right
|
Lean
|
A proof of |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
A proof of |
Examples:
>>> str(mul_pos(term('ha'), term('hb')))
'mul_pos ha hb'
Source code in src/veriphy/toolkit/_emit.py
174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 | |
natural_iso_facts(t, name=None)
Return facts T * U = 1 and U * T = 1 for an invertible natural transformation and its inverse U.
With the naturality fact they give VeriphyCheck.repIso, a natural isomorphism.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
t
|
Matrix
|
The transformation (square, invertible, rational). |
required |
name
|
str | None
|
A Lean name for |
None
|
Returns:
| Type | Description |
|---|---|
Lean
|
The facts |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If |
Source code in src/veriphy/toolkit/_representation.py
413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 | |
naturality_proof(t, rho_generators, sigma_generators, *, rho, sigma, closure)
Return a proof of ∀ g, T * ρ g = σ g * T: naturality between two group representations as functors.
A representation of G is a functor from its one-object category, and T is natural when every square
T ρ(g) = σ(g) T commutes. Sage checks the squares for the generators; the kernel checks each again
(decide +kernel, unfolding ρ and σ at the generator), and VeriphyCheck.intertwines_of_closure extends them
to the whole group from the goal's closure fact. VeriphyCheck.repHom (or repIso, given natural_iso_facts)
packages the result as a morphism of Rep.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
t
|
Matrix
|
The candidate natural transformation. |
required |
rho_generators
|
Sequence[Matrix]
|
|
required |
sigma_generators
|
Sequence[Matrix]
|
|
required |
rho
|
str
|
The Lean name of |
required |
sigma
|
str
|
The Lean name of |
required |
closure
|
str
|
The name of the hypothesis |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If a square fails, naming the generator. |
Examples:
>>> swap = matrix(QQ, [[0, 1, 0], [1, 0, 0], [0, 0, 1]])
>>> cycle = matrix(QQ, [[0, 0, 1], [1, 0, 0], [0, 1, 0]])
>>> one = identity_matrix(QQ, 1)
>>> print(naturality_proof(matrix(QQ, [[1, 1, 1]]), [cycle, swap], [one, one], rho='perm', sigma='triv',
... closure='hS'))
refine VeriphyCheck.intertwines_of_closure perm triv _ hS ?_
rintro s (rfl | rfl)
· decide +kernel
· decide +kernel
Source code in src/veriphy/toolkit/_representation.py
357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 | |
negate_goal(name)
Turn a ≤/< goal into False with its negation as hypothesis name.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
name
|
str
|
The name of the negated goal (use |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic block. |
Examples:
>>> print(negate_goal('hneg'))
by_contra hneg
push Not at hneg
Source code in src/veriphy/toolkit/_emit.py
396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 | |
nilpotency_index(n)
Return the least k with Nᵏ = 0, or None when N is not nilpotent.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
n
|
Matrix
|
A square matrix. |
required |
Returns:
| Type | Description |
|---|---|
int | None
|
The index. |
Examples:
>>> nilpotency_index(matrix(QQ, [[0, 1, 2], [0, 0, 3], [0, 0, 0]]))
3
Source code in src/veriphy/toolkit/_exponential.py
35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 | |
nilpotent_exponential(n)
Return exp N for a nilpotent rational matrix, and a proof of exp N = E for the goal's N and E.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
n
|
Matrix
|
The nilpotent matrix. |
required |
Returns:
| Type | Description |
|---|---|
tuple[Matrix, Lean]
|
|
Raises:
| Type | Description |
|---|---|
CertificateError
|
If |
Examples:
>>> e, proof = nilpotent_exponential(matrix(QQ, [[0, 1, 2], [0, 0, 3], [0, 0, 0]]))
>>> e
[ 1 1 7/2]
[ 0 1 3]
[ 0 0 1]
Source code in src/veriphy/toolkit/_exponential.py
56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 | |
nlinarith(hints=())
Call nlinarith with hint terms (products and squares that Sage found).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
hints
|
Sequence[Lean]
|
Proof terms added to |
()
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Examples:
>>> str(nlinarith([term('sq_nonneg (a - b)'), term('mul_pos ha hb')]))
'nlinarith [sq_nonneg (a - b), mul_pos ha hb]'
Source code in src/veriphy/toolkit/_emit.py
197 198 199 200 201 202 203 204 205 206 207 208 209 210 | |
norm_num(lemmas=(), at=None)
Call norm_num, optionally with extra simp lemmas and at a hypothesis.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
lemmas
|
Sequence[str]
|
Lemma or hypothesis names. |
()
|
at
|
str | None
|
A hypothesis to normalize instead of the goal. |
None
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Examples:
>>> str(norm_num()), str(norm_num(at='hk'))
('norm_num', 'norm_num at hk')
Source code in src/veriphy/toolkit/_emit.py
242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 | |
nullstellensatz_proof(problem)
Refute a system of polynomial equalities with no common zero: 1 = Σ gᵢ fᵢ, from a Gröbner lift.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
problem
|
Problem
|
The problem; its goal is |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If 1 is not in the ideal of the equalities (they have a common zero over ℂ). |
Examples:
>>> from veriphy.toolkit import read_problem
>>> prob = read_problem({'vars': ['x0', 'x1'], 'atoms': ['x', 'y'], 'carrier': 'ℚ', 'goal': {'kind': 'false'},
... 'hyps': [{'name': 'hxy', 'rel': 'eq', 'poly': '(x0 * x1) - (1)', 'text': 'x * y = 1'},
... {'name': 'hx', 'rel': 'eq', 'poly': '(x0) - (0)', 'text': 'x = 0'}]})
>>> print(nullstellensatz_proof(prob))
have h1 : (1 : ℚ) = 0 := by linear_combination (-1) * hxy + (y) * hx
exact one_ne_zero h1
Source code in src/veriphy/toolkit/_algebraic.py
45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 | |
operator_identity(lhs, rhs, coordinates, *, psi='ψ', smooth='hψ', point='x', name='hop')
Return a fact (lhs ψ) x = (rhs ψ) x, checked first in Sage on a symbolic ψ, then proved in Lean.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
lhs
|
Operator
|
The left operator. |
required |
rhs
|
Operator
|
The right operator. |
required |
coordinates
|
Coordinates
|
The coordinates. |
required |
psi
|
str
|
The Lean name of the test function. |
'ψ'
|
smooth
|
str
|
The Lean name of the hypothesis |
'hψ'
|
point
|
str
|
The Lean name of the point. |
'x'
|
name
|
str
|
The fact's name. |
'hop'
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the identity fails in Sage (the difference is shown). |
Examples:
>>> c = Coordinates(1)
>>> d, x = c.partial(0), c.multiplication(c.symbols[0])
>>> print(operator_identity(commutator(d, x), c.scalar(1), c).text.splitlines()[0])
have hd0 : Differentiable ℝ (ψ) := (hψ.iterate_deriv' 1 0).differentiable (by norm_num)
Source code in src/veriphy/toolkit/_operators.py
181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 | |
operator_relations(matrices, names, pairs=None)
Return facts Xᵢ * Xⱼ - Xⱼ * Xᵢ = Σ cₖ • Xₖ for matrices over ℚ(i), proved entrywise over ℂ.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
matrices
|
Sequence[Matrix]
|
The matrices (Pauli, spin, gamma matrices), with entries in ℚ(i). |
required |
names
|
Sequence[str]
|
Their Lean names (definitions over ℂ, unfolded by the proof). |
required |
pairs
|
Sequence[tuple[int, int]] | None
|
The pairs to state; every |
None
|
Returns:
| Type | Description |
|---|---|
Lean
|
The facts |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If a commutator is not in the span of the matrices. |
Source code in src/veriphy/toolkit/_operators.py
288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 | |
packed_product_certificate(a, b, c)
Return a proof term of A * B = C for large integer matrices, with their rows packed in the certificate.
The goal's matrices should be definitions (or literals) equal by unfolding to the packed ones; the kernel checks
the product on lists, at n³ integer operations.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
a
|
Matrix
|
The left factor, an integer matrix. |
required |
b
|
Matrix
|
The right factor. |
required |
c
|
Matrix
|
The claimed product. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The proof term. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the matrices are not square integer matrices of one size, or |
Examples:
>>> from sage.all import matrix
>>> a, b = matrix(ZZ, [[1, 2], [3, 4]]), matrix(ZZ, [[0, 1], [1, 0]])
>>> print(packed_product_certificate(a, b, a * b))
VeriphyCheck.ofLists_mul (n := 2) (rows₁ := VeriphyCheck.unpackRows 4 4 2 [101, 135])
(rows₂ := VeriphyCheck.unpackRows 4 4 2 [84, 69]) (prod := VeriphyCheck.unpackRows 4 4 2 [86, 120])
(by decide +kernel) (by decide +kernel)
Source code in src/veriphy/toolkit/_reflect.py
75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 | |
parameter_context(name='α')
Return ℚ(α) for a transcendental parameter α: identities are identities of rational functions.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
name
|
str
|
The parameter's Lean text. |
'α'
|
Returns:
| Type | Description |
|---|---|
FieldContext
|
The context; denominators need |
Source code in src/veriphy/toolkit/_number_field.py
164 165 166 167 168 169 170 171 172 173 | |
parenthesize(text)
Return Lean text wrapped in parentheses unless it is a single identifier or numeral.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
text
|
str
|
The Lean source. |
required |
Returns:
| Type | Description |
|---|---|
str
|
The text, safe to use as an operand. |
Examples:
>>> parenthesize('f a'), parenthesize('v₁'), parenthesize('↑n')
('(f a)', 'v₁', '(↑n)')
Source code in src/veriphy/toolkit/_lean.py
75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 | |
parity_of(m, even_dim)
Return the parity of a homogeneous supermatrix: 0 when block diagonal, 1 when block off-diagonal.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
m
|
Matrix
|
The supermatrix. |
required |
even_dim
|
int
|
The dimension of the even part. |
required |
Returns:
| Type | Description |
|---|---|
int
|
The parity. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the matrix is not homogeneous. |
Source code in src/veriphy/toolkit/_superalgebra.py
64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 | |
parse_polynomial(ring, s, *, param)
Parse a polynomial string in ring.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
ring
|
MPolynomialRing_base
|
The polynomial ring. |
required |
s
|
object
|
The polynomial, written in Sage syntax. |
required |
param
|
str
|
The request parameter the string came from, named in errors. |
required |
Returns:
| Type | Description |
|---|---|
MPolynomial
|
The polynomial. |
Raises:
| Type | Description |
|---|---|
ParamError
|
If |
Examples:
>>> parse_polynomial(create_ring(['x0']), 'x0^2 - 1/2', param='poly')
x0^2 - 1/2
Source code in src/veriphy/toolkit/_problem.py
81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 | |
parse_symbolic(text, symbols, typed=None)
Parse a symbolic expression serialized by Lean's symbolic translation, or return None when it does not parse.
typed(e, 'ℕ') markers (a sub-expression computed at another Lean type) evaluate to e, and are recorded in
typed when a list is given.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
text
|
object
|
The expression in Sage syntax, over the variables in |
required |
symbols
|
dict[str, Expression]
|
The symbolic variables by name. |
required |
typed
|
list[tuple[Expression, str]] | None
|
Where to record the marked sub-expressions with their Lean type. |
None
|
Returns:
| Type | Description |
|---|---|
Expression | Matrix | None
|
The expression in Sage's symbolic ring (a matrix over it for a matrix-valued expression), or |
Examples:
>>> x0 = SR.var('x0')
>>> parse_symbolic('(sqrt(x0) + log(x0))', {'x0': x0})
sqrt(x0) + log(x0)
>>> parse_symbolic('sum((k_)^(2), k_, 0, x0 - 1)', {'x0': x0})
1/3*x0^3 - 1/2*x0^2 + 1/6*x0
>>> parse_symbolic('mod(x0, 3)', {'x0': x0})
mod(x0, 3)
>>> parse_symbolic('(matrix(SR, [[1, x0]])) - (matrix(SR, [[1, 0]]))', {'x0': x0})
[ 0 x0]
>>> marked = []
>>> parse_symbolic("typed(mod(x0, 7), 'ℕ') + gcd(x0, 6) + gcd(4, 6)", {'x0': x0}, marked)
gcd(x0, 6) + mod(x0, 7) + 2
>>> marked
[(mod(x0, 7), 'ℕ')]
Source code in src/veriphy/toolkit/_problem.py
121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 | |
parse_table(data, source, default_namespace=None)
Validate a table read from JSON against the schema and return it.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
data
|
object
|
The parsed JSON. |
required |
source
|
str
|
Where it came from (a file name), named in errors. |
required |
default_namespace
|
str | None
|
The namespace of a table that names none ( |
None
|
Returns:
| Type | Description |
|---|---|
Table
|
The table. |
Raises:
| Type | Description |
|---|---|
TableError
|
If a field is missing or of the wrong kind, naming the source and the field. |
Examples:
>>> parse_table({'namespace': 'project', 'functions': [{'lean': 'Real.cosh', 'arity': 1}]}, 'cosh.json')
Traceback (most recent call last):
...
veriphy.core._errors.TableError: cosh.json: missing field 'sage'
>>> table = parse_table({'namespace': 'project',
... 'functions': [{'lean': 'Real.cosh', 'sage': 'cosh', 'arity': 1, 'types': ['ℝ']}]}, 'cosh.json')
>>> table.functions[0].sage, table.functions[0].types
('cosh', ('ℝ',))
Source code in src/veriphy/toolkit/_table.py
248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 | |
pentagon_violations(data)
Return the number of pentagon equations the F-symbols fail.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
data
|
Fusion
|
The fusion data. |
required |
Returns:
| Type | Description |
|---|---|
int
|
The count. |
Source code in src/veriphy/toolkit/_fusion.py
204 205 206 207 208 209 210 211 212 213 | |
polynomial(p, problem)
Render a polynomial of the problem's ring as a Lean term over the atoms' text.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
p
|
object
|
A polynomial in |
required |
problem
|
Problem
|
The problem whose atoms name the variables. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The term, |
Examples:
>>> from veriphy.toolkit import read_problem
>>> prob = read_problem({'vars': ['x0', 'x1'], 'atoms': ['f a', 'b'], 'goal': {'kind': 'false'}})
>>> str(polynomial('2*x0^2 - x0*x1/3', prob))
'2 * (f a) ^ 2 - 1 / 3 * (f a) * b'
Source code in src/veriphy/toolkit/_lean.py
125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 | |
positive_roots(cartan_type)
Return the positive roots as their coefficients on the simple roots, in Sage's labeling.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
cartan_type
|
str
|
The type, as |
required |
Returns:
| Type | Description |
|---|---|
list[list[int]]
|
One coefficient list per root. |
Examples:
>>> sorted(positive_roots('G2'))
[[0, 1], [1, 0], [1, 1], [2, 1], [3, 1], [3, 2]]
Source code in src/veriphy/toolkit/_lie.py
375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 | |
positivity()
Call positivity.
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Examples:
>>> str(positivity())
'positivity'
Source code in src/veriphy/toolkit/_emit.py
213 214 215 216 217 218 219 220 221 222 223 | |
positivstellensatz_proof(problem, squares=None, multiplier_degree=1)
Refute a real semialgebraic system: κ = Σ wₖ Pₖ + Σ hⱼ fⱼ with every Pₖ ≤ 0 and κ > 0.
The facts Pₖ are the inequality hypotheses, their pairwise products and the given squares (by default squares of
variables and of their sums and differences); the multipliers hⱼ of the equalities are polynomials. An exact LP
finds the weights; linear_combination checks the identity.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
problem
|
Problem
|
The problem; its goal is |
required |
squares
|
Sequence[MPolynomial] | None
|
Polynomials whose squares may enter the certificate. |
None
|
multiplier_degree
|
int
|
The degree of the equality multipliers. |
1
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If no certificate of this degree exists. |
Source code in src/veriphy/toolkit/_algebraic.py
124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 | |
prime_certificate(p)
Return a proof term of Nat.Prime p from a Pratt certificate the kernel checks.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
p
|
object
|
A prime number. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The proof term. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If |
Examples:
>>> print(prime_certificate(7))
VeriphyCheck.prime_of_pratt (cert := [(3, 2, [(2, 1)]), (7, 3, [(2, 1), (3, 1)])]) (by decide +kernel)
Source code in src/veriphy/toolkit/_reflect.py
129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 | |
primitive(omega)
Return a function f with df = ω for a closed 1-form on ℝⁿ, by integrating along the coordinate axes.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
omega
|
Sequence[object]
|
The components |
required |
Returns:
| Type | Description |
|---|---|
object
|
The primitive. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the form is not closed ( |
Examples:
>>> x0, x1, x2 = coordinates(3)
>>> primitive([2 * x0 * x1, x0**2, 2 * x2])
x0^2*x1 + x2^2
Source code in src/veriphy/toolkit/_geometry.py
158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 | |
projector_facts(projectors, rho)
Return facts that the matrices are projectors onto summands of the representation.
Each Pₖ is idempotent (hp_k), distinct ones are orthogonal (ho_k_l), they sum to the identity (hsum),
and each commutes with every representation matrix (hc_k_i).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
projectors
|
Sequence[Matrix]
|
The projectors. |
required |
rho
|
Rep
|
The representation's matrices. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The facts. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If a claimed identity fails in Sage. |
Source code in src/veriphy/toolkit/_representation.py
278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 | |
quadratic_context(d, name='hs')
Return ℚ(√d) inside ℝ: the generator Real.sqrt d, with Real.sqrt d ^ 2 = d from Real.sq_sqrt.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
d
|
int
|
A positive integer that is not a square. |
required |
name
|
str
|
The fact's name. |
'hs'
|
Returns:
| Type | Description |
|---|---|
FieldContext
|
The context. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If |
Examples:
>>> print(quadratic_context(2).setup)
have hs : Real.sqrt 2 ^ 2 = 2 := Real.sq_sqrt (by norm_num)
Source code in src/veriphy/toolkit/_number_field.py
89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 | |
radical_proof(problem, max_power=8)
Prove p = 0 (the goal lhs = rhs) from equalities whose ideal contains a power pᵏ.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
problem
|
Problem
|
The problem; its goal is a polynomial equality over a ring without zero divisors. |
required |
max_power
|
int
|
The largest power tried. |
8
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic: |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If no power up to |
Source code in src/veriphy/toolkit/_algebraic.py
77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 | |
rational(q)
Render an exact rational as a Lean numeral term.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
q
|
object
|
Anything Sage converts exactly to a rational. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
|
Examples:
>>> [str(rational(x)) for x in (3, -3, QQ(3) / 2, QQ(-3) / 2)]
['3', '-3', '3 / 2', '-(3 / 2)']
Source code in src/veriphy/toolkit/_lean.py
93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 | |
rational_matrix_term(m, carrier='ℚ')
Return a typed !![…] literal of a rational matrix.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
m
|
Matrix
|
A matrix with rational entries. |
required |
carrier
|
str
|
The Lean type of the entries. |
'ℚ'
|
Returns:
| Type | Description |
|---|---|
str
|
The Lean text. |
Examples:
>>> rational_matrix_term(matrix(QQ, [[1, 1/2], [0, -1]]))
'(!![1, 1 / 2; 0, -1] : Matrix (Fin 2) (Fin 2) ℚ)'
Source code in src/veriphy/toolkit/_lie.py
393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 | |
rcases(target, names, branches)
Split a disjunction proof into branches, naming the hypothesis of each.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
target
|
Lean
|
A proof of a disjunction |
required |
names
|
Sequence[str]
|
One hypothesis name per disjunct. |
required |
branches
|
Sequence[Lean]
|
One tactic block per disjunct. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Raises:
| Type | Description |
|---|---|
VeriphyError
|
If the numbers of names and branches differ. |
Examples:
>>> print(rcases(term('le_or_lt x 0'), ['hx', 'hx'], [tactic('nlinarith'), tactic('positivity')]))
rcases le_or_lt x 0 with hx | hx
· nlinarith
· positivity
Source code in src/veriphy/toolkit/_emit.py
350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 | |
read_problem(problem)
Bind a serialized Lean problem to Sage objects.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
problem
|
object
|
The problem as |
required |
Returns:
| Type | Description |
|---|---|
Problem
|
The bound problem. |
Raises:
| Type | Description |
|---|---|
ParamError
|
If the serialization is malformed. |
Examples:
>>> bound = read_problem({'vars': ['x0'], 'atoms': ['x'],
... 'hyps': [{'name': 'h', 'poly': 'x0 - 1', 'rel': 'le', 'text': 'x ≤ 1'},
... {'name': 'hs', 'text': 'Real.sin x ≤ 1'}],
... 'goal': {'kind': 'other', 'text': 'Real.cos x ≤ 1'}})
>>> [(h.name, h.poly, h.rel) for h in bound.hyps]
[('h', x0 - 1, 'le'), ('hs', None, None)]
>>> bound.goal.text
'Real.cos x ≤ 1'
Source code in src/veriphy/toolkit/_problem.py
540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 | |
real_matrix_term(m)
Return a matrix with entries q √k as a Lean literal over ℝ.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
m
|
Matrix
|
The matrix (rationals times square roots of integers). |
required |
Returns:
| Type | Description |
|---|---|
str
|
The literal. |
Source code in src/veriphy/toolkit/_operators.py
346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 | |
recurrence_proof(order, recurrence, initial)
Return a proof of a goal a n = f n by strong induction, from a recurrence of order d and d initial values.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
order
|
int
|
The recurrence's order |
required |
recurrence
|
str
|
The name of the hypothesis |
required |
initial
|
Sequence[str]
|
The names of the hypotheses |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the number of initial conditions is not the order. |
Examples:
>>> print(recurrence_proof(2, 'hrec', ['h0', 'h1']))
induction n using Nat.strong_induction_on with
| _ n ih =>
match n with
| 0 => rw [h0]; norm_num
| 1 => rw [h1]; norm_num
| m + 2 => rw [hrec, ih m (by omega), ih (m + 1) (by omega)]; ring
Source code in src/veriphy/toolkit/_summation.py
228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 | |
refute(kappa, *, strict, weighted, problem)
Close False from a combination of hypotheses that reduces to the contradictory constant κ.
The combination proves κ ≤ 0 (or κ < 0 when strict), which norm_num refutes.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
kappa
|
object
|
The constant the combination reduces to, positive (or zero when |
required |
strict
|
bool
|
Whether the combination uses a strict hypothesis. |
required |
weighted
|
Sequence[tuple[object, Lean]]
|
Pairs of a weight and a hypothesis proof, as for |
required |
problem
|
Problem
|
The problem, which must name its carrier type. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic block. |
Raises:
| Type | Description |
|---|---|
VeriphyError
|
If the problem does not name its carrier type. |
Examples:
>>> from veriphy.toolkit import read_problem
>>> prob = read_problem({'vars': ['x0'], 'carrier': 'ℚ', 'goal': {'kind': 'false'}})
>>> print(refute(2, strict=False, weighted=[(1, term('h1')), (-1, term('h2'))], problem=prob))
have hκ : (2 : ℚ) ≤ 0 := by linear_combination h1 + (-1) * h2
norm_num at hκ
Source code in src/veriphy/toolkit/_emit.py
413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 | |
render_element(x, context)
Return a field element as Lean text in the context's generator (a rational function for a parameter).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
x
|
NumberFieldElement | FractionFieldElement | int
|
An element of the field (a rational function in the parameter for ℚ(α)). |
required |
context
|
FieldContext
|
The field's context. |
required |
Returns:
| Type | Description |
|---|---|
str
|
The text. |
Examples:
>>> from sage.all import QuadraticField
>>> render_element(QuadraticField(2, 's').gen() / 2, quadratic_context(2))
'(1 / 2) * (Real.sqrt 2)'
Source code in src/veriphy/toolkit/_number_field.py
195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 | |
render_polynomial(p, generator)
Return a polynomial over ℚ in x as Lean text in the generator, highest degree first.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
p
|
Polynomial
|
The polynomial. |
required |
generator
|
str
|
The generator's Lean text. |
required |
Returns:
| Type | Description |
|---|---|
str
|
The text, |
Examples:
>>> render_polynomial(X**4 + X**3 - X / 2 + 1, 'ζ')
'ζ ^ 4 + ζ ^ 3 - (1 / 2) * ζ + 1'
>>> render_polynomial(-X, 'Real.sqrt 2')
'-(Real.sqrt 2)'
Source code in src/veriphy/toolkit/_number_field.py
56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 | |
representation_relations(rho, table, names=None, pairs=None)
Return facts ⁅ρ(eᵢ), ρ(eⱼ)⁆ = Σ cᵢⱼₖ • ρ(eₖ): the matrices satisfy the algebra's bracket relations.
Sage checks each relation first; the kernel checks it again (VeriphyCheck.bracket_eq_of_check).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
rho
|
Rep
|
The representation's matrices, on the algebra's basis. |
required |
table
|
Table
|
The algebra's structure constants on that basis. |
required |
names
|
Sequence[str] | None
|
Lean names for the matrices; literals when |
None
|
pairs
|
Sequence[tuple[int, int]] | None
|
The pairs to state; every |
None
|
Returns:
| Type | Description |
|---|---|
Lean
|
The facts, |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If a relation fails in Sage, naming it. |
Source code in src/veriphy/toolkit/_representation.py
240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 | |
require_domain(problem, kinds=DOMAIN_KINDS, proofs=None)
Discharge the problem's domain conditions of the given kinds, by hypothesis or by a supplied proof.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
problem
|
Problem
|
The problem. |
required |
kinds
|
Sequence[str]
|
The condition kinds required ( |
DOMAIN_KINDS
|
proofs
|
Mapping[str, Lean | str] | None
|
A tactic proving a condition, by the condition's text, for conditions no hypothesis discharges. |
None
|
Returns:
| Type | Description |
|---|---|
tuple[list[str], list[Lean]]
|
The names of facts stating the conditions, and the |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If a required condition is neither discharged nor supplied, naming each one. |
Examples:
>>> from veriphy.toolkit import read_problem
>>> prob = read_problem({'vars': ['x0'], 'atoms': ['x'], 'goal': {'kind': 'false'},
... 'domain': [{'expr': 'x0', 'kind': 'pos', 'text': '0 < x'}]})
>>> require_domain(prob)
Traceback (most recent call last):
...
veriphy.core._errors.CertificateError: undischarged domain conditions: 0 < x (pass their proofs)
>>> names, haves = require_domain(prob, proofs={'0 < x': 'positivity'})
>>> names, [str(h) for h in haves]
(['hd'], ['have hd : 0 < x := by positivity'])
Source code in src/veriphy/toolkit/_symbolic_emit.py
341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 | |
restrict(rho, basis)
Return the matrices of the representation on an invariant subspace, in the given basis (columns).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
rho
|
Rep
|
The representation. |
required |
basis
|
Matrix
|
Columns spanning an invariant subspace. |
required |
Returns:
| Type | Description |
|---|---|
Rep
|
The restricted matrices. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the subspace is not invariant. |
Source code in src/veriphy/toolkit/_representation.py
149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 | |
rewrite_by(lhs, rhs, justification, problem)
Rewrite lhs into rhs, justified by a tactic: rw [show lhs = rhs by tac].
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
lhs
|
object
|
The expression to rewrite, a Lean term or a polynomial of the problem. |
required |
rhs
|
object
|
Its replacement. |
required |
justification
|
Lean
|
A tactic proving |
required |
problem
|
Problem
|
The problem. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Examples:
>>> from veriphy.toolkit import read_problem
>>> prob = read_problem({'vars': ['x0'], 'atoms': ['x'], 'goal': {'kind': 'false'}})
>>> str(rewrite_by('x0^2 - 1', term('(x - 1) * (x + 1)'), tactic('ring1'), prob))
'rw [show x ^ 2 - 1 = (x - 1) * (x + 1) by ring1]'
Source code in src/veriphy/toolkit/_emit.py
272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 | |
rewrite_candidates(problem)
Return the rewrites the problem's tables (core, packs, project) offer for its goal, in table order.
An entry applies when the goal mentions every function it names, and, when it has a pattern, when the pattern matches the goal's symbolic form; the pattern's bindings then fill the side conditions.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
problem
|
Problem
|
The problem. |
required |
Returns:
| Type | Description |
|---|---|
list[RewriteCandidate]
|
The applicable rewrites. |
Examples:
>>> from veriphy.toolkit import read_problem
>>> prob = read_problem({'vars': ['x0', 'x1'], 'atoms': ['x', 'y'], 'carrier': 'ℝ',
... 'hyps': [{'name': 'hx', 'poly': 'x0', 'rel': 'ne', 'text': 'x ≠ 0'},
... {'name': 'hy', 'poly': 'x1', 'rel': 'ne', 'text': 'y ≠ 0'}],
... 'goal': {'kind': 'other', 'rel': 'eq', 'expr': '(log((x0 * x1))) - ((log(x0) + log(x1)))',
... 'text': 'Real.log (x * y) = Real.log x + Real.log y'}})
>>> [str(c.emit(prob)) for c in rewrite_candidates(prob)]
['rw [Real.log_mul (by assumption) (by assumption)]']
Source code in src/veriphy/toolkit/_symbolic_emit.py
550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 | |
root_fact(which)
Return the fact hζ : ζ ^ m = r for the field's standard root: 1, √5 in ℝ or exp (2πi/16) in ℂ.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
which
|
str
|
|
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The fact. |
Examples:
>>> print(root_fact('sqrt5'))
have hζ : Real.sqrt 5 ^ 2 = algebraMap ℚ _ (5) := by
rw [Real.sq_sqrt (by norm_num)]; simp
Source code in src/veriphy/toolkit/_fusion.py
345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 | |
root_proof(p_lean, a, b, p)
Return a proof of ∃! x : ℝ, (a < x ∧ x < b) ∧ p x = 0 for an interval from isolate_roots.
Existence is the intermediate value theorem with the endpoint signs; uniqueness is strict monotonicity on
[a, b], from the derivative's sign, which nlinarith checks on the interval.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
p_lean
|
str
|
The polynomial as the goal writes it, as a function of |
required |
a
|
object
|
The interval's left end. |
required |
b
|
object
|
The interval's right end. |
required |
p
|
Polynomial
|
The polynomial (Sage), to read the signs and the derivative. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the signs at the ends agree, or |
Source code in src/veriphy/toolkit/_numerics.py
191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 | |
smith_certificate(a)
Return the Smith normal form D = U A V of a square integer matrix, with facts proving it.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
a
|
Matrix
|
A square integer matrix. |
required |
Returns:
| Type | Description |
|---|---|
Matrix
|
|
Matrix
|
are integer matrices, so |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the matrix is not square and integral. |
Examples:
>>> d, u, v, facts = smith_certificate(matrix(ZZ, [[2, 4], [6, 8]]))
>>> d.diagonal()
[2, 4]
Source code in src/veriphy/toolkit/_normal_form.py
19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 | |
smul_combination(coefficients, names)
Return the Lean text of Σ cₖ • nameₖ, leaving out zero terms and unit coefficients.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
coefficients
|
Sequence[object]
|
Rational coefficients. |
required |
names
|
Sequence[str]
|
The Lean terms they multiply. |
required |
Returns:
| Type | Description |
|---|---|
str
|
The text, |
Examples:
>>> smul_combination([2, 0, -1], ['e', 'f', 'h'])
'2 • e - h'
>>> smul_combination([QQ(1) / 2, 1], ['x', 'y'])
'(1 / 2 : ℚ) • x + y'
>>> smul_combination([0, 0], ['x', 'y'])
'0'
Source code in src/veriphy/toolkit/_lie.py
156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 | |
so7_spinor_gammas()
Return seven anticommuting real antisymmetric 8 by 8 matrices squaring to -1 (the spinor of so(7)).
Returns:
| Type | Description |
|---|---|
list[Matrix]
|
The gamma matrices, tensor products of |
list[Matrix]
|
( |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If no such set is found (it always is). |
Source code in src/veriphy/toolkit/_superalgebra.py
382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 | |
solve_exact_lp(nvars, eqs=(), les=(), objective=None, nonneg=False, *, maximize=False)
Solve a linear program exactly over the rationals.
A row (coeffs, const) means sum(coeffs[j] * t_j) + const, which is = 0 in eqs and <= 0 in les. A row
with only zero coefficients is decided directly, and a problem with no variables or no live rows never reaches the
solver backend.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
nvars
|
int
|
The number of variables |
required |
eqs
|
Iterable[Row]
|
The equality rows. |
()
|
les
|
Iterable[Row]
|
The inequality rows. |
()
|
objective
|
Sequence[object] | None
|
The objective coefficients, or |
None
|
nonneg
|
bool | Iterable[int]
|
|
False
|
maximize
|
bool
|
Whether to maximize the objective instead of minimizing it. |
False
|
Returns:
| Type | Description |
|---|---|
list[Rational] | None
|
The exact solution, or |
Examples:
>>> solve_exact_lp(1, eqs=[([3], -1)])
[1/3]
>>> solve_exact_lp(1, les=[([1], 0), ([-1], 1)]) is None
True
Source code in src/veriphy/toolkit/_lp.py
25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 | |
solve_exists(problem, proofs=None, solution=None)
Prove ∃ x, (∀ t, ODE) ∧ conditions by solving the equation with Sage and checking the solution.
Sage's desolve finds the solution with the initial conditions (or solution is used, a body in s_); the proof
supplies it as the witness, states its derivatives as facts, and closes each conjunct.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
problem
|
Problem
|
The problem; its goal is an existential over an unknown function. |
required |
proofs
|
Mapping[str, str] | None
|
Tactics proving nonzero conditions no hypothesis states, by their Lean text. |
None
|
solution
|
Expression | None
|
A solution body in the variable |
None
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the goal is not such an existential, or Sage finds no solution. |
Source code in src/veriphy/toolkit/_ode.py
178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 | |
solve_recurrence(coefficients, initial)
Return the closed form of a(n + d) = c₀ a(n) + … + c_{d-1} a(n + d - 1) with initial values.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
coefficients
|
Sequence[object]
|
|
required |
initial
|
Sequence[object]
|
|
required |
Returns:
| Type | Description |
|---|---|
Expr
|
The closed form in |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If sympy finds none. |
Examples:
>>> solve_recurrence([-6, 5], [0, 1])
-2**n + 3**n
Source code in src/veriphy/toolkit/_summation.py
201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 | |
sos_decomposition(p)
Find an exact sum of squares p = Σ cᵢ qᵢ² with rational cᵢ > 0, through a numeric SDP.
The Gram matrix is parametrized exactly over QQ. The SDP maximizes its smallest eigenvalue margin, and the
weights are rounded to rationals at increasing precision until the exact matrix is positive semidefinite. The
squares come from its exact LDLᵀ factorization and are checked to sum to p. A polynomial with real zeros whose
Gram matrices all lie on the boundary of the positive semidefinite cone with an irrational kernel cannot be
rounded exactly, and is reported as a failure. Supply candidate squares to the exact LP instead.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
p
|
MPolynomial
|
A polynomial over QQ. |
required |
Returns:
| Type | Description |
|---|---|
list[tuple[Rational, MPolynomial]]
|
The |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If no exact sum of squares is found. |
Examples:
>>> from veriphy.toolkit import create_ring
>>> x, y = create_ring(['x', 'y']).gens()
>>> p = x**4 + 2*x**2*y**2 + y**4 - x**2 - 2*x*y - y**2 + QQ(11) / 10
>>> sum(c * q**2 for c, q in sos_decomposition(p)) == p
True
Source code in src/veriphy/toolkit/_sos.py
85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 | |
sparse_rows_term(table, ring=None)
Return the rows of a table, the nonzero (k, c) of each [eᵢ, eⱼ}, as a Lean term.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
table
|
Table
|
Rational structure constants. |
required |
ring
|
str | None
|
|
None
|
Returns:
| Type | Description |
|---|---|
str
|
The term |
Examples:
>>> rows = sparse_rows_term([[[0, 0], [0, 1]], [[0, -1], [0, 0]]])
>>> rows.startswith('(fun (i j : Fin 2) => ((([[[], [(1, 1)]], [[(1, -1)], []]] : List (List (List (Fin 2 × ℤ')
True
Source code in src/veriphy/toolkit/_superalgebra.py
434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 | |
spin_representation(two_j)
Return [e, f, h] of 𝔰𝔩₂ on spin j = two_j / 2, in the basis vₖ = fᵏ v / k! (k = 0 … 2j).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
two_j
|
int
|
Twice the spin. |
required |
Returns:
| Type | Description |
|---|---|
Rep
|
The three matrices, |
Examples:
>>> [m.list() for m in spin_representation(1)]
[[0, 1, 0, 0], [0, 0, 1, 0], [1, 0, 0, -1]]
Source code in src/veriphy/toolkit/_representation.py
55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 | |
sq_nonneg(q, problem)
Build the proof term sq_nonneg (q).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
q
|
object
|
The expression squared, a Lean term or a polynomial of the problem. |
required |
problem
|
Problem
|
The problem. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The term. |
Examples:
>>> from veriphy.toolkit import read_problem
>>> prob = read_problem({'vars': ['x0', 'x1'], 'atoms': ['a', 'b'], 'goal': {'kind': 'false'}})
>>> str(sq_nonneg('x0 - x1', prob))
'sq_nonneg (a - b)'
Source code in src/veriphy/toolkit/_emit.py
138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 | |
steps(*blocks)
Sequence tactic blocks, one after another.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
*blocks
|
Lean
|
The tactics, in order. |
()
|
Returns:
| Type | Description |
|---|---|
Lean
|
The combined tactic block. |
Raises:
| Type | Description |
|---|---|
VeriphyError
|
If there are no blocks. |
Examples:
>>> print(steps(tactic('intro x'), tactic('positivity')))
intro x
positivity
Source code in src/veriphy/toolkit/_emit.py
504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 | |
structure_constants(basis)
Return c[i][j][k], the coefficient of eₖ in ⁅eᵢ, eⱼ⁆ = eᵢ eⱼ - eⱼ eᵢ.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
basis
|
Sequence[Matrix]
|
Square matrices of one size, over ℚ, a number field or Sage's symbolic ring. |
required |
Returns:
| Type | Description |
|---|---|
Table
|
The table, with entries in the matrices' ring. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the basis is dependent, or not closed under the bracket (naming the first pair whose bracket leaves the span). |
Examples:
>>> e, f, h = matrix(QQ, [[0, 1], [0, 0]]), matrix(QQ, [[0, 0], [1, 0]]), matrix(QQ, [[1, 0], [0, -1]])
>>> c = structure_constants([e, f, h])
>>> c[2][0], c[2][1], c[0][1]
([2, 0, 0], [0, -2, 0], [0, 0, 1])
>>> structure_constants([e, f])
Traceback (most recent call last):
...
veriphy.core._errors.CertificateError: the basis is not closed under the bracket: ⁅e0, e1⁆ is not in its span
Source code in src/veriphy/toolkit/_lie.py
34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 | |
structure_constants_term(table)
Return a structure-constant table as a Lean term Fin n → Fin n → Fin n → ℤ (or ℚ when not integral).
VeriphyCheck.jacobi_of_check (by decide +kernel) and bracket_self_of_check then prove the Lie axioms for it.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
table
|
Sequence[Sequence[Sequence[object]]]
|
|
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The term. |
Examples:
>>> print(structure_constants_term([[[0, 0], [0, 1]], [[0, -1], [0, 0]]]))
(![![![0, 0], ![0, 1]], ![![0, -1], ![0, 0]]] : Fin 2 → Fin 2 → Fin 2 → ℤ)
>>> print(structure_constants_term([[[0, 0], [0, 1/2]], [[0, -1/2], [0, 0]]]))
(![![![0, 0], ![0, (1 / 2)]], ![![0, (-1 / 2)], ![0, 0]]] : Fin 2 → Fin 2 → Fin 2 → ℚ)
Source code in src/veriphy/toolkit/_reflect.py
155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 | |
sum_by_induction(variable, index_set='range', lower=0)
Prove ∑ k ∈ s n, f k = F n by induction on n, each case by push_cast and ring1.
The index set s n is Finset.range n, Finset.Icc lower n or Finset.Ico lower n, with lower 0 or 1 (a
sum from elsewhere is first rewritten to start there, for example with Finset.sum_Ico_eq_sum_range).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
variable
|
str
|
The name of the natural-number variable |
required |
index_set
|
str
|
|
'range'
|
lower
|
int
|
The lower bound of an |
0
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic block. |
Raises:
| Type | Description |
|---|---|
VeriphyError
|
If the index set or lower bound is not supported. |
Examples:
>>> print(sum_by_induction('n'))
induction n with
| zero => rw [Finset.sum_range_zero]; (try push_cast); ring1
| succ n ih => rw [Finset.sum_range_succ, ih]; (try push_cast); ring1
>>> print(sum_by_induction('n', 'Icc', 1))
induction n with
| zero => simp
| succ n ih => rw [Finset.sum_Icc_succ_top (by omega), ih]; (try push_cast); ring1
Source code in src/veriphy/toolkit/_emit.py
449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 | |
super_casimir(basis, parities, form)
Return the quadratic Casimir Σ (B⁻¹) eᵢ eⱼ for an invariant form, checked to commute with every basis element.
The order of the inverse form's indices differs between conventions for superalgebras; Sage tries both and keeps the one that commutes.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
basis
|
Sequence[Matrix]
|
Homogeneous supermatrices. |
required |
parities
|
Sequence[int]
|
Their parities. |
required |
form
|
Matrix
|
An invariant nondegenerate form on the basis. |
required |
Returns:
| Type | Description |
|---|---|
Matrix
|
The Casimir (an even supermatrix). |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the form is degenerate, or neither ordering commutes. |
Source code in src/veriphy/toolkit/_superalgebra.py
142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 | |
super_jacobi_certificate(table, parities, name='hsuper')
Return a fact that the structure constants satisfy the super-Jacobi identity on every basis triple.
Sage checks it first; the kernel checks it again on the sparse table (VeriphyCheck.Sparse.superJacobiCheck),
at a cost that follows the nonzero products of constants.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
table
|
Table
|
Rational structure constants (integers check fastest; see |
required |
parities
|
Sequence[int]
|
The basis parities. |
required |
name
|
str
|
The fact's name. |
'hsuper'
|
Returns:
| Type | Description |
|---|---|
Lean
|
The fact |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the identity fails in Sage, naming a violation. |
Source code in src/veriphy/toolkit/_superalgebra.py
499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 | |
super_jacobi_family_certificate(table0, table1, parities, name='hfamily', field='ℝ')
Return a fact that c₀ + α c₁ satisfies super-Jacobi for every α in any field of characteristic zero.
The super-Jacobi sums are quadratic in α, so the kernel checks at α = 0, 1 and -1 decide them.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
table0
|
Table
|
The constant part of the structure constants. |
required |
table1
|
Table
|
The part linear in |
required |
parities
|
Sequence[int]
|
The basis parities. |
required |
name
|
str
|
The fact's name. |
'hfamily'
|
field
|
str
|
The field of characteristic zero |
'ℝ'
|
Returns:
| Type | Description |
|---|---|
Lean
|
The fact |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the identity fails in Sage at one of the three values. |
Source code in src/veriphy/toolkit/_superalgebra.py
526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 | |
super_jacobi_violations(table, parities)
Return the basis triples and coordinates (i, j, k, m) where the super-Jacobi identity fails.
The identity is (-1)^(|i||k|) [eᵢ, [eⱼ, eₖ}} + (-1)^(|j||i|) [eⱼ, [eₖ, eᵢ}} + (-1)^(|k||j|) [eₖ, [eᵢ, eⱼ}} = 0.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
table
|
Table
|
Structure constants. |
required |
parities
|
Sequence[int]
|
The basis parities. |
required |
Returns:
| Type | Description |
|---|---|
list[tuple[int, int, int, int]]
|
The violations, empty for a Lie superalgebra. |
Source code in src/veriphy/toolkit/_superalgebra.py
179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 | |
super_relations(basis, parities, names)
Return facts stating each graded bracket of a basis of supermatrices, checked by the kernel.
An odd pair gets the anticommutator x * y + y * x = …, any other the commutator x * y - y * x = ….
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
basis
|
Sequence[Matrix]
|
Homogeneous supermatrices over ℚ. |
required |
parities
|
Sequence[int]
|
Their parities. |
required |
names
|
Sequence[str]
|
Their Lean names (definitions). |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The facts |
Source code in src/veriphy/toolkit/_superalgebra.py
563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 | |
super_structure_constants(basis, parities)
Return the structure constants of the graded commutator on a basis of supermatrices.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
basis
|
Sequence[Matrix]
|
Homogeneous supermatrices. |
required |
parities
|
Sequence[int]
|
Their parities. |
required |
Returns:
| Type | Description |
|---|---|
Table
|
|
Raises:
| Type | Description |
|---|---|
CertificateError
|
If a bracket leaves the span, or has the wrong parity (naming the pair). |
Examples:
>>> h, e = matrix(QQ, [[1, 0], [0, 1]]), matrix(QQ, [[0, 1], [0, 0]])
>>> f = matrix(QQ, [[0, 0], [1, 0]])
>>> c = super_structure_constants([h, e, f], [0, 1, 1])
>>> c[1][2]
[1, 0, 0]
Source code in src/veriphy/toolkit/_superalgebra.py
88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 | |
supertrace(m, even_dim)
Return the supertrace tr A - tr D of a supermatrix [[A, B], [C, D]] with A of size even_dim.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
m
|
Matrix
|
The supermatrix. |
required |
even_dim
|
int
|
The dimension of the even part. |
required |
Returns:
| Type | Description |
|---|---|
object
|
The supertrace. |
Examples:
>>> supertrace(identity_matrix(QQ, 3), 1)
-1
Source code in src/veriphy/toolkit/_superalgebra.py
47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 | |
supertrace_form(basis, even_dim)
Return the supertrace form B[i][j] = str(eᵢ eⱼ) of a basis of supermatrices.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
basis
|
Sequence[Matrix]
|
Homogeneous supermatrices. |
required |
even_dim
|
int
|
The dimension of the even part of the superspace. |
required |
Returns:
| Type | Description |
|---|---|
Matrix
|
The form's matrix. |
Source code in src/veriphy/toolkit/_superalgebra.py
129 130 131 132 133 134 135 136 137 138 139 | |
symbolic(expr, problem, lean_type=None)
Render a Sage symbolic expression over the problem's variables as a Lean term over its atoms.
Functions render through the problem's translation tables, dispatching on type: exp, log, sin, cos,
tan render as their Complex versions when the argument mentions I or a ℂ atom and as Real versions
otherwise; abs renders as |·|, pi as Real.pi, I as Complex.I. The term is rendered at lean_type (the
problem's carrier by default) and ascribed to it; integer-valued operators (factorial, binomial, gcd,
remainders, floor, ceil) and sub-expressions Lean computes at ℕ or ℤ render at that type and are cast. A
function outside the tables, a symbol that is not an atom, or a fraction or ℕ subtraction rendered at ℕ or ℤ
raises CertificateError.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
expr
|
object
|
A symbolic expression, or anything Sage's symbolic ring converts, over |
required |
problem
|
Problem
|
The problem whose atoms name the variables. |
required |
lean_type
|
str | None
|
The Lean type of the term, the problem's carrier when |
None
|
Returns:
| Type | Description |
|---|---|
Lean
|
The term. |
Examples:
>>> from sage.all import exp, sqrt
>>> from veriphy.toolkit import read_problem
>>> prob = read_problem({'vars': ['x0', 'x1'], 'atoms': ['x', 'z'], 'atom_types': ['ℝ', 'ℂ'],
... 'goal': {'kind': 'false'}})
>>> x0, x1 = prob.symbols['x0'], prob.symbols['x1']
>>> str(symbolic(abs(x0 - 1), prob)), str(symbolic(exp(x1), prob)), str(symbolic(sqrt(x0) / (x0**2 + 1), prob))
('|x - 1|', 'Complex.exp z', '(Real.sqrt x) / (x ^ 2 + 1)')
>>> nat = read_problem({'vars': ['x0', 'x1'], 'atoms': ['x', 'n'], 'atom_types': ['ℝ', 'ℕ'], 'carrier': 'ℝ',
... 'goal': {'expr': "(typed(mod(x1, 7), 'ℕ') + x0) - (x0)", 'kind': 'other', 'rel': 'le', 'text': ''}})
>>> str(symbolic(nat.goal.expr + nat.symbols['x0'], nat))
'(x + ((n % 7 : ℕ) : ℝ) : ℝ)'
>>> str(symbolic(nat.symbols['x1'] + 1, nat, lean_type='ℕ'))
'(n + 1 : ℕ)'
Source code in src/veriphy/toolkit/_symbolic_emit.py
258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 | |
tactic(text)
Wrap Lean source as a tactic.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
text
|
str
|
The Lean source of a tactic or tactic block. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Examples:
>>> tactic('norm_num').kind
'tactic'
Source code in src/veriphy/toolkit/_lean.py
59 60 61 62 63 64 65 66 67 68 69 70 71 72 | |
tensor_representation(rho, sigma)
Return the tensor product representation, x ↦ ρ(x) ⊗ 1 + 1 ⊗ σ(x).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
rho
|
Rep
|
The first representation, one matrix per basis element of the algebra. |
required |
sigma
|
Rep
|
The second, on the same basis. |
required |
Returns:
| Type | Description |
|---|---|
Rep
|
The product's matrices. |
Source code in src/veriphy/toolkit/_representation.py
79 80 81 82 83 84 85 86 87 88 89 90 | |
term(text)
Wrap Lean source as a term.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
text
|
str
|
The Lean source of a term. |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The term. |
Examples:
>>> str(term('h1'))
'h1'
Source code in src/veriphy/toolkit/_lean.py
43 44 45 46 47 48 49 50 51 52 53 54 55 56 | |
term_lean(e)
Return a hypergeometric term as a Lean lambda fun n k => … over ℚ, zero where a shifted binomial is negative.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
e
|
Expr
|
The term, in the symbols |
required |
Returns:
| Type | Description |
|---|---|
str
|
The lambda. |
Examples:
>>> print(term_lean(-sp.binomial(N, K - 1) / (2 * 2**N)))
fun (n k : ℕ) => if k < 1 then 0 else (((-1 : ℚ) / 2) * ((2 : ℚ) ^ (n))⁻¹ * ((n).choose (k - 1) : ℚ))
Source code in src/veriphy/toolkit/_summation.py
71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 | |
trace_form(basis)
Return the trace form of the representation, B[i][j] = tr(eᵢ eⱼ).
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
basis
|
Sequence[Matrix]
|
The representation matrices. |
required |
Returns:
| Type | Description |
|---|---|
Matrix
|
The symmetric matrix of the form. |
Source code in src/veriphy/toolkit/_lie.py
107 108 109 110 111 112 113 114 115 116 117 | |
verify_definition(problem, proofs=None)
Prove an ODE goal about a function defined explicitly by a hypothesis x = fun s => ….
The proof substitutes the definition, states each derivative of the body as a fact, rewrites with them and closes
the remaining identity by ring1, field_simp or norm_num.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
problem
|
Problem
|
The problem; its goal is an equation in an unknown function that a hypothesis defines. |
required |
proofs
|
Mapping[str, str] | None
|
Tactics proving nonzero conditions no hypothesis states, by their Lean text. |
None
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic block. |
Raises:
| Type | Description |
|---|---|
CertificateError
|
If no hypothesis defines a function of the goal. |
Source code in src/veriphy/toolkit/_ode.py
102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 | |
weyl_group_order(cartan_type)
Return the order of the Weyl group, from Sage.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
cartan_type
|
str
|
The type, as |
required |
Returns:
| Type | Description |
|---|---|
int
|
The order. |
Examples:
>>> weyl_group_order('E8')
696729600
Source code in src/veriphy/toolkit/_lie.py
358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 | |
witness(values, side)
Close an existential goal with exact rational values and a tactic for the side conditions.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
values
|
Sequence[object]
|
One rational per binder. |
required |
side
|
Lean
|
The tactic proving the body at those values, such as |
required |
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Examples:
>>> str(witness([1, QQ(-1) / 2], tactic('norm_num')))
'exact ⟨1, -(1 / 2), by norm_num⟩'
Source code in src/veriphy/toolkit/_emit.py
378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 | |
wz_mate(f)
Return the WZ mate G of a summand F(n, k) with Σₖ F(n, k) constant in n.
G satisfies F(n + 1, k) - F(n, k) = G(n, k + 1) - G(n, k); it is Gosper's antidifference in k of the left
side.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
f
|
Expr
|
The normalized summand (its sum over |
required |
Returns:
| Type | Description |
|---|---|
Expr
|
|
Raises:
| Type | Description |
|---|---|
CertificateError
|
If the difference is not Gosper-summable (no WZ pair). |
Examples:
>>> wz_mate(sp.binomial(N, K) / 2**N)
-binomial(n, k - 1)/(2*2**n)
Source code in src/veriphy/toolkit/_summation.py
91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 | |
wz_proof(f, closed_form, closed_form_lean, mate=None)
Return a proof of ∑ k ∈ Finset.range (n + 1), F n k = S n (with n in scope) by a WZ pair.
The normalized summand F / S sums to 1: the summand identity telescopes, the sum is constant in n, and it is 1
at n = 0. F must vanish at k = n + 1 (natural boundaries), and S n ≠ 0 closes by positivity.
Parameters:
| Name | Type | Description | Default |
|---|---|---|---|
f
|
Expr
|
The summand |
required |
closed_form
|
Expr
|
|
required |
closed_form_lean
|
str
|
The Lean text of |
required |
mate
|
Expr | None
|
The WZ mate of |
None
|
Returns:
| Type | Description |
|---|---|
Lean
|
The tactic. |
Source code in src/veriphy/toolkit/_summation.py
119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 | |