UOR Schema

IRI: https://uor.foundation/schema/
Prefix: schema:
Space: kernel
Comment: Core value types and term language for the UOR ring substrate. Defines Datum (ring element), Term (syntactic expression), and the Ring container.

This is a kernel-space namespace in the Define stage of the PRISM pipeline. It provides the immutable algebraic substrate — ring structure, schema vocabulary, and operation algebra.

Learn more: Pipeline Overview · The Ring Substrate

Class hierarchy

Imports

https://uor.foundation/u/

Classes

Name	Subclass Of	Disjoint With	Comment
`Datum`	`Thing`	`Term`	An element of the ring Z/(2^n)Z at a specific Witt level n. The primary semantic value type. Disjoint from Term: datums are values, terms are syntactic expressions that evaluate to datums.
`Term`	`Thing`	`Datum`	A syntactic expression in the UOR term language. Terms are evaluated to produce Datums. Disjoint from Datum.
`Triad`	`Thing`		A three-component structure encoding an element's position in the UOR address space: stratum (ring layer), spectrum (bit pattern), and glyph (Braille address).
`Literal`	`Term`, `SurfaceSymbol`		A term that directly denotes a datum value. A Literal is a leaf node in the term language — it refers to a concrete Datum via schema:denotes without being a Datum itself.
`Application`	`Term`		A term formed by applying an operation to one or more argument terms. The application's value is the result of evaluating the operator on the evaluated arguments.
`Ring`	`Thing`		The ambient ring Z/(2^n)Z at a specific Witt level n. The Ring is the primary data structure of the UOR kernel. Its two generators (negation and complement) produce the dihedral group D_{2^n} that governs the invariance frame.
`W16Ring`	`Ring`		The concrete ring Z/(2^16)Z at Witt level 16. Subclass of schema:Ring. Carries 65,536 elements. W16Ring is the first extension of the default Q0 ring and is the target of Amendment 26's universality proofs.
`WittLevel`	`Thing`		A named Witt level Q_k at which the UOR ring operates. Level Q_k uses 8(k+1) bits, 2^(8(k+1)) states, and modulus 2^(8*(k+1)). The named individuals Q0-Q3 are the spec-defined reference levels. The class is open: Prism implementations operating at higher levels declare their own WittLevel individuals. The nextWittLevel property forms an unbounded chain Q0 -> Q1 -> Q2 -> ...
`TermExpression`	`Thing`		Root AST node for parsed EBNF term expressions. Identity lhs/rhs values are instances of TermExpression subtypes. Maps to the `term` production in the EBNF grammar.
`LiteralExpression`	`TermExpression`		A leaf AST node: an integer literal, variable reference, or named constant.
`ApplicationExpression`	`TermExpression`		An AST node representing operator application: an operator applied to an argument list (e.g., add(x, y)).
`InfixExpression`	`TermExpression`		An AST node for infix relations and logical connectives (e.g., x <= y, P -> Q, a = b).
`SetExpression`	`TermExpression`		An AST node for set-builder notation (e.g., {x : P(x)}).
`CompositionExpression`	`TermExpression`		An AST node for function composition (f compose g).
`ForAllDeclaration`	`Thing`		A structured quantifier binding: typed variable declarations with a domain and quantifier kind (universal or existential). Replaces the string-valued op:forAll property.
`VariableBinding`	`Thing`		A single variable binding: a variable name bound to a domain type (e.g., x in R_n).
`QuantifierKind`	`Thing`		The kind of quantifier: Universal (forall) or Existential (exists). Controlled vocabulary with exactly 2 individuals.
`SurfaceSymbol`	`Thing`		An abstract leaf value that a grounding map can accept as surface input. Has no direct instances: every SurfaceSymbol is either a Datum-denoting schema:Literal or an xsd-typed schema:HostValue, and the two cases are disjoint.
`HostValue`	`SurfaceSymbol`	`Term`, `Datum`	An xsd-typed value that denotes a host datatype rather than a ring datum. Used in property-position slots whose range is xsd and as the host-side input of a grounding map.
`HostStringLiteral`	`HostValue`		A host string literal carrying an xsd:string value.
`HostBooleanLiteral`	`HostValue`		A host boolean literal carrying an xsd:boolean value.

Properties

Name	Kind	Functional	Domain	Range	Comment
`value`	Datatype	true	`Datum`	`nonNegativeInteger`	The integer value of a datum element. For a Datum in Z/(2^n)Z, this is an integer in [0, 2^n).
`wittLength`	Datatype	true	`Datum`	`positiveInteger`	The Witt level n of a datum, where the datum's ring is Z/(2^n)Z. Determines the bit width and modulus of the datum.
`stratum`	Datatype	true	`Datum`	`nonNegativeInteger`	The ring-layer index of a datum, indicating its position in the stratification of Z/(2^n)Z.
`spectrum`	Datatype	true	`Datum`	`nonNegativeInteger`	The bit-pattern representation of a datum, encoding its position in the hypercube geometry of Z/(2^n)Z.
`element`	Object	true	`Datum`	`Element`	The content-addressable element associated with this datum, linking the algebraic value to its identifier.
`operator`	Object	true	`Application`	`Operation`	The operation applied in an Application term.
`argument`	Object	false	`Application`	`Term`	An argument term in an Application. The ordering of arguments follows rdf:List semantics.
`ringWittLength`	Datatype	true	`Ring`	`positiveInteger`	The bit width n of the ring Z/(2^n)Z. Distinct from schema:wittLength on Datum — ringWittLength is the container's bit width; datum wittLength is a membership property.
`modulus`	Datatype	true	`Ring`	`positiveInteger`	The modulus 2^n of the ring. Equals 2 raised to the power of ringWittLength.
`generator`	Object	true	`Ring`	`Datum`	The generator element π₁ (value = 1) of the ring. Under iterated successor application, π₁ generates all ring elements.
`negation`	Object	true	`Ring`	`Involution`	The ring reflection involution: neg(x) = (-x) mod 2^n. One of the two generators of the dihedral group D_{2^n}.
`complement`	Object	true	`Ring`	`Involution`	The hypercube reflection involution: bnot(x) = (2^n - 1) ⊕ x. The second generator of the dihedral group D_{2^n}.
`denotes`	Object	true	`Literal`	`Datum`	The datum value that a Literal term denotes. Bridges the Term/Datum disjointness: a Literal refers to a Datum without being one. Evaluation of a Literal produces its denoted Datum.
`bitsWidth`	Datatype	true	`WittLevel`	`positiveInteger`	The bit width 8*(k+1) of this Witt level.
`cycleSize`	Datatype	true	`WittLevel`	`positiveInteger`	The number of distinct states 2^(8*(k+1)) at this Witt level.
`nextWittLevel`	Object	true	`WittLevel`	`WittLevel`	The next Witt level in the chain: Q_k -> Q_(k+1). The chain is unbounded; Q3 points to Q4, which is not a named individual in the spec but may be declared by Prism implementations.
`wittLevelPredecessor`	Object	true	`WittLevel`	`WittLevel`	The predecessor Witt level in the chain: Q_(k+1) -> Q_k. Inverse of nextWittLevel. If nextWittLevel(Q_k) = Q_(k+1), then wittLevelPredecessor(Q_(k+1)) = Q_k. Formalizes the chain extension protocol (QL_8).
`atWittLevel`	Object	true	`Ring`	`WittLevel`	The Witt level at which this Ring instance operates. Links a concrete Ring individual to its WittLevel.
`W16bitWidth`	Datatype	true	`W16Ring`	`positiveInteger`	Bit width of the Q1 ring: 16.
`W16capacity`	Datatype	true	`W16Ring`	`positiveInteger`	Carrier set size of the Q1 ring: 65,536 elements.
`boundVariables`	Object	false	`ForAllDeclaration`	`VariableBinding`	The variable bindings in a quantifier declaration. Non-functional: a ForAllDeclaration may bind multiple variables.
`variableDomain`	Object	true	`VariableBinding`	`Class`	The domain type of a variable binding (e.g., schema:Ring, type:ConstrainedType).
`variableName`	Datatype	true	`VariableBinding`	`string`	The name of a bound variable (e.g., 'x', 'y', 'n').
`quantifierKind`	Object	true	`ForAllDeclaration`	`QuantifierKind`	The kind of quantifier: Universal or Existential.
`expressionOperator`	Object	true	`ApplicationExpression`	`Operation`	The operator in an application expression (e.g., op:add, op:neg).
`leftOperand`	Object	true	`InfixExpression`	`TermExpression`	The left operand of an infix expression.
`rightOperand`	Object	true	`InfixExpression`	`TermExpression`	The right operand of an infix expression.
`arguments`	Object	false	`ApplicationExpression`	`TermExpression`	The argument list of an application expression. Non-functional: an application may take multiple arguments.
`literalValue`	Datatype	true	`LiteralExpression`	`string`	The string representation of a literal expression value (e.g., '42', 'x', 'pi1').
`infixOperator`	Datatype	true	`InfixExpression`	`string`	The operator symbol in an infix expression (e.g., '=', '\u{2264}', '\u{2192}').
`hostString`	Datatype	true	`HostStringLiteral`	`string`	The string value carried by a HostStringLiteral.
`hostBoolean`	Datatype	true	`HostBooleanLiteral`	`boolean`	The boolean value carried by a HostBooleanLiteral.

Named Individuals

Name	Type	Comment
`Universal`	`QuantifierKind`	Universal quantification (forall).
`Existential`	`QuantifierKind`	Existential quantification (exists).
`π₁`	`Datum`	The unique generator of R_n under successor. Value = 1 at every Witt level. Under iterated application of succ, π₁ generates every element of the ring.
`value`: 1
`zero`	`Datum`	The additive identity of the ring. Value = 0 at every Witt level. op:add(x, zero) = x for all x in R_n.
`value`: 0
`W8`	`WittLevel`	Witt level 0: 8-bit ring Z/256Z, 256 states. The reference level for all ComputationCertificate proofs in the spec.
`bitsWidth`: 8 `cycleSize`: 256 `nextWittLevel`: `W16`
`W16`	`WittLevel`	Witt level 1: 16-bit ring Z/65536Z, 65,536 states.
`bitsWidth`: 16 `cycleSize`: 65536 `nextWittLevel`: `W24` `wittLevelPredecessor`: `W8`
`W24`	`WittLevel`	Witt level 2: 24-bit ring Z/16777216Z, 16,777,216 states.
`bitsWidth`: 24 `cycleSize`: 16777216 `nextWittLevel`: `W32` `wittLevelPredecessor`: `W16`
`W32`	`WittLevel`	Witt level 3: 32-bit ring Z/4294967296Z, 4,294,967,296 states. The highest named level in the spec. nextWittLevel is absent — Prism implementations may extend the chain.
`bitsWidth`: 32 `cycleSize`: 4294967296 `wittLevelPredecessor`: `W24`
`term_criticalIdentity_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_AD_1_lhs`	`LiteralExpression`
`literalValue`: addresses(glyph(d))
`term_AD_1_rhs`	`LiteralExpression`
`literalValue`: d
`term_AD_1_forAll`	`ForAllDeclaration`
`variableName`: d ∈ R_n
`term_AD_2_lhs`	`LiteralExpression`
`literalValue`: glyph(ι(addresses(a)))
`term_AD_2_rhs`	`LiteralExpression`
`literalValue`: ι_addr(a)
`term_AD_2_forAll`	`ForAllDeclaration`
`variableName`: a ∈ Addr(R_n), ι : R_n → R_{n'}
`term_R_A1_lhs`	`LiteralExpression`
`literalValue`: add(x, add(y, z))
`term_R_A1_rhs`	`LiteralExpression`
`literalValue`: add(add(x, y), z)
`term_R_A1_forAll`	`ForAllDeclaration`
`variableName`: x, y, z ∈ R_n
`term_R_A2_lhs`	`LiteralExpression`
`literalValue`: add(x, 0)
`term_R_A2_rhs`	`LiteralExpression`
`literalValue`: x
`term_R_A2_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_R_A3_lhs`	`LiteralExpression`
`literalValue`: add(x, neg(x))
`term_R_A3_rhs`	`LiteralExpression`
`literalValue`: 0
`term_R_A3_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_R_A4_lhs`	`LiteralExpression`
`literalValue`: add(x, y)
`term_R_A4_rhs`	`LiteralExpression`
`literalValue`: add(y, x)
`term_R_A4_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_R_A5_lhs`	`LiteralExpression`
`literalValue`: sub(x, y)
`term_R_A5_rhs`	`LiteralExpression`
`literalValue`: add(x, neg(y))
`term_R_A5_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_R_A6_lhs`	`LiteralExpression`
`literalValue`: neg(neg(x))
`term_R_A6_rhs`	`LiteralExpression`
`literalValue`: x
`term_R_A6_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_R_M1_lhs`	`LiteralExpression`
`literalValue`: mul(x, mul(y, z))
`term_R_M1_rhs`	`LiteralExpression`
`literalValue`: mul(mul(x, y), z)
`term_R_M1_forAll`	`ForAllDeclaration`
`variableName`: x, y, z ∈ R_n
`term_R_M2_lhs`	`LiteralExpression`
`literalValue`: mul(x, 1)
`term_R_M2_rhs`	`LiteralExpression`
`literalValue`: x
`term_R_M2_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_R_M3_lhs`	`LiteralExpression`
`literalValue`: mul(x, y)
`term_R_M3_rhs`	`LiteralExpression`
`literalValue`: mul(y, x)
`term_R_M3_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_R_M4_lhs`	`LiteralExpression`
`literalValue`: mul(x, add(y, z))
`term_R_M4_rhs`	`LiteralExpression`
`literalValue`: add(mul(x, y), mul(x, z))
`term_R_M4_forAll`	`ForAllDeclaration`
`variableName`: x, y, z ∈ R_n
`term_R_M5_lhs`	`LiteralExpression`
`literalValue`: mul(x, 0)
`term_R_M5_rhs`	`LiteralExpression`
`literalValue`: 0
`term_R_M5_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_B_1_lhs`	`LiteralExpression`
`literalValue`: xor(x, xor(y, z))
`term_B_1_rhs`	`LiteralExpression`
`literalValue`: xor(xor(x, y), z)
`term_B_1_forAll`	`ForAllDeclaration`
`variableName`: x, y, z ∈ R_n
`term_B_2_lhs`	`LiteralExpression`
`literalValue`: xor(x, 0)
`term_B_2_rhs`	`LiteralExpression`
`literalValue`: x
`term_B_2_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_B_3_lhs`	`LiteralExpression`
`literalValue`: xor(x, x)
`term_B_3_rhs`	`LiteralExpression`
`literalValue`: 0
`term_B_3_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_B_4_lhs`	`LiteralExpression`
`literalValue`: and(x, and(y, z))
`term_B_4_rhs`	`LiteralExpression`
`literalValue`: and(and(x, y), z)
`term_B_4_forAll`	`ForAllDeclaration`
`variableName`: x, y, z ∈ R_n
`term_B_5_lhs`	`LiteralExpression`
`literalValue`: and(x, 2^n - 1)
`term_B_5_rhs`	`LiteralExpression`
`literalValue`: x
`term_B_5_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_B_6_lhs`	`LiteralExpression`
`literalValue`: and(x, 0)
`term_B_6_rhs`	`LiteralExpression`
`literalValue`: 0
`term_B_6_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_B_7_lhs`	`LiteralExpression`
`literalValue`: or(x, or(y, z))
`term_B_7_rhs`	`LiteralExpression`
`literalValue`: or(or(x, y), z)
`term_B_7_forAll`	`ForAllDeclaration`
`variableName`: x, y, z ∈ R_n
`term_B_8_lhs`	`LiteralExpression`
`literalValue`: or(x, 0)
`term_B_8_rhs`	`LiteralExpression`
`literalValue`: x
`term_B_8_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_B_9_lhs`	`LiteralExpression`
`literalValue`: and(x, or(x, y))
`term_B_9_rhs`	`LiteralExpression`
`literalValue`: x
`term_B_9_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_B_10_lhs`	`LiteralExpression`
`literalValue`: and(x, or(y, z))
`term_B_10_rhs`	`LiteralExpression`
`literalValue`: or(and(x, y), and(x, z))
`term_B_10_forAll`	`ForAllDeclaration`
`variableName`: x, y, z ∈ R_n
`term_B_11_lhs`	`LiteralExpression`
`literalValue`: bnot(and(x, y))
`term_B_11_rhs`	`LiteralExpression`
`literalValue`: or(bnot(x), bnot(y))
`term_B_11_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_B_12_lhs`	`LiteralExpression`
`literalValue`: bnot(or(x, y))
`term_B_12_rhs`	`LiteralExpression`
`literalValue`: and(bnot(x), bnot(y))
`term_B_12_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_B_13_lhs`	`LiteralExpression`
`literalValue`: bnot(bnot(x))
`term_B_13_rhs`	`LiteralExpression`
`literalValue`: x
`term_B_13_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_X_1_lhs`	`LiteralExpression`
`literalValue`: neg(x)
`term_X_1_rhs`	`LiteralExpression`
`literalValue`: sub(0, x)
`term_X_1_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_X_2_lhs`	`LiteralExpression`
`literalValue`: bnot(x)
`term_X_2_rhs`	`LiteralExpression`
`literalValue`: xor(x, 2^n - 1)
`term_X_2_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_X_3_lhs`	`LiteralExpression`
`literalValue`: succ(x)
`term_X_3_rhs`	`LiteralExpression`
`literalValue`: add(x, 1)
`term_X_3_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_X_4_lhs`	`LiteralExpression`
`literalValue`: pred(x)
`term_X_4_rhs`	`LiteralExpression`
`literalValue`: sub(x, 1)
`term_X_4_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_X_5_lhs`	`LiteralExpression`
`literalValue`: neg(x)
`term_X_5_rhs`	`LiteralExpression`
`literalValue`: add(bnot(x), 1)
`term_X_5_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_X_6_lhs`	`LiteralExpression`
`literalValue`: bnot(x)
`term_X_6_rhs`	`LiteralExpression`
`literalValue`: pred(neg(x))
`term_X_6_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_X_7_lhs`	`LiteralExpression`
`literalValue`: xor(x, y)
`term_X_7_rhs`	`LiteralExpression`
`literalValue`: add(x, y) - 2 * and(x, y)
`term_X_7_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ Z (before mod)
`term_D_1_lhs`	`LiteralExpression`
`literalValue`: succ^{2^n}(x)
`term_D_1_rhs`	`LiteralExpression`
`literalValue`: x
`term_D_1_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_D_3_lhs`	`LiteralExpression`
`literalValue`: neg(succ(neg(x)))
`term_D_3_rhs`	`LiteralExpression`
`literalValue`: pred(x)
`term_D_3_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_D_4_lhs`	`LiteralExpression`
`literalValue`: bnot(neg(x))
`term_D_4_rhs`	`LiteralExpression`
`literalValue`: pred(x)
`term_D_4_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_D_5_lhs`	`LiteralExpression`
`literalValue`: D_{2^n}
`term_D_5_rhs`	`LiteralExpression`
`literalValue`: {succ^k, neg ∘ succ^k : 0 ≤ k < 2^n}
`term_D_5_forAll`	`ForAllDeclaration`
`variableName`: n ≥ 1
`term_U_1_lhs`	`LiteralExpression`
`literalValue`: R_n×
`term_U_1_rhs`	`LiteralExpression`
`literalValue`: Z/2 × Z/2^{n-2}
`term_U_1_forAll`	`ForAllDeclaration`
`variableName`: n ≥ 3
`term_U_2_lhs`	`LiteralExpression`
`literalValue`: R_1× ≅ {1}; R_2× ≅ Z/2
`term_U_2_rhs`	`LiteralExpression`
`literalValue`: special cases for small n
`term_U_2_forAll`	`ForAllDeclaration`
`variableName`: n ∈ {1, 2}
`term_U_3_lhs`	`LiteralExpression`
`literalValue`: ord(u)
`term_U_3_rhs`	`LiteralExpression`
`literalValue`: lcm(ord((-1)^a), ord(3^b))
`term_U_3_forAll`	`ForAllDeclaration`
`variableName`: u = (-1)^a · 3^b ∈ R_n×
`term_U_4_lhs`	`LiteralExpression`
`literalValue`: ord_g(2)
`term_U_4_rhs`	`LiteralExpression`
`literalValue`: divides φ(g)
`term_U_4_forAll`	`ForAllDeclaration`
`variableName`: g odd
`term_U_5_lhs`	`LiteralExpression`
`literalValue`: step_g
`term_U_5_rhs`	`LiteralExpression`
`literalValue`: 2 * ((g - (2^n mod g)) mod g) + 1
`term_U_5_forAll`	`ForAllDeclaration`
`variableName`: g odd, g > 1
`term_AG_1_lhs`	`LiteralExpression`
`literalValue`: μ_u
`term_AG_1_rhs`	`LiteralExpression`
`literalValue`: ∉ D_{2^n}
`term_AG_1_forAll`	`ForAllDeclaration`
`variableName`: u ∈ R_n×, u ≠ ±1
`term_AG_2_lhs`	`LiteralExpression`
`literalValue`: Aff(R_n)
`term_AG_2_rhs`	`LiteralExpression`
`literalValue`: R_n× ⋉ R_n
`term_AG_2_forAll`	`ForAllDeclaration`
`variableName`: n ≥ 1
`term_AG_3_lhs`	`LiteralExpression`
`literalValue`: \|Aff(R_n)\|
`term_AG_3_rhs`	`LiteralExpression`
`literalValue`: 2^{2n-1}
`term_AG_3_forAll`	`ForAllDeclaration`
`variableName`: n ≥ 1
`term_AG_4_lhs`	`LiteralExpression`
`literalValue`: D_{2^n}
`term_AG_4_rhs`	`LiteralExpression`
`literalValue`: ⊂ Aff(R_n), u ∈ {±1}
`term_AG_4_forAll`	`ForAllDeclaration`
`variableName`: n ≥ 1
`term_CA_1_lhs`	`LiteralExpression`
`literalValue`: add(x,y)_k
`term_CA_1_rhs`	`LiteralExpression`
`literalValue`: xor(x_k, xor(y_k, c_k(x,y)))
`term_CA_1_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n, 0 ≤ k < n
`term_CA_2_lhs`	`LiteralExpression`
`literalValue`: c_{k+1}(x,y)
`term_CA_2_rhs`	`LiteralExpression`
`literalValue`: or(and(x_k,y_k), and(xor(x_k,y_k), c_k))
`term_CA_2_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_CA_3_lhs`	`LiteralExpression`
`literalValue`: c(x, y)
`term_CA_3_rhs`	`LiteralExpression`
`literalValue`: c(y, x)
`term_CA_3_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_CA_4_lhs`	`LiteralExpression`
`literalValue`: c(x, 0)
`term_CA_4_rhs`	`LiteralExpression`
`literalValue`: 0
`term_CA_4_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n, all positions
`term_CA_5_lhs`	`LiteralExpression`
`literalValue`: c(x, neg(x))_k
`term_CA_5_rhs`	`LiteralExpression`
`literalValue`: 1
`term_CA_5_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n, k > v_2(x)
`term_CA_6_lhs`	`LiteralExpression`
`literalValue`: d_Δ(x, y) > 0
`term_CA_6_rhs`	`LiteralExpression`
`literalValue`: ∃ k : c_k(x,y) = 1
`term_CA_6_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_C_1_lhs`	`LiteralExpression`
`literalValue`: pins(compose(A, B))
`term_C_1_rhs`	`LiteralExpression`
`literalValue`: pins(A) ∪ pins(B)
`term_C_1_forAll`	`ForAllDeclaration`
`variableName`: constraints A, B
`term_C_2_lhs`	`LiteralExpression`
`literalValue`: compose(A, B)
`term_C_2_rhs`	`LiteralExpression`
`literalValue`: compose(B, A)
`term_C_2_forAll`	`ForAllDeclaration`
`variableName`: constraints A, B
`term_C_3_lhs`	`LiteralExpression`
`literalValue`: compose(compose(A,B), C)
`term_C_3_rhs`	`LiteralExpression`
`literalValue`: compose(A, compose(B,C))
`term_C_3_forAll`	`ForAllDeclaration`
`variableName`: constraints A, B, C
`term_C_4_lhs`	`LiteralExpression`
`literalValue`: compose(A, A)
`term_C_4_rhs`	`LiteralExpression`
`literalValue`: A
`term_C_4_forAll`	`ForAllDeclaration`
`variableName`: constraint A
`term_C_5_lhs`	`LiteralExpression`
`literalValue`: compose(A, ε)
`term_C_5_rhs`	`LiteralExpression`
`literalValue`: A
`term_C_5_forAll`	`ForAllDeclaration`
`variableName`: constraint A, identity ε
`term_C_6_lhs`	`LiteralExpression`
`literalValue`: compose(A, Ω)
`term_C_6_rhs`	`LiteralExpression`
`literalValue`: Ω
`term_C_6_forAll`	`ForAllDeclaration`
`variableName`: constraint A, annihilator Ω
`term_CDI_lhs`	`LiteralExpression`
`literalValue`: carry(residue(T))
`term_CDI_rhs`	`LiteralExpression`
`literalValue`: depth(T)
`term_CDI_forAll`	`ForAllDeclaration`
`variableName`: T ∈ T_n
`term_CL_1_lhs`	`LiteralExpression`
`literalValue`: Constraint/≡
`term_CL_1_rhs`	`LiteralExpression`
`literalValue`: 2^{[n]}
`term_CL_1_forAll`	`ForAllDeclaration`
`variableName`: constraint equivalence classes
`term_CL_2_lhs`	`LiteralExpression`
`literalValue`: A ∨ B
`term_CL_2_rhs`	`LiteralExpression`
`literalValue`: compose(A, B)
`term_CL_2_forAll`	`ForAllDeclaration`
`variableName`: constraints A, B
`term_CL_3_lhs`	`LiteralExpression`
`literalValue`: pins(A ∧ B)
`term_CL_3_rhs`	`LiteralExpression`
`literalValue`: pins(A) ∩ pins(B)
`term_CL_3_forAll`	`ForAllDeclaration`
`variableName`: constraints A, B
`term_CL_4_lhs`	`LiteralExpression`
`literalValue`: (A ∨ B) ∧ C
`term_CL_4_rhs`	`LiteralExpression`
`literalValue`: (A ∧ C) ∨ (B ∧ C)
`term_CL_4_forAll`	`ForAllDeclaration`
`variableName`: constraints A, B, C
`term_CL_5_lhs`	`LiteralExpression`
`literalValue`: A ∧ A̅ = ε, A ∨ A̅ = Ω
`term_CL_5_rhs`	`LiteralExpression`
`literalValue`: ∃ A̅ (complement)
`term_CL_5_forAll`	`ForAllDeclaration`
`variableName`: constraint A
`term_CM_1_lhs`	`LiteralExpression`
`literalValue`: C_i redundant in {C_1,...,C_k}
`term_CM_1_rhs`	`LiteralExpression`
`literalValue`: pins(C_i) ⊆ ∪_{j≠i} pins(C_j)
`term_CM_1_forAll`	`ForAllDeclaration`
`variableName`: constraint set {C_1,...,C_k}
`term_CM_2_lhs`	`LiteralExpression`
`literalValue`: minimal cover
`term_CM_2_rhs`	`LiteralExpression`
`literalValue`: irredundant sub-collection (greedy removal)
`term_CM_2_forAll`	`ForAllDeclaration`
`variableName`: CompositeConstraint
`term_CM_3_lhs`	`LiteralExpression`
`literalValue`: min constraints to cover n sites
`term_CM_3_rhs`	`LiteralExpression`
`literalValue`: ⌈n / max_k pins_per_constraint_k⌉
`term_CM_3_forAll`	`ForAllDeclaration`
`variableName`: n sites, constraint set
`term_CR_1_lhs`	`LiteralExpression`
`literalValue`: cost(ResidueConstraint(m, r))
`term_CR_1_rhs`	`LiteralExpression`
`literalValue`: step_m = 2 × ((−2^n) mod m) + 1
`term_CR_1_forAll`	`ForAllDeclaration`
`variableName`: ResidueConstraint
`term_CR_2_lhs`	`LiteralExpression`
`literalValue`: cost(CarryConstraint(p))
`term_CR_2_rhs`	`LiteralExpression`
`literalValue`: popcount(p)
`term_CR_2_forAll`	`ForAllDeclaration`
`variableName`: CarryConstraint
`term_CR_3_lhs`	`LiteralExpression`
`literalValue`: cost(DepthConstraint(d_min, d_max))
`term_CR_3_rhs`	`LiteralExpression`
`literalValue`: cost(residue) + cost(carry)
`term_CR_3_forAll`	`ForAllDeclaration`
`variableName`: DepthConstraint
`term_CR_4_lhs`	`LiteralExpression`
`literalValue`: cost(compose(A, B))
`term_CR_4_rhs`	`LiteralExpression`
`literalValue`: ≤ cost(A) + cost(B)
`term_CR_4_forAll`	`ForAllDeclaration`
`variableName`: constraints A, B
`term_CR_5_lhs`	`LiteralExpression`
`literalValue`: optimal resolution order
`term_CR_5_rhs`	`LiteralExpression`
`literalValue`: increasing cost order
`term_CR_5_forAll`	`ForAllDeclaration`
`variableName`: constraint set
`term_F_1_lhs`	`LiteralExpression`
`literalValue`: pinned site
`term_F_1_rhs`	`LiteralExpression`
`literalValue`: cannot be unpinned
`term_F_1_forAll`	`ForAllDeclaration`
`variableName`: SiteIndex
`term_F_2_lhs`	`LiteralExpression`
`literalValue`: pin operations to close
`term_F_2_rhs`	`LiteralExpression`
`literalValue`: ≤ n
`term_F_2_forAll`	`ForAllDeclaration`
`variableName`: FreeRank
`term_F_3_lhs`	`LiteralExpression`
`literalValue`: pinnedCount + freeRank
`term_F_3_rhs`	`LiteralExpression`
`literalValue`: totalSites = n
`term_F_3_forAll`	`ForAllDeclaration`
`variableName`: FreeRank
`term_F_4_lhs`	`LiteralExpression`
`literalValue`: isClosed
`term_F_4_rhs`	`LiteralExpression`
`literalValue`: freeRank = 0 ⇔ pinnedCount = n
`term_F_4_forAll`	`ForAllDeclaration`
`variableName`: FreeRank
`term_FL_1_lhs`	`LiteralExpression`
`literalValue`: ⊥
`term_FL_1_rhs`	`LiteralExpression`
`literalValue`: all sites free (freeRank = n)
`term_FL_1_forAll`	`ForAllDeclaration`
`variableName`: FreeRank lattice
`term_FL_2_lhs`	`LiteralExpression`
`literalValue`: ⊤
`term_FL_2_rhs`	`LiteralExpression`
`literalValue`: all sites pinned (pinnedCount = n)
`term_FL_2_forAll`	`ForAllDeclaration`
`variableName`: FreeRank lattice
`term_FL_3_lhs`	`LiteralExpression`
`literalValue`: join(S₁, S₂)
`term_FL_3_rhs`	`LiteralExpression`
`literalValue`: union of pinnings from S₁ and S₂
`term_FL_3_forAll`	`ForAllDeclaration`
`variableName`: FreeRank states S₁, S₂
`term_FL_4_lhs`	`LiteralExpression`
`literalValue`: lattice height
`term_FL_4_rhs`	`LiteralExpression`
`literalValue`: n
`term_FL_4_forAll`	`ForAllDeclaration`
`variableName`: FreeRank lattice
`term_FPM_1_lhs`	`LiteralExpression`
`literalValue`: x ∈ Unit
`term_FPM_1_rhs`	`LiteralExpression`
`literalValue`: site_0(x) = 1 (x is odd)
`term_FPM_1_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_FPM_2_lhs`	`LiteralExpression`
`literalValue`: x ∈ Exterior
`term_FPM_2_rhs`	`LiteralExpression`
`literalValue`: x ∉ carrier(T)
`term_FPM_2_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n, type T
`term_FPM_3_lhs`	`LiteralExpression`
`literalValue`: x ∈ Irreducible
`term_FPM_3_rhs`	`LiteralExpression`
`literalValue`: x ∉ Unit ∪ Exterior AND no non-trivial factorization
`term_FPM_3_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_FPM_4_lhs`	`LiteralExpression`
`literalValue`: x ∈ Reducible
`term_FPM_4_rhs`	`LiteralExpression`
`literalValue`: x ∉ Unit ∪ Exterior ∪ Irreducible
`term_FPM_4_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_FPM_5_lhs`	`LiteralExpression`
`literalValue`: x = 2^{v(x)} ⋅ u
`term_FPM_5_rhs`	`LiteralExpression`
`literalValue`: u odd, v(x) = min position of 1-bit
`term_FPM_5_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_FPM_6_lhs`	`LiteralExpression`
`literalValue`: \|{x: v(x) = k}\|
`term_FPM_6_rhs`	`LiteralExpression`
`literalValue`: 2^{n−k−1} for 0 < k < n; 1 for k = n
`term_FPM_6_forAll`	`ForAllDeclaration`
`variableName`: R_n
`term_FPM_7_lhs`	`LiteralExpression`
`literalValue`: base type partition
`term_FPM_7_rhs`	`LiteralExpression`
`literalValue`: \|Unit\| = 2^{n−1}; \|Irr\| = 2^{n−2}; \|Red\| = 2^{n−2}
`term_FPM_7_forAll`	`ForAllDeclaration`
`variableName`: R_n, n ≥ 3
`term_FS_1_lhs`	`LiteralExpression`
`literalValue`: site_k(x)
`term_FS_1_rhs`	`LiteralExpression`
`literalValue`: (x >> k) AND 1
`term_FS_1_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n, 0 ≤ k < n
`term_FS_2_lhs`	`LiteralExpression`
`literalValue`: site_0(x)
`term_FS_2_rhs`	`LiteralExpression`
`literalValue`: x mod 2 (parity)
`term_FS_2_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_FS_3_lhs`	`LiteralExpression`
`literalValue`: site_k(x) given sites 0..k−1
`term_FS_3_rhs`	`LiteralExpression`
`literalValue`: determines x mod 2^{k+1}
`term_FS_3_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_FS_4_lhs`	`LiteralExpression`
`literalValue`: sites 0..k together
`term_FS_4_rhs`	`LiteralExpression`
`literalValue`: determine x mod 2^{k+1}
`term_FS_4_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_FS_5_lhs`	`LiteralExpression`
`literalValue`: all n sites
`term_FS_5_rhs`	`LiteralExpression`
`literalValue`: determine x uniquely
`term_FS_5_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_FS_6_lhs`	`LiteralExpression`
`literalValue`: stratum(x)
`term_FS_6_rhs`	`LiteralExpression`
`literalValue`: v_2(x) = min{k : site_k(x) = 1}
`term_FS_6_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_FS_7_lhs`	`LiteralExpression`
`literalValue`: depth(x)
`term_FS_7_rhs`	`LiteralExpression`
`literalValue`: ≤ v_2(x) for irreducible elements
`term_FS_7_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n, base type
`term_RE_1_lhs`	`LiteralExpression`
`literalValue`: Π_D(T)
`term_RE_1_rhs`	`LiteralExpression`
`literalValue`: Π_C(T) = Π_E(T)
`term_RE_1_forAll`	`ForAllDeclaration`
`variableName`: T ∈ T_n
`term_IR_1_lhs`	`LiteralExpression`
`literalValue`: pinnedCount(state_{i+1})
`term_IR_1_rhs`	`LiteralExpression`
`literalValue`: ≥ pinnedCount(state_i)
`term_IR_1_forAll`	`ForAllDeclaration`
`variableName`: resolution states
`term_IR_2_lhs`	`LiteralExpression`
`literalValue`: iterations to converge
`term_IR_2_rhs`	`LiteralExpression`
`literalValue`: ≤ n
`term_IR_2_forAll`	`ForAllDeclaration`
`variableName`: resolution loop
`term_IR_3_lhs`	`LiteralExpression`
`literalValue`: convergenceRate
`term_IR_3_rhs`	`LiteralExpression`
`literalValue`: pinnedCount / iterationCount
`term_IR_3_forAll`	`ForAllDeclaration`
`variableName`: ResolutionState
`term_IR_4_lhs`	`LiteralExpression`
`literalValue`: constraint set spans all sites
`term_IR_4_rhs`	`LiteralExpression`
`literalValue`: loop terminates
`term_IR_4_forAll`	`ForAllDeclaration`
`variableName`: complete constraint set
`term_SF_1_lhs`	`LiteralExpression`
`literalValue`: n ≡ 0 (mod ord_g(2))
`term_SF_1_rhs`	`LiteralExpression`
`literalValue`: factor g has optimal resolution at level n
`term_SF_1_forAll`	`ForAllDeclaration`
`variableName`: factor g, quantum n
`term_SF_2_lhs`	`LiteralExpression`
`literalValue`: constraints with smaller step_g
`term_SF_2_rhs`	`LiteralExpression`
`literalValue`: are more constraining, apply first
`term_SF_2_forAll`	`ForAllDeclaration`
`variableName`: constraint ordering
`term_RD_1_lhs`	`LiteralExpression`
`literalValue`: same type T and constraint sequence
`term_RD_1_rhs`	`LiteralExpression`
`literalValue`: unique resolved partition
`term_RD_1_forAll`	`ForAllDeclaration`
`variableName`: T ∈ T_n, [C₁,...,Cₖ]
`term_RD_2_lhs`	`LiteralExpression`
`literalValue`: complete constraint set, any order
`term_RD_2_rhs`	`LiteralExpression`
`literalValue`: same final partition
`term_RD_2_forAll`	`ForAllDeclaration`
`variableName`: closing constraint set
`term_SE_1_lhs`	`LiteralExpression`
`literalValue`: EvaluationResolver
`term_SE_1_rhs`	`LiteralExpression`
`literalValue`: directly computes set-theoretic partition
`term_SE_1_forAll`	`ForAllDeclaration`
`variableName`: T ∈ T_n
`term_SE_2_lhs`	`LiteralExpression`
`literalValue`: DihedralFactorizationResolver
`term_SE_2_rhs`	`LiteralExpression`
`literalValue`: orbit decomposition yields same partition
`term_SE_2_forAll`	`ForAllDeclaration`
`variableName`: T ∈ T_n
`term_SE_3_lhs`	`LiteralExpression`
`literalValue`: CanonicalFormResolver
`term_SE_3_rhs`	`LiteralExpression`
`literalValue`: confluent rewrite → same partition
`term_SE_3_forAll`	`ForAllDeclaration`
`variableName`: T ∈ T_n
`term_SE_4_lhs`	`LiteralExpression`
`literalValue`: Π_D(T) = Π_C(T) = Π_E(T)
`term_SE_4_rhs`	`LiteralExpression`
`literalValue`: all compute same set-theoretic partition
`term_SE_4_forAll`	`ForAllDeclaration`
`variableName`: T ∈ T_n
`term_OO_1_lhs`	`LiteralExpression`
`literalValue`: benefit(C_i, S)
`term_OO_1_rhs`	`LiteralExpression`
`literalValue`: \|pins(C_i) ∖ S\|
`term_OO_1_forAll`	`ForAllDeclaration`
`variableName`: constraint C_i, pinned set S
`term_OO_2_lhs`	`LiteralExpression`
`literalValue`: cost(C_i)
`term_OO_2_rhs`	`LiteralExpression`
`literalValue`: step_{m_i} or popcount(p_i)
`term_OO_2_forAll`	`ForAllDeclaration`
`variableName`: ResidueConstraint or CarryConstraint
`term_OO_3_lhs`	`LiteralExpression`
`literalValue`: greedy selection
`term_OO_3_rhs`	`LiteralExpression`
`literalValue`: argmax benefit(C_i, S) / cost(C_i)
`term_OO_3_forAll`	`ForAllDeclaration`
`variableName`: each resolution step
`term_OO_4_lhs`	`LiteralExpression`
`literalValue`: greedy approximation
`term_OO_4_rhs`	`LiteralExpression`
`literalValue`: (1 − 1/e) ≈ 63% of optimal
`term_OO_4_forAll`	`ForAllDeclaration`
`variableName`: weighted set cover
`term_OO_5_lhs`	`LiteralExpression`
`literalValue`: equal cost tiebreaker
`term_OO_5_rhs`	`LiteralExpression`
`literalValue`: prefer vertical (residue) before horizontal (carry)
`term_OO_5_forAll`	`ForAllDeclaration`
`variableName`: cost-tied constraints
`term_CB_1_lhs`	`LiteralExpression`
`literalValue`: min convergenceRate
`term_CB_1_rhs`	`LiteralExpression`
`literalValue`: 1 site per iteration
`term_CB_1_forAll`	`ForAllDeclaration`
`variableName`: worst case
`term_CB_2_lhs`	`LiteralExpression`
`literalValue`: max convergenceRate
`term_CB_2_rhs`	`LiteralExpression`
`literalValue`: n sites in 1 iteration
`term_CB_2_forAll`	`ForAllDeclaration`
`variableName`: best case
`term_CB_3_lhs`	`LiteralExpression`
`literalValue`: expected rate (residue)
`term_CB_3_rhs`	`LiteralExpression`
`literalValue`: ⌊log_2(m)⌋ sites per constraint
`term_CB_3_forAll`	`ForAllDeclaration`
`variableName`: ResidueConstraint(m, r)
`term_CB_4_lhs`	`LiteralExpression`
`literalValue`: convergenceRate < 1 for 2 iterations
`term_CB_4_rhs`	`LiteralExpression`
`literalValue`: constraint set may be insufficient
`term_CB_4_forAll`	`ForAllDeclaration`
`variableName`: stall detection
`term_CB_5_lhs`	`LiteralExpression`
`literalValue`: ∪_i pins(C_i) = {0,...,n−1}
`term_CB_5_rhs`	`LiteralExpression`
`literalValue`: constraint set closes budget
`term_CB_5_forAll`	`ForAllDeclaration`
`variableName`: sufficiency criterion
`term_CB_6_lhs`	`LiteralExpression`
`literalValue`: iterations for k constraints
`term_CB_6_rhs`	`LiteralExpression`
`literalValue`: ≤ min(k, n)
`term_CB_6_forAll`	`ForAllDeclaration`
`variableName`: well-formed model
`term_OB_M1_lhs`	`LiteralExpression`
`literalValue`: d_R(x, z)
`term_OB_M1_rhs`	`LiteralExpression`
`literalValue`: ≤ d_R(x, y) + d_R(y, z)
`term_OB_M1_forAll`	`ForAllDeclaration`
`variableName`: x, y, z ∈ R_n
`term_OB_M2_lhs`	`LiteralExpression`
`literalValue`: d_H(x, z)
`term_OB_M2_rhs`	`LiteralExpression`
`literalValue`: ≤ d_H(x, y) + d_H(y, z)
`term_OB_M2_forAll`	`ForAllDeclaration`
`variableName`: x, y, z ∈ R_n
`term_OB_M3_lhs`	`LiteralExpression`
`literalValue`: d_Δ(x, y)
`term_OB_M3_rhs`	`LiteralExpression`
`literalValue`: \|d_R(x, y) − d_H(x, y)\|
`term_OB_M3_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_OB_M4_lhs`	`LiteralExpression`
`literalValue`: d_R(neg(x), neg(y))
`term_OB_M4_rhs`	`LiteralExpression`
`literalValue`: d_R(x, y)
`term_OB_M4_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_OB_M5_lhs`	`LiteralExpression`
`literalValue`: d_H(bnot(x), bnot(y))
`term_OB_M5_rhs`	`LiteralExpression`
`literalValue`: d_H(x, y)
`term_OB_M5_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_OB_M6_lhs`	`LiteralExpression`
`literalValue`: d_R(succ(x), succ(y))
`term_OB_M6_rhs`	`LiteralExpression`
`literalValue`: d_R(x, y) but d_H may differ
`term_OB_M6_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_OB_C1_lhs`	`LiteralExpression`
`literalValue`: [neg, bnot](x)
`term_OB_C1_rhs`	`LiteralExpression`
`literalValue`: 2
`term_OB_C1_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_OB_C2_lhs`	`LiteralExpression`
`literalValue`: [neg, add(•,k)](x)
`term_OB_C2_rhs`	`LiteralExpression`
`literalValue`: −2k mod 2^n
`term_OB_C2_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n, constant k
`term_OB_C3_lhs`	`LiteralExpression`
`literalValue`: [bnot, xor(•,k)](x)
`term_OB_C3_rhs`	`LiteralExpression`
`literalValue`: 0
`term_OB_C3_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n, constant k
`term_OB_H1_lhs`	`LiteralExpression`
`literalValue`: closed additive path monodromy
`term_OB_H1_rhs`	`LiteralExpression`
`literalValue`: trivial (abelian ⇒ path-independent)
`term_OB_H1_forAll`	`ForAllDeclaration`
`variableName`: additive group
`term_OB_H2_lhs`	`LiteralExpression`
`literalValue`: closed {neg,bnot} path monodromy
`term_OB_H2_rhs`	`LiteralExpression`
`literalValue`: ∈ D_{2^n}
`term_OB_H2_forAll`	`ForAllDeclaration`
`variableName`: dihedral generators
`term_OB_H3_lhs`	`LiteralExpression`
`literalValue`: succ-only path WindingNumber
`term_OB_H3_rhs`	`LiteralExpression`
`literalValue`: path length / 2^n
`term_OB_H3_forAll`	`ForAllDeclaration`
`variableName`: closed succ path
`term_OB_P1_lhs`	`LiteralExpression`
`literalValue`: PathLength(p₁ ⋅ p₂)
`term_OB_P1_rhs`	`LiteralExpression`
`literalValue`: PathLength(p₁) + PathLength(p₂)
`term_OB_P1_forAll`	`ForAllDeclaration`
`variableName`: paths p₁, p₂
`term_OB_P2_lhs`	`LiteralExpression`
`literalValue`: TotalVariation(p₁ ⋅ p₂)
`term_OB_P2_rhs`	`LiteralExpression`
`literalValue`: ≤ TotalVariation(p₁) + TotalVariation(p₂)
`term_OB_P2_forAll`	`ForAllDeclaration`
`variableName`: paths p₁, p₂
`term_OB_P3_lhs`	`LiteralExpression`
`literalValue`: ReductionLength(c₁ ; c₂)
`term_OB_P3_rhs`	`LiteralExpression`
`literalValue`: ReductionLength(c₁) + ReductionLength(c₂)
`term_OB_P3_forAll`	`ForAllDeclaration`
`variableName`: reductions c₁, c₂
`term_CT_1_lhs`	`LiteralExpression`
`literalValue`: catastrophe boundaries
`term_CT_1_rhs`	`LiteralExpression`
`literalValue`: g = 2^k for 1 ≤ k ≤ n−1
`term_CT_1_forAll`	`ForAllDeclaration`
`variableName`: stratum transitions
`term_CT_2_lhs`	`LiteralExpression`
`literalValue`: odd prime catastrophe
`term_CT_2_rhs`	`LiteralExpression`
`literalValue`: ResidueConstraint(p, •) transitions visibility
`term_CT_2_forAll`	`ForAllDeclaration`
`variableName`: odd prime p
`term_CT_3_lhs`	`LiteralExpression`
`literalValue`: CatastropheThreshold(g)
`term_CT_3_rhs`	`LiteralExpression`
`literalValue`: step_g / n
`term_CT_3_forAll`	`ForAllDeclaration`
`variableName`: factor g
`term_CT_4_lhs`	`LiteralExpression`
`literalValue`: composite catastrophe g = p⋅q
`term_CT_4_rhs`	`LiteralExpression`
`literalValue`: max(step_p, step_q) / n
`term_CT_4_forAll`	`ForAllDeclaration`
`variableName`: composite g
`term_CF_1_lhs`	`LiteralExpression`
`literalValue`: CurvatureFlux(γ)
`term_CF_1_rhs`	`LiteralExpression`
`literalValue`: Σ \|d_R(x_i, x_{i+1}) − d_H(x_i, x_{i+1})\|
`term_CF_1_forAll`	`ForAllDeclaration`
`variableName`: path γ
`term_CF_2_lhs`	`LiteralExpression`
`literalValue`: ResolutionCost(T)
`term_CF_2_rhs`	`LiteralExpression`
`literalValue`: ≥ CurvatureFlux(γ_opt)
`term_CF_2_forAll`	`ForAllDeclaration`
`variableName`: type T
`term_CF_3_lhs`	`LiteralExpression`
`literalValue`: CurvatureFlux(x, succ(x))
`term_CF_3_rhs`	`LiteralExpression`
`literalValue`: trailing_ones(x) for t < n; n−1 for x = 2^n−1
`term_CF_3_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_CF_4_lhs`	`LiteralExpression`
`literalValue`: Σ_{x ∈ R_n} CurvatureFlux(x, succ(x))
`term_CF_4_rhs`	`LiteralExpression`
`literalValue`: 2^n − 2
`term_CF_4_forAll`	`ForAllDeclaration`
`variableName`: n ≥ 1
`term_HG_1_lhs`	`LiteralExpression`
`literalValue`: additive holonomy
`term_HG_1_rhs`	`LiteralExpression`
`literalValue`: trivial (abelian ⇒ path-independent)
`term_HG_1_forAll`	`ForAllDeclaration`
`variableName`: additive group
`term_HG_2_lhs`	`LiteralExpression`
`literalValue`: {neg, bnot, succ, pred} holonomy
`term_HG_2_rhs`	`LiteralExpression`
`literalValue`: D_{2^n}
`term_HG_2_forAll`	`ForAllDeclaration`
`variableName`: dihedral generators
`term_HG_3_lhs`	`LiteralExpression`
`literalValue`: {mul(•, u) : u ∈ R_n×} holonomy
`term_HG_3_rhs`	`LiteralExpression`
`literalValue`: R_n× ≅ Z/2 × Z/2^{n−2}
`term_HG_3_forAll`	`ForAllDeclaration`
`variableName`: unit group
`term_HG_4_lhs`	`LiteralExpression`
`literalValue`: Hol(R_n)
`term_HG_4_rhs`	`LiteralExpression`
`literalValue`: Aff(R_n) = R_n× ⋉ R_n
`term_HG_4_forAll`	`ForAllDeclaration`
`variableName`: n ≥ 1
`term_HG_5_lhs`	`LiteralExpression`
`literalValue`: Hol(R_n) decomposition
`term_HG_5_rhs`	`LiteralExpression`
`literalValue`: D_{2^n} ⋅ {mul(•,u) : u ∈ R_n×, u ≠ ±1}
`term_HG_5_forAll`	`ForAllDeclaration`
`variableName`: n ≥ 1
`term_T_C1_lhs`	`LiteralExpression`
`literalValue`: compose(id, f)
`term_T_C1_rhs`	`LiteralExpression`
`literalValue`: f
`term_T_C1_forAll`	`ForAllDeclaration`
`variableName`: f ∈ Transform
`term_T_C2_lhs`	`LiteralExpression`
`literalValue`: compose(f, id)
`term_T_C2_rhs`	`LiteralExpression`
`literalValue`: f
`term_T_C2_forAll`	`ForAllDeclaration`
`variableName`: f ∈ Transform
`term_T_C3_lhs`	`LiteralExpression`
`literalValue`: compose(f, compose(g, h))
`term_T_C3_rhs`	`LiteralExpression`
`literalValue`: compose(compose(f, g), h)
`term_T_C3_forAll`	`ForAllDeclaration`
`variableName`: f, g, h ∈ Transform
`term_T_C4_lhs`	`LiteralExpression`
`literalValue`: f composesWith g
`term_T_C4_rhs`	`LiteralExpression`
`literalValue`: target(f) = source(g)
`term_T_C4_forAll`	`ForAllDeclaration`
`variableName`: f, g ∈ Transform
`term_T_I1_lhs`	`LiteralExpression`
`literalValue`: d_R(neg(x), neg(y))
`term_T_I1_rhs`	`LiteralExpression`
`literalValue`: d_R(x, y)
`term_T_I1_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_T_I2_lhs`	`LiteralExpression`
`literalValue`: d_H(bnot(x), bnot(y))
`term_T_I2_rhs`	`LiteralExpression`
`literalValue`: d_H(x, y)
`term_T_I2_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_T_I3_lhs`	`LiteralExpression`
`literalValue`: succ = neg ∘ bnot
`term_T_I3_rhs`	`LiteralExpression`
`literalValue`: preserves d_R but not d_H
`term_T_I3_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_T_I4_lhs`	`LiteralExpression`
`literalValue`: ring isometries
`term_T_I4_rhs`	`LiteralExpression`
`literalValue`: form a group under composition
`term_T_I4_forAll`	`ForAllDeclaration`
`variableName`: Isometry
`term_T_I5_lhs`	`LiteralExpression`
`literalValue`: CurvatureObservable
`term_T_I5_rhs`	`LiteralExpression`
`literalValue`: measures failure of ring isometry to be Hamming isometry
`term_T_I5_forAll`	`ForAllDeclaration`
`variableName`: Isometry
`term_T_E1_lhs`	`LiteralExpression`
`literalValue`: ι(x) = ι(y)
`term_T_E1_rhs`	`LiteralExpression`
`literalValue`: x = y
`term_T_E1_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n (injectivity)
`term_T_E2_lhs`	`LiteralExpression`
`literalValue`: ι(add(x,y))
`term_T_E2_rhs`	`LiteralExpression`
`literalValue`: add(ι(x), ι(y)); ι(mul(x,y)) = mul(ι(x), ι(y))
`term_T_E2_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_T_E3_lhs`	`LiteralExpression`
`literalValue`: ι₂ ∘ ι₁ : R_n → R_k
`term_T_E3_rhs`	`LiteralExpression`
`literalValue`: is an embedding (transitivity)
`term_T_E3_forAll`	`ForAllDeclaration`
`variableName`: ι₁: R_n → R_m, ι₂: R_m → R_k
`term_T_E4_lhs`	`LiteralExpression`
`literalValue`: glyph ∘ ι ∘ addresses
`term_T_E4_rhs`	`LiteralExpression`
`literalValue`: well-defined
`term_T_E4_forAll`	`ForAllDeclaration`
`variableName`: embedding ι
`term_T_A1_lhs`	`LiteralExpression`
`literalValue`: g ∈ D_{2^n} on Constraint C
`term_T_A1_rhs`	`LiteralExpression`
`literalValue`: g⋅C (transformed constraint)
`term_T_A1_forAll`	`ForAllDeclaration`
`variableName`: g ∈ D_{2^n}, C ∈ Constraint
`term_T_A2_lhs`	`LiteralExpression`
`literalValue`: g ∈ D_{2^n} on Partition
`term_T_A2_rhs`	`LiteralExpression`
`literalValue`: permutes components
`term_T_A2_forAll`	`ForAllDeclaration`
`variableName`: g ∈ D_{2^n}
`term_T_A3_lhs`	`LiteralExpression`
`literalValue`: D_{2^n} orbits on R_n
`term_T_A3_rhs`	`LiteralExpression`
`literalValue`: determine irreducibility boundaries
`term_T_A3_forAll`	`ForAllDeclaration`
`variableName`: DihedralFactorizationResolver
`term_T_A4_lhs`	`LiteralExpression`
`literalValue`: fixed points of neg
`term_T_A4_rhs`	`LiteralExpression`
`literalValue`: {0, 2^{n−1}}; bnot has none (n > 0)
`term_T_A4_forAll`	`ForAllDeclaration`
`variableName`: R_n
`term_AU_1_lhs`	`LiteralExpression`
`literalValue`: Aut(R_n)
`term_AU_1_rhs`	`LiteralExpression`
`literalValue`: {μ_u : x ↦ mul(u, x) \| u ∈ R_n×}
`term_AU_1_forAll`	`ForAllDeclaration`
`variableName`: n ≥ 1
`term_AU_2_lhs`	`LiteralExpression`
`literalValue`: Aut(R_n)
`term_AU_2_rhs`	`LiteralExpression`
`literalValue`: ≅ R_n× ≅ Z/2 × Z/2^{n−2}
`term_AU_2_forAll`	`ForAllDeclaration`
`variableName`: n ≥ 3
`term_AU_3_lhs`	`LiteralExpression`
`literalValue`: \|Aut(R_n)\|
`term_AU_3_rhs`	`LiteralExpression`
`literalValue`: 2^{n−1}
`term_AU_3_forAll`	`ForAllDeclaration`
`variableName`: n ≥ 1
`term_AU_4_lhs`	`LiteralExpression`
`literalValue`: Aut(R_n) ∩ D_{2^n}
`term_AU_4_rhs`	`LiteralExpression`
`literalValue`: {id, neg}
`term_AU_4_forAll`	`ForAllDeclaration`
`variableName`: n ≥ 1
`term_AU_5_lhs`	`LiteralExpression`
`literalValue`: Aff(R_n)
`term_AU_5_rhs`	`LiteralExpression`
`literalValue`: ⟨D_{2^n}, μ_3⟩
`term_AU_5_forAll`	`ForAllDeclaration`
`variableName`: n ≥ 1
`term_EF_1_lhs`	`LiteralExpression`
`literalValue`: F_ι(f)
`term_EF_1_rhs`	`LiteralExpression`
`literalValue`: ι ∘ f ∘ ι⁻¹ on Im(ι)
`term_EF_1_forAll`	`ForAllDeclaration`
`variableName`: ι: R_n → R_m, f ∈ Cat(R_n)
`term_EF_2_lhs`	`LiteralExpression`
`literalValue`: F_ι(f ∘ g)
`term_EF_2_rhs`	`LiteralExpression`
`literalValue`: F_ι(f) ∘ F_ι(g)
`term_EF_2_forAll`	`ForAllDeclaration`
`variableName`: ι: R_n → R_m
`term_EF_3_lhs`	`LiteralExpression`
`literalValue`: F_ι(id_{R_n})
`term_EF_3_rhs`	`LiteralExpression`
`literalValue`: id_{Im(ι)}
`term_EF_3_forAll`	`ForAllDeclaration`
`variableName`: ι: R_n → R_m
`term_EF_4_lhs`	`LiteralExpression`
`literalValue`: F_{ι₂ ∘ ι₁}
`term_EF_4_rhs`	`LiteralExpression`
`literalValue`: F_{ι₂} ∘ F_{ι₁}
`term_EF_4_forAll`	`ForAllDeclaration`
`variableName`: ι₁: R_n → R_m, ι₂: R_m → R_k
`term_EF_5_lhs`	`LiteralExpression`
`literalValue`: F_ι(ring isometry)
`term_EF_5_rhs`	`LiteralExpression`
`literalValue`: ring isometry at level m
`term_EF_5_forAll`	`ForAllDeclaration`
`variableName`: ι: R_n → R_m
`term_EF_6_lhs`	`LiteralExpression`
`literalValue`: F_ι(D_{2^n})
`term_EF_6_rhs`	`LiteralExpression`
`literalValue`: ⊆ D_{2^m} as subgroup
`term_EF_6_forAll`	`ForAllDeclaration`
`variableName`: ι: R_n → R_m
`term_EF_7_lhs`	`LiteralExpression`
`literalValue`: F_ι(R_n×)
`term_EF_7_rhs`	`LiteralExpression`
`literalValue`: ⊆ R_m× as subgroup
`term_EF_7_forAll`	`ForAllDeclaration`
`variableName`: ι: R_n → R_m
`term_AA_1_lhs`	`LiteralExpression`
`literalValue`: glyph(x)
`term_AA_1_rhs`	`LiteralExpression`
`literalValue`: [braille(x[0:5]), braille(x[6:11]), ...]
`term_AA_1_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n (6-bit blocks)
`term_AA_2_lhs`	`LiteralExpression`
`literalValue`: braille(a ⊕ b)
`term_AA_2_rhs`	`LiteralExpression`
`literalValue`: braille(a) ⊕ braille(b)
`term_AA_2_forAll`	`ForAllDeclaration`
`variableName`: a, b ∈ {0,1}^6
`term_AA_3_lhs`	`LiteralExpression`
`literalValue`: glyph(bnot(x))
`term_AA_3_rhs`	`LiteralExpression`
`literalValue`: complement each Braille character of glyph(x)
`term_AA_3_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_AA_4_lhs`	`LiteralExpression`
`literalValue`: glyph(add(x, y))
`term_AA_4_rhs`	`LiteralExpression`
`literalValue`: ≠ f(glyph(x), glyph(y)) in general
`term_AA_4_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_AA_5_lhs`	`LiteralExpression`
`literalValue`: liftable operations
`term_AA_5_rhs`	`LiteralExpression`
`literalValue`: {xor, and, or, bnot}; NOT {add, sub, mul, neg, succ, pred}
`term_AA_5_forAll`	`ForAllDeclaration`
`variableName`: operations on R_n
`term_AA_6_lhs`	`LiteralExpression`
`literalValue`: neg(x) = succ(bnot(x))
`term_AA_6_rhs`	`LiteralExpression`
`literalValue`: bnot lifts, succ does not
`term_AA_6_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_AM_1_lhs`	`LiteralExpression`
`literalValue`: d_addr(a, b)
`term_AM_1_rhs`	`LiteralExpression`
`literalValue`: Σ_i popcount(braille_i(a) ⊕ braille_i(b))
`term_AM_1_forAll`	`ForAllDeclaration`
`variableName`: addresses a, b
`term_AM_2_lhs`	`LiteralExpression`
`literalValue`: d_addr(glyph(x), glyph(y))
`term_AM_2_rhs`	`LiteralExpression`
`literalValue`: d_H(x, y)
`term_AM_2_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_AM_3_lhs`	`LiteralExpression`
`literalValue`: d_addr
`term_AM_3_rhs`	`LiteralExpression`
`literalValue`: does NOT preserve d_R in general
`term_AM_3_forAll`	`ForAllDeclaration`
`variableName`: addresses
`term_AM_4_lhs`	`LiteralExpression`
`literalValue`: d_Δ(x, y)
`term_AM_4_rhs`	`LiteralExpression`
`literalValue`: \|d_R(x,y) − d_addr(glyph(x), glyph(y))\|
`term_AM_4_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_TH_1_lhs`	`LiteralExpression`
`literalValue`: S(state)
`term_TH_1_rhs`	`LiteralExpression`
`literalValue`: freeRank × ln 2
`term_TH_1_forAll`	`ForAllDeclaration`
`variableName`: state ∈ FreeRank
`term_TH_2_lhs`	`LiteralExpression`
`literalValue`: S(⊥)
`term_TH_2_rhs`	`LiteralExpression`
`literalValue`: n × ln 2
`term_TH_2_forAll`	`ForAllDeclaration`
`variableName`: unconstrained type
`term_TH_3_lhs`	`LiteralExpression`
`literalValue`: S(⊤)
`term_TH_3_rhs`	`LiteralExpression`
`literalValue`: 0
`term_TH_3_forAll`	`ForAllDeclaration`
`variableName`: fully resolved type
`term_TH_4_lhs`	`LiteralExpression`
`literalValue`: total resolution cost
`term_TH_4_rhs`	`LiteralExpression`
`literalValue`: n × k_B T × ln 2
`term_TH_4_forAll`	`ForAllDeclaration`
`variableName`: Landauer bound
`term_TH_5_lhs`	`LiteralExpression`
`literalValue`: β*
`term_TH_5_rhs`	`LiteralExpression`
`literalValue`: ln 2
`term_TH_5_forAll`	`ForAllDeclaration`
`variableName`: UOR site system
`term_TH_6_lhs`	`LiteralExpression`
`literalValue`: constraint application
`term_TH_6_rhs`	`LiteralExpression`
`literalValue`: removes entropy; convergenceRate = cooling rate
`term_TH_6_forAll`	`ForAllDeclaration`
`variableName`: resolution loop
`term_TH_7_lhs`	`LiteralExpression`
`literalValue`: CatastropheThreshold
`term_TH_7_rhs`	`LiteralExpression`
`literalValue`: temperature of partition phase transition
`term_TH_7_forAll`	`ForAllDeclaration`
`variableName`: partition bifurcation
`term_TH_8_lhs`	`LiteralExpression`
`literalValue`: step_g
`term_TH_8_rhs`	`LiteralExpression`
`literalValue`: free-energy cost of constraint boundary
`term_TH_8_forAll`	`ForAllDeclaration`
`variableName`: constraint boundary g
`term_TH_9_lhs`	`LiteralExpression`
`literalValue`: computational hardness
`term_TH_9_rhs`	`LiteralExpression`
`literalValue`: type incompleteness (high temperature)
`term_TH_9_forAll`	`ForAllDeclaration`
`variableName`: type specification
`term_TH_10_lhs`	`LiteralExpression`
`literalValue`: type resolution
`term_TH_10_rhs`	`LiteralExpression`
`literalValue`: measurement; cost ≥ entropy removed
`term_TH_10_forAll`	`ForAllDeclaration`
`variableName`: resolution process
`term_AR_1_lhs`	`LiteralExpression`
`literalValue`: adiabatic schedule
`term_AR_1_rhs`	`LiteralExpression`
`literalValue`: decreasing freeRank × cost-per-site order
`term_AR_1_forAll`	`ForAllDeclaration`
`variableName`: constraint ordering
`term_AR_2_lhs`	`LiteralExpression`
`literalValue`: Cost_adiabatic
`term_AR_2_rhs`	`LiteralExpression`
`literalValue`: Σ_i cost(C_{σ(i)}) where σ is optimal
`term_AR_2_forAll`	`ForAllDeclaration`
`variableName`: optimal ordering
`term_AR_3_lhs`	`LiteralExpression`
`literalValue`: Cost_adiabatic
`term_AR_3_rhs`	`LiteralExpression`
`literalValue`: ≥ n × k_B T × ln 2
`term_AR_3_forAll`	`ForAllDeclaration`
`variableName`: Landauer bound
`term_AR_4_lhs`	`LiteralExpression`
`literalValue`: η = (n × ln 2) / Cost_adiabatic
`term_AR_4_rhs`	`LiteralExpression`
`literalValue`: ≤ 1
`term_AR_4_forAll`	`ForAllDeclaration`
`variableName`: adiabatic efficiency
`term_AR_5_lhs`	`LiteralExpression`
`literalValue`: greedy vs adiabatic difference
`term_AR_5_rhs`	`LiteralExpression`
`literalValue`: ≤ 5% for n ≤ 16
`term_AR_5_forAll`	`ForAllDeclaration`
`variableName`: empirical, Q0–Q4
`term_PD_1_lhs`	`LiteralExpression`
`literalValue`: phase space
`term_PD_1_rhs`	`LiteralExpression`
`literalValue`: {(n, g) : n ∈ Z₊, g constraint boundary}
`term_PD_1_forAll`	`ForAllDeclaration`
`variableName`: UOR phase diagram
`term_PD_2_lhs`	`LiteralExpression`
`literalValue`: phase boundaries
`term_PD_2_rhs`	`LiteralExpression`
`literalValue`: g \| (2^n − 1) or g = 2^k
`term_PD_2_forAll`	`ForAllDeclaration`
`variableName`: (n, g) plane
`term_PD_3_lhs`	`LiteralExpression`
`literalValue`: parity boundary
`term_PD_3_rhs`	`LiteralExpression`
`literalValue`: \|Unit\| = 2^{n−1}, \|non-Unit\| = 2^{n−1}
`term_PD_3_forAll`	`ForAllDeclaration`
`variableName`: g = 2
`term_PD_4_lhs`	`LiteralExpression`
`literalValue`: resonance lines
`term_PD_4_rhs`	`LiteralExpression`
`literalValue`: n = k ⋅ ord_g(2)
`term_PD_4_forAll`	`ForAllDeclaration`
`variableName`: (n, g) plane
`term_PD_5_lhs`	`LiteralExpression`
`literalValue`: phase count at level n
`term_PD_5_rhs`	`LiteralExpression`
`literalValue`: ≤ 2^n (typical O(n))
`term_PD_5_forAll`	`ForAllDeclaration`
`variableName`: quantum level n
`term_RC_1_lhs`	`LiteralExpression`
`literalValue`: reversible pinning of site k
`term_RC_1_rhs`	`LiteralExpression`
`literalValue`: store prior state in ancilla site k'
`term_RC_1_forAll`	`ForAllDeclaration`
`variableName`: SiteIndex k
`term_RC_2_lhs`	`LiteralExpression`
`literalValue`: reversible pinning entropy
`term_RC_2_rhs`	`LiteralExpression`
`literalValue`: ΔS_total = 0
`term_RC_2_forAll`	`ForAllDeclaration`
`variableName`: reversible strategy
`term_RC_3_lhs`	`LiteralExpression`
`literalValue`: deferred Landauer cost
`term_RC_3_rhs`	`LiteralExpression`
`literalValue`: n × k_B T × ln 2 at ancilla erasure
`term_RC_3_forAll`	`ForAllDeclaration`
`variableName`: ancilla cleanup
`term_RC_4_lhs`	`LiteralExpression`
`literalValue`: reversible total cost
`term_RC_4_rhs`	`LiteralExpression`
`literalValue`: = irreversible total cost (redistributed)
`term_RC_4_forAll`	`ForAllDeclaration`
`variableName`: reversible strategy
`term_RC_5_lhs`	`LiteralExpression`
`literalValue`: quantum UOR
`term_RC_5_rhs`	`LiteralExpression`
`literalValue`: superposed sites, cost ∝ winning path
`term_RC_5_forAll`	`ForAllDeclaration`
`variableName`: hypothetical quantum
`term_DC_1_lhs`	`LiteralExpression`
`literalValue`: ∂_R f(x)
`term_DC_1_rhs`	`LiteralExpression`
`literalValue`: f(succ(x)) - f(x)
`term_DC_1_forAll`	`ForAllDeclaration`
`variableName`: f : R_n → R_n, x ∈ R_n
`term_DC_2_lhs`	`LiteralExpression`
`literalValue`: ∂_H f(x)
`term_DC_2_rhs`	`LiteralExpression`
`literalValue`: f(bnot(x)) - f(x)
`term_DC_2_forAll`	`ForAllDeclaration`
`variableName`: f : R_n → R_n, x ∈ R_n
`term_DC_3_lhs`	`LiteralExpression`
`literalValue`: ∂_H id(x)
`term_DC_3_rhs`	`LiteralExpression`
`literalValue`: bnot(x) - x = -(2x + 1) mod 2^n
`term_DC_3_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_DC_4_lhs`	`LiteralExpression`
`literalValue`: [neg, bnot](x)
`term_DC_4_rhs`	`LiteralExpression`
`literalValue`: ∂_R neg(x) - ∂_H neg(x)
`term_DC_4_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_DC_5_lhs`	`LiteralExpression`
`literalValue`: ∂_R f - ∂_H f
`term_DC_5_rhs`	`LiteralExpression`
`literalValue`: Σ carry contributions
`term_DC_5_forAll`	`ForAllDeclaration`
`variableName`: f : R_n → R_n
`term_DC_6_lhs`	`LiteralExpression`
`literalValue`: J_k(x)
`term_DC_6_rhs`	`LiteralExpression`
`literalValue`: ∂_R f_k(x) where f_k = site_k
`term_DC_6_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n, 0 ≤ k < n
`term_DC_7_lhs`	`LiteralExpression`
`literalValue`: J_{n-1}(x)
`term_DC_7_rhs`	`LiteralExpression`
`literalValue`: may differ from lower sites
`term_DC_7_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_DC_8_lhs`	`LiteralExpression`
`literalValue`: rank(J(x))
`term_DC_8_rhs`	`LiteralExpression`
`literalValue`: = d_H(x, succ(x)) - 1 for generic x
`term_DC_8_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_DC_9_lhs`	`LiteralExpression`
`literalValue`: κ(x)
`term_DC_9_rhs`	`LiteralExpression`
`literalValue`: Σ_k J_k(x)
`term_DC_9_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n
`term_DC_10_lhs`	`LiteralExpression`
`literalValue`: optimal next constraint
`term_DC_10_rhs`	`LiteralExpression`
`literalValue`: argmax J_k over free sites
`term_DC_10_forAll`	`ForAllDeclaration`
`variableName`: resolution step
`term_DC_11_lhs`	`LiteralExpression`
`literalValue`: Σ_{x} J_k(x)
`term_DC_11_rhs`	`LiteralExpression`
`literalValue`: ≈ (2^n - 2)/n for each k
`term_DC_11_forAll`	`ForAllDeclaration`
`variableName`: 0 ≤ k < n
`term_HA_1_lhs`	`LiteralExpression`
`literalValue`: N(C)
`term_HA_1_rhs`	`LiteralExpression`
`literalValue`: simplicial complex on constraints
`term_HA_1_forAll`	`ForAllDeclaration`
`variableName`: constraint set C
`term_HA_2_lhs`	`LiteralExpression`
`literalValue`: resolution stalls
`term_HA_2_rhs`	`LiteralExpression`
`literalValue`: ⟺ H_k(N(C)) ≠ 0 for some k > 0
`term_HA_2_forAll`	`ForAllDeclaration`
`variableName`: constraint set C
`term_HA_3_lhs`	`LiteralExpression`
`literalValue`: S_residual
`term_HA_3_rhs`	`LiteralExpression`
`literalValue`: ≥ Σ_k β_k × ln 2
`term_HA_3_forAll`	`ForAllDeclaration`
`variableName`: constraint configuration C
`term_IT_2_lhs`	`LiteralExpression`
`literalValue`: χ(N(C))
`term_IT_2_rhs`	`LiteralExpression`
`literalValue`: Σ_k (-1)^k β_k
`term_IT_2_forAll`	`ForAllDeclaration`
`variableName`: constraint nerve N(C)
`term_IT_3_lhs`	`LiteralExpression`
`literalValue`: χ(N(C))
`term_IT_3_rhs`	`LiteralExpression`
`literalValue`: Σ_k (-1)^k dim(H_k)
`term_IT_3_forAll`	`ForAllDeclaration`
`variableName`: constraint nerve N(C)
`term_IT_6_lhs`	`LiteralExpression`
`literalValue`: λ_1(N(C))
`term_IT_6_rhs`	`LiteralExpression`
`literalValue`: lower bounds convergence rate
`term_IT_6_forAll`	`ForAllDeclaration`
`variableName`: constraint nerve N(C)
`term_IT_7a_lhs`	`LiteralExpression`
`literalValue`: Σ κ_k - χ(N(C))
`term_IT_7a_rhs`	`LiteralExpression`
`literalValue`: = S_residual / ln 2
`term_IT_7a_forAll`	`ForAllDeclaration`
`variableName`: constraint configuration C
`term_IT_7b_lhs`	`LiteralExpression`
`literalValue`: S_residual
`term_IT_7b_rhs`	`LiteralExpression`
`literalValue`: = (Σ κ_k - χ) × ln 2
`term_IT_7b_forAll`	`ForAllDeclaration`
`variableName`: constraint configuration C
`term_IT_7c_lhs`	`LiteralExpression`
`literalValue`: resolution cost
`term_IT_7c_rhs`	`LiteralExpression`
`literalValue`: ≥ n - χ(N(C))
`term_IT_7c_forAll`	`ForAllDeclaration`
`variableName`: constraint configuration C
`term_IT_7d_lhs`	`LiteralExpression`
`literalValue`: resolution complete
`term_IT_7d_rhs`	`LiteralExpression`
`literalValue`: ⟺ χ(N(C)) = n and all β_k = 0
`term_IT_7d_forAll`	`ForAllDeclaration`
`variableName`: constraint nerve N(C)
`term_phi_1_lhs`	`LiteralExpression`
`literalValue`: φ₁(neg, ResidueConstraint(m,r))
`term_phi_1_rhs`	`LiteralExpression`
`literalValue`: ResidueConstraint(m, m-r)
`term_phi_1_forAll`	`ForAllDeclaration`
`variableName`: ring op, constraint
`term_phi_2_lhs`	`LiteralExpression`
`literalValue`: φ₂(compose(A,B))
`term_phi_2_rhs`	`LiteralExpression`
`literalValue`: φ₂(A) ∪ φ₂(B)
`term_phi_2_forAll`	`ForAllDeclaration`
`variableName`: constraints A, B
`term_phi_3_lhs`	`LiteralExpression`
`literalValue`: φ₃(closed site state)
`term_phi_3_rhs`	`LiteralExpression`
`literalValue`: unique 4-component partition
`term_phi_3_forAll`	`ForAllDeclaration`
`variableName`: closed FreeRank
`term_phi_4_lhs`	`LiteralExpression`
`literalValue`: φ₄(T, x)
`term_phi_4_rhs`	`LiteralExpression`
`literalValue`: φ₃(φ₂(φ₁(T, x)))
`term_phi_4_forAll`	`ForAllDeclaration`
`variableName`: T ∈ T_n, x ∈ R_n
`term_phi_5_lhs`	`LiteralExpression`
`literalValue`: φ₅(neg)
`term_phi_5_rhs`	`LiteralExpression`
`literalValue`: preserves d_R, may change d_H
`term_phi_5_forAll`	`ForAllDeclaration`
`variableName`: op ∈ Operation
`term_phi_6_lhs`	`LiteralExpression`
`literalValue`: φ₆(state, observables)
`term_phi_6_rhs`	`LiteralExpression`
`literalValue`: RefinementSuggestion
`term_phi_6_forAll`	`ForAllDeclaration`
`variableName`: ResolutionState
`term_psi_1_lhs`	`LiteralExpression`
`literalValue`: N(constraints)
`term_psi_1_rhs`	`LiteralExpression`
`literalValue`: SimplicialComplex
`term_psi_1_forAll`	`ForAllDeclaration`
`variableName`: constraint set
`term_psi_2_lhs`	`LiteralExpression`
`literalValue`: C(K)
`term_psi_2_rhs`	`LiteralExpression`
`literalValue`: ChainComplex
`term_psi_2_forAll`	`ForAllDeclaration`
`variableName`: simplicial complex K
`term_psi_3_lhs`	`LiteralExpression`
`literalValue`: H_k(C)
`term_psi_3_rhs`	`LiteralExpression`
`literalValue`: ker(∂_k) / im(∂_{k+1})
`term_psi_3_forAll`	`ForAllDeclaration`
`variableName`: chain complex C
`term_psi_5_lhs`	`LiteralExpression`
`literalValue`: C^k
`term_psi_5_rhs`	`LiteralExpression`
`literalValue`: Hom(C_k, R)
`term_psi_5_forAll`	`ForAllDeclaration`
`variableName`: chain complex C, ring R
`term_psi_6_lhs`	`LiteralExpression`
`literalValue`: H^k(C)
`term_psi_6_rhs`	`LiteralExpression`
`literalValue`: ker(δ^k) / im(δ^{k-1})
`term_psi_6_forAll`	`ForAllDeclaration`
`variableName`: cochain complex C
`term_surfaceSymmetry_lhs`	`LiteralExpression`
`literalValue`: P(Π(G(s)))
`term_surfaceSymmetry_rhs`	`LiteralExpression`
`literalValue`: s' where type(s') ≡ type(s) under F.constraint
`term_surfaceSymmetry_forAll`	`ForAllDeclaration`
`variableName`: G: GroundingMap, P: ProjectionMap, F: Frame, s: Literal, G.symbolConstraints = P.projectionOrder
`term_CC_1_lhs`	`LiteralExpression`
`literalValue`: resolution(x, T)
`term_CC_1_rhs`	`LiteralExpression`
`literalValue`: O(1) for CompleteType T
`term_CC_1_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n, T: CompleteType
`term_CC_2_lhs`	`LiteralExpression`
`literalValue`: completeness(T)
`term_CC_2_rhs`	`LiteralExpression`
`literalValue`: implies completeness(T')
`term_CC_2_forAll`	`ForAllDeclaration`
`variableName`: T, T': ConstrainedType, T ⊆ T'
`term_CC_3_lhs`	`LiteralExpression`
`literalValue`: sitesClosed(W₁) + sitesClosed(W₂)
`term_CC_3_rhs`	`LiteralExpression`
`literalValue`: = n for valid concat(W₁, W₂)
`term_CC_3_forAll`	`ForAllDeclaration`
`variableName`: W₁, W₂: CompletenessWitness
`term_CC_4_lhs`	`LiteralExpression`
`literalValue`: CompletenessResolver
`term_CC_4_rhs`	`LiteralExpression`
`literalValue`: fix(ψ-pipeline, CompletenessCandidate)
`term_CC_4_forAll`	`ForAllDeclaration`
`variableName`: CompletenessCandidate
`term_CC_5_lhs`	`LiteralExpression`
`literalValue`: cert.verified = true
`term_CC_5_rhs`	`LiteralExpression`
`literalValue`: implies χ(N(C)) = n ∧ ∀k: β_k = 0
`term_CC_5_forAll`	`ForAllDeclaration`
`variableName`: cert: CompletenessCertificate
`term_QL_1_lhs`	`LiteralExpression`
`literalValue`: neg(bnot(x))
`term_QL_1_rhs`	`LiteralExpression`
`literalValue`: succ(x) in Z/(2ⁿ)Z
`term_QL_1_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n, n ≥ 1
`term_QL_2_lhs`	`LiteralExpression`
`literalValue`: \|D_{2ⁿ}\|
`term_QL_2_rhs`	`LiteralExpression`
`literalValue`: 2ⁿ⁺¹ for all n ≥ 1
`term_QL_2_forAll`	`ForAllDeclaration`
`variableName`: n ≥ 1
`term_QL_3_lhs`	`LiteralExpression`
`literalValue`: P(j) = 2^{-j}
`term_QL_3_rhs`	`LiteralExpression`
`literalValue`: Boltzmann distribution at β* = ln 2, all n ≥ 1
`term_QL_3_forAll`	`ForAllDeclaration`
`variableName`: j ∈ R_n, n ≥ 1
`term_QL_4_lhs`	`LiteralExpression`
`literalValue`: siteBudget(PrimitiveType, n)
`term_QL_4_rhs`	`LiteralExpression`
`literalValue`: = n (one site per bit)
`term_QL_4_forAll`	`ForAllDeclaration`
`variableName`: PrimitiveType, n ≥ 1
`term_QL_5_lhs`	`LiteralExpression`
`literalValue`: resolution(CompleteType, n)
`term_QL_5_rhs`	`LiteralExpression`
`literalValue`: O(1) for all n ≥ 1
`term_QL_5_forAll`	`ForAllDeclaration`
`variableName`: CompleteType, n ≥ 1
`term_QL_6_lhs`	`LiteralExpression`
`literalValue`: contentAddress(x, n)
`term_QL_6_rhs`	`LiteralExpression`
`literalValue`: bijection for all n ≥ 1
`term_QL_6_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n, n ≥ 1
`term_QL_7_lhs`	`LiteralExpression`
`literalValue`: ψ-pipeline(ConstrainedType, n)
`term_QL_7_rhs`	`LiteralExpression`
`literalValue`: valid ChainComplex for all n ≥ 1
`term_QL_7_forAll`	`ForAllDeclaration`
`variableName`: ConstrainedType, n ≥ 1
`term_GR_1_lhs`	`LiteralExpression`
`literalValue`: freeRank(B_{i+1})
`term_GR_1_rhs`	`LiteralExpression`
`literalValue`: ≤ freeRank(B_i)
`term_GR_1_forAll`	`ForAllDeclaration`
`variableName`: i in Session S
`term_GR_2_lhs`	`LiteralExpression`
`literalValue`: b.datum resolves under b.constraint
`term_GR_2_rhs`	`LiteralExpression`
`literalValue`: in O(1) iff Binding b is sound
`term_GR_2_forAll`	`ForAllDeclaration`
`variableName`: b: Binding
`term_GR_3_lhs`	`LiteralExpression`
`literalValue`: ∃ i: freeRank(B_i) = 0
`term_GR_3_rhs`	`LiteralExpression`
`literalValue`: Session S converges
`term_GR_3_forAll`	`ForAllDeclaration`
`variableName`: Session S
`term_GR_4_lhs`	`LiteralExpression`
`literalValue`: bindings(C_fresh) ∩ bindings(C_prior)
`term_GR_4_rhs`	`LiteralExpression`
`literalValue`: = ∅ after SessionBoundary
`term_GR_4_forAll`	`ForAllDeclaration`
`variableName`: C_prior, C_fresh: Context, SessionBoundary event
`term_GR_5_lhs`	`LiteralExpression`
`literalValue`: ContradictionBoundary
`term_GR_5_rhs`	`LiteralExpression`
`literalValue`: iff ∃ b, b': same address, different datum, same constraint
`term_GR_5_forAll`	`ForAllDeclaration`
`variableName`: b, b': Binding in same Context
`term_TS_1_lhs`	`LiteralExpression`
`literalValue`: nerve(T, target)
`term_TS_1_rhs`	`LiteralExpression`
`literalValue`: ∃ ConstrainedType T over R_n realising target
`term_TS_1_forAll`	`ForAllDeclaration`
`variableName`: target: χ* ≤ n, β₀* = 1, β_k* = 0 for k ≥ 1
`term_TS_2_lhs`	`LiteralExpression`
`literalValue`: basisSize(T, IT_7d target)
`term_TS_2_rhs`	`LiteralExpression`
`literalValue`: n
`term_TS_2_forAll`	`ForAllDeclaration`
`variableName`: IT_7d target, n-site types
`term_TS_3_lhs`	`LiteralExpression`
`literalValue`: χ(N(C + constraint))
`term_TS_3_rhs`	`LiteralExpression`
`literalValue`: ≥ χ(N(C))
`term_TS_3_forAll`	`ForAllDeclaration`
`variableName`: C: synthesis candidate constraint set
`term_TS_4_lhs`	`LiteralExpression`
`literalValue`: steps(TypeSynthesisResolver, target)
`term_TS_4_rhs`	`LiteralExpression`
`literalValue`: ≤ n
`term_TS_4_forAll`	`ForAllDeclaration`
`variableName`: target: realisable n-site type synthesis goal
`term_TS_5_lhs`	`LiteralExpression`
`literalValue`: SynthesizedType achieves IT_7d
`term_TS_5_rhs`	`LiteralExpression`
`literalValue`: iff CompletenessResolver certifies CompleteType
`term_TS_5_forAll`	`ForAllDeclaration`
`variableName`: T: SynthesizedType
`term_TS_6_lhs`	`LiteralExpression`
`literalValue`: E[steps, Jacobian-guided synthesis]
`term_TS_6_rhs`	`LiteralExpression`
`literalValue`: O(n log n) vs O(n²) uninformed
`term_TS_6_forAll`	`ForAllDeclaration`
`variableName`: T: n-site type synthesis goal
`term_TS_7_lhs`	`LiteralExpression`
`literalValue`: β₀(N(C)) for non-empty C
`term_TS_7_rhs`	`LiteralExpression`
`literalValue`: ≥ 1
`term_TS_7_forAll`	`ForAllDeclaration`
`variableName`: C: non-empty constraint set
`term_WLS_1_lhs`	`LiteralExpression`
`literalValue`: WittLift T' is CompleteType
`term_WLS_1_rhs`	`LiteralExpression`
`literalValue`: iff spectral sequence collapses at E_2
`term_WLS_1_forAll`	`ForAllDeclaration`
`variableName`: T: CompleteType at Q_n, T': WittLift to Q_{n+1}
`term_WLS_2_lhs`	`LiteralExpression`
`literalValue`: non-trivial LiftObstruction location
`term_WLS_2_rhs`	`LiteralExpression`
`literalValue`: specific site at bit position n+1
`term_WLS_2_forAll`	`ForAllDeclaration`
`variableName`: non-trivial LiftObstruction
`term_WLS_3_lhs`	`LiteralExpression`
`literalValue`: basisSize(T') for trivial lift
`term_WLS_3_rhs`	`LiteralExpression`
`literalValue`: basisSize(T) + 1
`term_WLS_3_forAll`	`ForAllDeclaration`
`variableName`: T: CompleteType at Q_n with closed constraint set
`term_WLS_4_lhs`	`LiteralExpression`
`literalValue`: spectral sequence convergence page
`term_WLS_4_rhs`	`LiteralExpression`
`literalValue`: ≤ E_{d+2}
`term_WLS_4_forAll`	`ForAllDeclaration`
`variableName`: depth-d constraint configuration
`term_WLS_5_lhs`	`LiteralExpression`
`literalValue`: universallyValid identity in R_{n+1}
`term_WLS_5_rhs`	`LiteralExpression`
`literalValue`: holds with lifted constraint set
`term_WLS_5_forAll`	`ForAllDeclaration`
`variableName`: every op:universallyValid identity, WittLift T'
`term_WLS_6_lhs`	`LiteralExpression`
`literalValue`: ψ-pipeline ChainComplex(T')
`term_WLS_6_rhs`	`LiteralExpression`
`literalValue`: valid and restricts to ChainComplex(T) on base nerve
`term_WLS_6_forAll`	`ForAllDeclaration`
`variableName`: T': any WittLift of a CompleteType T
`term_MN_1_lhs`	`LiteralExpression`
`literalValue`: HolonomyGroup(T)
`term_MN_1_rhs`	`LiteralExpression`
`literalValue`: ≤ D_{2^n}
`term_MN_1_forAll`	`ForAllDeclaration`
`variableName`: T: ConstrainedType over R_n
`term_MN_2_lhs`	`LiteralExpression`
`literalValue`: HolonomyGroup(T) for additive constraints
`term_MN_2_rhs`	`LiteralExpression`
`literalValue`: {id} (trivial: T is FlatType)
`term_MN_2_forAll`	`ForAllDeclaration`
`variableName`: T: all ResidueConstraint or DepthConstraint
`term_MN_3_lhs`	`LiteralExpression`
`literalValue`: HolonomyGroup(T) with neg + bnot in closed path
`term_MN_3_rhs`	`LiteralExpression`
`literalValue`: D_{2^n} (full dihedral holonomy)
`term_MN_3_forAll`	`ForAllDeclaration`
`variableName`: T: ConstrainedType with neg-related and bnot-related constraints in closed path
`term_MN_4_lhs`	`LiteralExpression`
`literalValue`: HolonomyGroup(T) ≠ {id}
`term_MN_4_rhs`	`LiteralExpression`
`literalValue`: ⟹ β₁(N(C(T))) ≥ 1
`term_MN_4_forAll`	`ForAllDeclaration`
`variableName`: T: ConstrainedType
`term_MN_5_lhs`	`LiteralExpression`
`literalValue`: CompleteType (IT_7d) ⟹ β₁ = 0 ⟹ holonomy
`term_MN_5_rhs`	`LiteralExpression`
`literalValue`: trivial ⟹ FlatType
`term_MN_5_forAll`	`ForAllDeclaration`
`variableName`: T: CompleteType
`term_MN_6_lhs`	`LiteralExpression`
`literalValue`: monodromy(p₁ · p₂)
`term_MN_6_rhs`	`LiteralExpression`
`literalValue`: monodromy(p₁) · monodromy(p₂) in D_{2^n}
`term_MN_6_forAll`	`ForAllDeclaration`
`variableName`: p₁, p₂: ClosedConstraintPath
`term_MN_7_lhs`	`LiteralExpression`
`literalValue`: TwistedType T ⟹ H²(N(C(T')); ℤ/2ℤ)
`term_MN_7_rhs`	`LiteralExpression`
`literalValue`: non-zero class (non-trivial LiftObstruction)
`term_MN_7_forAll`	`ForAllDeclaration`
`variableName`: T': any WittLift of TwistedType T
`term_PT_1_lhs`	`LiteralExpression`
`literalValue`: siteBudget(A × B)
`term_PT_1_rhs`	`LiteralExpression`
`literalValue`: siteBudget(A) + siteBudget(B)
`term_PT_1_forAll`	`ForAllDeclaration`
`variableName`: A, B: TypeDefinition
`term_PT_2_lhs`	`LiteralExpression`
`literalValue`: partition(A × B)
`term_PT_2_rhs`	`LiteralExpression`
`literalValue`: partition(A) ⊗ partition(B)
`term_PT_2_forAll`	`ForAllDeclaration`
`variableName`: A, B: TypeDefinition
`term_PT_3_lhs`	`LiteralExpression`
`literalValue`: χ(N(C(A × B)))
`term_PT_3_rhs`	`LiteralExpression`
`literalValue`: χ(N(C(A))) + χ(N(C(B)))
`term_PT_3_forAll`	`ForAllDeclaration`
`variableName`: A, B: TypeDefinition
`term_PT_4_lhs`	`LiteralExpression`
`literalValue`: S(A × B)
`term_PT_4_rhs`	`LiteralExpression`
`literalValue`: S(A) + S(B)
`term_PT_4_forAll`	`ForAllDeclaration`
`variableName`: A, B: TypeDefinition
`term_ST_1_lhs`	`LiteralExpression`
`literalValue`: siteBudget(A + B)
`term_ST_1_rhs`	`LiteralExpression`
`literalValue`: max(siteBudget(A), siteBudget(B))
`term_ST_1_forAll`	`ForAllDeclaration`
`variableName`: A, B: TypeDefinition
`term_ST_2_lhs`	`LiteralExpression`
`literalValue`: S(A + B)
`term_ST_2_rhs`	`LiteralExpression`
`literalValue`: ln 2 + max(S(A), S(B))
`term_ST_2_forAll`	`ForAllDeclaration`
`variableName`: A, B: TypeDefinition
`term_GS_1_lhs`	`LiteralExpression`
`literalValue`: T_ctx(C)
`term_GS_1_rhs`	`LiteralExpression`
`literalValue`: freeRank(C) × ln 2 / n
`term_GS_1_forAll`	`ForAllDeclaration`
`variableName`: C: Context, n = siteBudget
`term_GS_2_lhs`	`LiteralExpression`
`literalValue`: σ(C)
`term_GS_2_rhs`	`LiteralExpression`
`literalValue`: (n − freeRank(C)) / n
`term_GS_2_forAll`	`ForAllDeclaration`
`variableName`: C: Context, n = siteBudget
`term_GS_3_lhs`	`LiteralExpression`
`literalValue`: σ(B_{i+1})
`term_GS_3_rhs`	`LiteralExpression`
`literalValue`: ≥ σ(B_i)
`term_GS_3_forAll`	`ForAllDeclaration`
`variableName`: i in Session S
`term_GS_4_lhs`	`LiteralExpression`
`literalValue`: σ(C) = 1
`term_GS_4_rhs`	`LiteralExpression`
`literalValue`: freeRank(C) = 0 ↔ S(C) = 0 ↔ T_ctx(C) = 0
`term_GS_4_forAll`	`ForAllDeclaration`
`variableName`: C: Context
`term_GS_5_lhs`	`LiteralExpression`
`literalValue`: stepCount(q, C) at freeRank(C) = 0
`term_GS_5_rhs`	`LiteralExpression`
`literalValue`: 0
`term_GS_5_forAll`	`ForAllDeclaration`
`variableName`: q: Query, C: GroundedContext
`term_GS_6_lhs`	`LiteralExpression`
`literalValue`: effectiveBudget(q, C)
`term_GS_6_rhs`	`LiteralExpression`
`literalValue`: max(0, siteBudget(q.type) − \|pinnedSites(C) ∩ q.siteSet\|)
`term_GS_6_forAll`	`ForAllDeclaration`
`variableName`: q: Query, C: Context
`term_GS_7_lhs`	`LiteralExpression`
`literalValue`: Cost_saturation(C)
`term_GS_7_rhs`	`LiteralExpression`
`literalValue`: n × k_B T × ln 2
`term_GS_7_forAll`	`ForAllDeclaration`
`variableName`: C: GroundedContext, n = siteBudget
`term_MS_1_lhs`	`LiteralExpression`
`literalValue`: β₀(N(C))
`term_MS_1_rhs`	`LiteralExpression`
`literalValue`: ≥ 1
`term_MS_1_forAll`	`ForAllDeclaration`
`variableName`: C: non-empty ConstrainedType
`term_MS_2_lhs`	`LiteralExpression`
`literalValue`: χ(N(C))
`term_MS_2_rhs`	`LiteralExpression`
`literalValue`: ≤ n
`term_MS_2_forAll`	`ForAllDeclaration`
`variableName`: C: ConstrainedType at quantum level n
`term_MS_3_lhs`	`LiteralExpression`
`literalValue`: χ(N(C + c))
`term_MS_3_rhs`	`LiteralExpression`
`literalValue`: ≥ χ(N(C))
`term_MS_3_forAll`	`ForAllDeclaration`
`variableName`: C: ConstrainedType, c: Constraint
`term_MS_4_lhs`	`LiteralExpression`
`literalValue`: achievable(χ, β_k, n)
`term_MS_4_rhs`	`LiteralExpression`
`literalValue`: → achievable(χ, β_k, n+1)
`term_MS_4_forAll`	`ForAllDeclaration`
`variableName`: (χ, β_k) achievable at level n
`term_MS_5_lhs`	`LiteralExpression`
`literalValue`: verified SynthesisSignature set
`term_MS_5_rhs`	`LiteralExpression`
`literalValue`: → exact morphospace boundary in the limit
`term_MS_5_forAll`	`ForAllDeclaration`
`variableName`: all quantum levels
`term_GD_1_lhs`	`LiteralExpression`
`literalValue`: isGeodesic(T)
`term_GD_1_rhs`	`LiteralExpression`
`literalValue`: AR_1-ordered(T) ∧ DC_10-selected(T)
`term_GD_1_forAll`	`ForAllDeclaration`
`variableName`: T: ComputationTrace
`term_GD_2_lhs`	`LiteralExpression`
`literalValue`: ΔS_step(i) on geodesic
`term_GD_2_rhs`	`LiteralExpression`
`literalValue`: ln 2
`term_GD_2_forAll`	`ForAllDeclaration`
`variableName`: step i of GeodesicTrace T
`term_GD_3_lhs`	`LiteralExpression`
`literalValue`: Cost_geodesic(T)
`term_GD_3_rhs`	`LiteralExpression`
`literalValue`: freeRank_initial × k_B T × ln 2
`term_GD_3_forAll`	`ForAllDeclaration`
`variableName`: T: GeodesicTrace
`term_GD_4_lhs`	`LiteralExpression`
`literalValue`: Cost(T) for geodesic T
`term_GD_4_rhs`	`LiteralExpression`
`literalValue`: = Cost(T') for any geodesic T' on same type
`term_GD_4_forAll`	`ForAllDeclaration`
`variableName`: T, T': GeodesicTrace on same ConstrainedType
`term_GD_5_lhs`	`LiteralExpression`
`literalValue`: isSubgeodesic(T)
`term_GD_5_rhs`	`LiteralExpression`
`literalValue`: ∃ i: J_k(step_i) < max_{free} J_k(state_i)
`term_GD_5_forAll`	`ForAllDeclaration`
`variableName`: T: ComputationTrace
`term_QM_1_lhs`	`LiteralExpression`
`literalValue`: S_vonNeumann(ψ)
`term_QM_1_rhs`	`LiteralExpression`
`literalValue`: Cost_Landauer(collapse(ψ))
`term_QM_1_forAll`	`ForAllDeclaration`
`variableName`: ψ: SuperposedSiteState
`term_QM_2_lhs`	`LiteralExpression`
`literalValue`: collapse(ψ)
`term_QM_2_rhs`	`LiteralExpression`
`literalValue`: apply(ResidueConstraint, collapsed_site)
`term_QM_2_forAll`	`ForAllDeclaration`
`variableName`: ψ: SuperposedSiteState
`term_QM_3_lhs`	`LiteralExpression`
`literalValue`: S_vN(ψ)
`term_QM_3_rhs`	`LiteralExpression`
`literalValue`: ∈ [0, ln 2]
`term_QM_3_forAll`	`ForAllDeclaration`
`variableName`: ψ: single-site SuperposedSiteState
`term_QM_4_lhs`	`LiteralExpression`
`literalValue`: collapse(collapse(ψ))
`term_QM_4_rhs`	`LiteralExpression`
`literalValue`: collapse(ψ)
`term_QM_4_forAll`	`ForAllDeclaration`
`variableName`: ψ: SuperposedSiteState
`term_QM_5_lhs`	`LiteralExpression`
`literalValue`: Σᵢ \|αᵢ\|²
`term_QM_5_rhs`	`LiteralExpression`
`literalValue`: 1
`term_QM_5_forAll`	`ForAllDeclaration`
`variableName`: SuperposedSiteState ψ
`term_RC_6_lhs`	`LiteralExpression`
`literalValue`: normalize(ψ)
`term_RC_6_rhs`	`LiteralExpression`
`literalValue`: ψ / sqrt(Σ \|αᵢ\|²)
`term_RC_6_forAll`	`ForAllDeclaration`
`variableName`: SuperposedSiteState ψ
`term_FPM_8_lhs`	`LiteralExpression`
`literalValue`: \|Irr\| + \|Red\| + \|Unit\| + \|Ext\|
`term_FPM_8_rhs`	`LiteralExpression`
`literalValue`: 2ⁿ
`term_FPM_8_forAll`	`ForAllDeclaration`
`variableName`: Partition P over R_n
`term_FPM_9_lhs`	`LiteralExpression`
`literalValue`: x ∈ Ext(T)
`term_FPM_9_rhs`	`LiteralExpression`
`literalValue`: x ∉ carrier(T)
`term_FPM_9_forAll`	`ForAllDeclaration`
`variableName`: TypeDefinition T, Datum x
`term_MN_8_lhs`	`LiteralExpression`
`literalValue`: holonomyClassified(T)
`term_MN_8_rhs`	`LiteralExpression`
`literalValue`: isFlatType(T) xor isTwistedType(T)
`term_MN_8_forAll`	`ForAllDeclaration`
`variableName`: ConstrainedType T with holonomyGroup
`term_QL_8_lhs`	`LiteralExpression`
`literalValue`: wittLevelPredecessor(nextWittLevel(Q_k))
`term_QL_8_rhs`	`LiteralExpression`
`literalValue`: Q_k
`term_QL_8_forAll`	`ForAllDeclaration`
`variableName`: WittLevel W_n with nextWittLevel defined
`term_D_7_lhs`	`LiteralExpression`
`literalValue`: compose(rᵃ sᵖ, rᵇ sᵠ)
`term_D_7_rhs`	`LiteralExpression`
`literalValue`: r^((a + (-1)ᵖ b) mod 2ⁿ) s^(p xor q)
`term_D_7_forAll`	`ForAllDeclaration`
`variableName`: DihedralElement rᵃ sᵖ, rᵇ sᵠ in D_{2ⁿ}
`term_SP_1_lhs`	`LiteralExpression`
`literalValue`: resolve_superposition(classical(x))
`term_SP_1_rhs`	`LiteralExpression`
`literalValue`: resolve_classical(x)
`term_SP_1_forAll`	`ForAllDeclaration`
`variableName`: Datum x
`term_SP_2_lhs`	`LiteralExpression`
`literalValue`: collapse(resolve_superposition(ψ))
`term_SP_2_rhs`	`LiteralExpression`
`literalValue`: resolve_classical(collapse(ψ))
`term_SP_2_forAll`	`ForAllDeclaration`
`variableName`: SuperposedSiteState ψ
`term_SP_3_lhs`	`LiteralExpression`
`literalValue`: amplitudeVector(resolve_superposition(ψ))
`term_SP_3_rhs`	`LiteralExpression`
`literalValue`: normalized
`term_SP_3_forAll`	`ForAllDeclaration`
`variableName`: SuperposedSiteState ψ
`term_SP_4_lhs`	`LiteralExpression`
`literalValue`: P(collapse to site k)
`term_SP_4_rhs`	`LiteralExpression`
`literalValue`: \|α_k\|²
`term_SP_4_forAll`	`ForAllDeclaration`
`variableName`: SuperposedSiteState ψ, site index k
`term_PT_2a_lhs`	`LiteralExpression`
`literalValue`: Π(A × B)
`term_PT_2a_rhs`	`LiteralExpression`
`literalValue`: PartitionProduct(Π(A), Π(B))
`term_PT_2a_forAll`	`ForAllDeclaration`
`variableName`: ProductType A × B
`term_PT_2b_lhs`	`LiteralExpression`
`literalValue`: Π(A + B)
`term_PT_2b_rhs`	`LiteralExpression`
`literalValue`: PartitionCoproduct(Π(A), Π(B))
`term_PT_2b_forAll`	`ForAllDeclaration`
`variableName`: SumType A + B
`term_GD_6_lhs`	`LiteralExpression`
`literalValue`: isGeodesic(trace)
`term_GD_6_rhs`	`LiteralExpression`
`literalValue`: isAR1Ordered(trace) ∧ isDC10Selected(trace)
`term_GD_6_forAll`	`ForAllDeclaration`
`variableName`: ComputationTrace trace
`term_WT_1_lhs`	`LiteralExpression`
`literalValue`: LiftChain(Q_j, Q_k) valid
`term_WT_1_rhs`	`LiteralExpression`
`literalValue`: every chainStep has trivial or resolved LiftObstruction
`term_WT_1_forAll`	`ForAllDeclaration`
`variableName`: LiftChain from Q_j to Q_k
`term_WT_2_lhs`	`LiteralExpression`
`literalValue`: obstructionCount(chain)
`term_WT_2_rhs`	`LiteralExpression`
`literalValue`: <= chainLength(chain)
`term_WT_2_forAll`	`ForAllDeclaration`
`variableName`: LiftChain
`term_WT_3_lhs`	`LiteralExpression`
`literalValue`: resolvedBasisSize(Q_k)
`term_WT_3_rhs`	`LiteralExpression`
`literalValue`: basisSize(Q_j) + chainLength + obstructionResolutionCost
`term_WT_3_forAll`	`ForAllDeclaration`
`variableName`: LiftChain with source Q_j, target Q_k
`term_WT_4_lhs`	`LiteralExpression`
`literalValue`: isFlat(chain)
`term_WT_4_rhs`	`LiteralExpression`
`literalValue`: obstructionCount = 0 iff HolonomyGroup trivial at every step
`term_WT_4_forAll`	`ForAllDeclaration`
`variableName`: LiftChain
`term_WT_5_lhs`	`LiteralExpression`
`literalValue`: LiftChainCertificate exists
`term_WT_5_rhs`	`LiteralExpression`
`literalValue`: CompleteType at Q_k satisfies IT_7d with witness chain
`term_WT_5_forAll`	`ForAllDeclaration`
`variableName`: Q_k for arbitrary k
`term_WT_6_lhs`	`LiteralExpression`
`literalValue`: QT_3 with chainLength=1, cost=0
`term_WT_6_rhs`	`LiteralExpression`
`literalValue`: reduces to QLS_3
`term_WT_6_forAll`	`ForAllDeclaration`
`variableName`: Single-step chains
`term_WT_7_lhs`	`LiteralExpression`
`literalValue`: flat chain resolvedBasisSize(Q_k)
`term_WT_7_rhs`	`LiteralExpression`
`literalValue`: basisSize(Q_j) + (k - j)
`term_WT_7_forAll`	`ForAllDeclaration`
`variableName`: LiftChain with isFlat = true
`term_CC_PINS_lhs`	`LiteralExpression`
`literalValue`: pinsSites(CarryConstraint(p))
`term_CC_PINS_rhs`	`LiteralExpression`
`literalValue`: {k : p(k)=1} union {first-zero(p)}
`term_CC_PINS_forAll`	`ForAllDeclaration`
`variableName`: bit-pattern p in CarryConstraint
`term_CC_COST_SITE_lhs`	`LiteralExpression`
`literalValue`: \|pinsSites(CarryConstraint(p))\|
`term_CC_COST_SITE_rhs`	`LiteralExpression`
`literalValue`: popcount(p) + 1
`term_CC_COST_SITE_forAll`	`ForAllDeclaration`
`variableName`: bit-pattern p in CarryConstraint
`term_jsat_RR_lhs`	`LiteralExpression`
`literalValue`: jointSat(Res(m1,r1), Res(m2,r2))
`term_jsat_RR_rhs`	`LiteralExpression`
`literalValue`: gcd(m1,m2) \| (r1 - r2)
`term_jsat_RR_forAll`	`ForAllDeclaration`
`variableName`: ResidueConstraint pairs over R_n
`term_jsat_CR_lhs`	`LiteralExpression`
`literalValue`: jointSat(Carry(p), Res(m,r))
`term_jsat_CR_rhs`	`LiteralExpression`
`literalValue`: pin-site intersection residue-class compatible
`term_jsat_CR_forAll`	`ForAllDeclaration`
`variableName`: CarryConstraint, ResidueConstraint pairs
`term_jsat_CC_lhs`	`LiteralExpression`
`literalValue`: jointSat(Carry(p1), Carry(p2))
`term_jsat_CC_rhs`	`LiteralExpression`
`literalValue`: p1 AND p2 conflict-free
`term_jsat_CC_forAll`	`ForAllDeclaration`
`variableName`: CarryConstraint pairs over R_n
`term_D_8_lhs`	`LiteralExpression`
`literalValue`: (r^a s^p)^(-1)
`term_D_8_rhs`	`LiteralExpression`
`literalValue`: r^(-(−1)^p a mod 2^n) s^p
`term_D_8_forAll`	`ForAllDeclaration`
`variableName`: a in 0..2^n, p in {0,1}
`term_D_9_lhs`	`LiteralExpression`
`literalValue`: ord(r^k s^1)
`term_D_9_rhs`	`LiteralExpression`
`literalValue`: 2
`term_D_9_forAll`	`ForAllDeclaration`
`variableName`: k in Z/(2^n)Z
`term_EXP_1_lhs`	`LiteralExpression`
`literalValue`: carrier(C) is monotone
`term_EXP_1_rhs`	`LiteralExpression`
`literalValue`: all residues of C = modulus - 1, no Carry/Depth
`term_EXP_1_forAll`	`ForAllDeclaration`
`variableName`: ConstrainedType C over R_n
`term_EXP_2_lhs`	`LiteralExpression`
`literalValue`: count of monotone ConstrainedTypes at Q_n
`term_EXP_2_rhs`	`LiteralExpression`
`literalValue`: 2^n
`term_EXP_2_forAll`	`ForAllDeclaration`
`variableName`: WittLevel W_n, n >= 1
`term_EXP_3_lhs`	`LiteralExpression`
`literalValue`: carrier(SumType(A,B))
`term_EXP_3_rhs`	`LiteralExpression`
`literalValue`: coproduct(carrier(A), carrier(B))
`term_EXP_3_forAll`	`ForAllDeclaration`
`variableName`: SumType A + B
`term_ST_3_lhs`	`LiteralExpression`
`literalValue`: chi(N(C(A+B)))
`term_ST_3_rhs`	`LiteralExpression`
`literalValue`: chi(N(C(A))) + chi(N(C(B)))
`term_ST_3_forAll`	`ForAllDeclaration`
`variableName`: disjoint SumType A + B
`term_ST_4_lhs`	`LiteralExpression`
`literalValue`: beta_k(N(C(A+B)))
`term_ST_4_rhs`	`LiteralExpression`
`literalValue`: beta_k(N(C(A))) + beta_k(N(C(B)))
`term_ST_4_forAll`	`ForAllDeclaration`
`variableName`: disjoint SumType A + B, k >= 0
`term_ST_5_lhs`	`LiteralExpression`
`literalValue`: CompleteType(A + B)
`term_ST_5_rhs`	`LiteralExpression`
`literalValue`: CompleteType(A) and CompleteType(B) and Q(A)=Q(B)
`term_ST_5_forAll`	`ForAllDeclaration`
`variableName`: SumType A + B
`term_TS_8_lhs`	`LiteralExpression`
`literalValue`: min constraints for beta_1 = k
`term_TS_8_rhs`	`LiteralExpression`
`literalValue`: 2k + 1
`term_TS_8_forAll`	`ForAllDeclaration`
`variableName`: first Betti number k >= 1, n-site type
`term_TS_9_lhs`	`LiteralExpression`
`literalValue`: TypeSynthesisResolver terminates
`term_TS_9_rhs`	`LiteralExpression`
`literalValue`: within 2^n steps
`term_TS_9_forAll`	`ForAllDeclaration`
`variableName`: WittLevel W_n, any target signature
`term_TS_10_lhs`	`LiteralExpression`
`literalValue`: ForbiddenSignature(sigma)
`term_TS_10_rhs`	`LiteralExpression`
`literalValue`: no ConstrainedType with <= n constraints realises sigma
`term_TS_10_forAll`	`ForAllDeclaration`
`variableName`: topological signature sigma at Q_n
`term_WT_8_lhs`	`LiteralExpression`
`literalValue`: ObstructionChain length from Q_j to Q_k
`term_WT_8_rhs`	`LiteralExpression`
`literalValue`: <= (k-j) * C(basisSize(Q_j), 3)
`term_WT_8_forAll`	`ForAllDeclaration`
`variableName`: LiftChain from Q_j to Q_k
`term_WT_9_lhs`	`LiteralExpression`
`literalValue`: TowerCompletenessResolver terminates
`term_WT_9_rhs`	`LiteralExpression`
`literalValue`: within QT_8 bound
`term_WT_9_forAll`	`ForAllDeclaration`
`variableName`: LiftChain of finite length
`term_COEFF_1_lhs`	`LiteralExpression`
`literalValue`: standard coefficient ring for psi-pipeline
`term_COEFF_1_rhs`	`LiteralExpression`
`literalValue`: Z/2Z
`term_COEFF_1_forAll`	`ForAllDeclaration`
`variableName`: CechNerve N(C) at any quantum level
`term_GO_1_lhs`	`LiteralExpression`
`literalValue`: pinsSites(killing constraint for obstruction c)
`term_GO_1_rhs`	`LiteralExpression`
`literalValue`: superset of pinsSites(C_i) cap pinsSites(C_j)
`term_GO_1_forAll`	`ForAllDeclaration`
`variableName`: GluingObstruction c, cycle pair (C_i, C_j)
`term_GR_6_lhs`	`LiteralExpression`
`literalValue`: freeRank(q) after grounding
`term_GR_6_rhs`	`LiteralExpression`
`literalValue`: sites of q not in BindingAccumulator
`term_GR_6_forAll`	`ForAllDeclaration`
`variableName`: grounded Session, new RelationQuery q
`term_GR_7_lhs`	`LiteralExpression`
`literalValue`: sigma after re-entry with query q
`term_GR_7_rhs`	`LiteralExpression`
`literalValue`: min(sigma, 1 - freeRank(q)/n)
`term_GR_7_forAll`	`ForAllDeclaration`
`variableName`: SessionResolver, new query q
`term_QM_6_lhs`	`LiteralExpression`
`literalValue`: amplitude index set of SuperposedSiteState over T
`term_QM_6_rhs`	`LiteralExpression`
`literalValue`: monotone pinning trajectories consistent with T
`term_QM_6_forAll`	`ForAllDeclaration`
`variableName`: SuperposedSiteState over ConstrainedType T at Q_n
`term_CIC_1_lhs`	`LiteralExpression`
`literalValue`: valid(T) ∧ T: Transform
`term_CIC_1_rhs`	`LiteralExpression`
`literalValue`: ∃ c: TransformCertificate. certifies(c, T)
`term_CIC_1_forAll`	`ForAllDeclaration`
`variableName`: Transform T
`term_CIC_2_lhs`	`LiteralExpression`
`literalValue`: isometry(T) ∧ metric-preserving(T)
`term_CIC_2_rhs`	`LiteralExpression`
`literalValue`: ∃ c: IsometryCertificate. certifies(c, T)
`term_CIC_2_forAll`	`ForAllDeclaration`
`variableName`: Isometry T
`term_CIC_3_lhs`	`LiteralExpression`
`literalValue`: f(f(x)) = x ∀ x ∈ R_n
`term_CIC_3_rhs`	`LiteralExpression`
`literalValue`: ∃ c: InvolutionCertificate. certifies(c, f)
`term_CIC_3_forAll`	`ForAllDeclaration`
`variableName`: Involution f
`term_CIC_4_lhs`	`LiteralExpression`
`literalValue`: σ(C) = 1 ∧ freeRank = 0
`term_CIC_4_rhs`	`LiteralExpression`
`literalValue`: ∃ c: GroundingCertificate. certifies(c, C)
`term_CIC_4_forAll`	`ForAllDeclaration`
`variableName`: GroundedContext C
`term_CIC_5_lhs`	`LiteralExpression`
`literalValue`: AR_1-ordered ∧ DC_10-selected trace
`term_CIC_5_rhs`	`LiteralExpression`
`literalValue`: ∃ c: GeodesicCertificate. certifies(c, trace)
`term_CIC_5_forAll`	`ForAllDeclaration`
`variableName`: GeodesicTrace
`term_CIC_6_lhs`	`LiteralExpression`
`literalValue`: S_vN = L_cost at β* = ln 2
`term_CIC_6_rhs`	`LiteralExpression`
`literalValue`: ∃ c: MeasurementCertificate. certifies(c, event)
`term_CIC_6_forAll`	`ForAllDeclaration`
`variableName`: MeasurementEvent
`term_CIC_7_lhs`	`LiteralExpression`
`literalValue`: P(k) = \|α_k\|² verified
`term_CIC_7_rhs`	`LiteralExpression`
`literalValue`: ∃ c: BornRuleVerification. certifies(c, event)
`term_CIC_7_forAll`	`ForAllDeclaration`
`variableName`: MeasurementEvent with amplitude vector
`term_GC_1_lhs`	`LiteralExpression`
`literalValue`: shared-frame grounding of symbol s
`term_GC_1_rhs`	`LiteralExpression`
`literalValue`: ∃ c: GroundingCertificate. certifies(c, map)
`term_GC_1_forAll`	`ForAllDeclaration`
`variableName`: GroundingMap with valid ProjectionMap
`term_GR_8_lhs`	`LiteralExpression`
`literalValue`: compose(S_A, S_B) valid at Q_k
`term_GR_8_rhs`	`LiteralExpression`
`literalValue`: ∀ j ≤ k: ∀ a ∈ pinnedSites(S_A, Q_j) ∩ pinnedSites(S_B, Q_j): datum(S_A, a, Q_j) = datum(S_B, a, Q_j)
`term_GR_8_forAll`	`ForAllDeclaration`
`variableName`: S_A, S_B: Session at quantum level Q_k (k ≥ 0)
`term_GR_9_lhs`	`LiteralExpression`
`literalValue`: leasedSites(L_A) ∩ leasedSites(L_B)
`term_GR_9_rhs`	`LiteralExpression`
`literalValue`: = ∅
`term_GR_9_forAll`	`ForAllDeclaration`
`variableName`: L_A, L_B: ContextLease on SharedContext C, L_A ≠ L_B
`term_GR_10_lhs`	`LiteralExpression`
`literalValue`: finalState(R, P_1, Q)
`term_GR_10_rhs`	`LiteralExpression`
`literalValue`: = finalState(R, P_2, Q) for any P_1, P_2: ExecutionPolicy
`term_GR_10_forAll`	`ForAllDeclaration`
`variableName`: SessionResolver R with ExecutionPolicy P, pending query set Q
`term_MC_1_lhs`	`LiteralExpression`
`literalValue`: Σᵢ freeRank(leasedSites(L_i))
`term_MC_1_rhs`	`LiteralExpression`
`literalValue`: = freeRank(C)
`term_MC_1_forAll`	`ForAllDeclaration`
`variableName`: SharedContext C; leaseSet {L_1, …, L_k} covering all sites of C
`term_MC_2_lhs`	`LiteralExpression`
`literalValue`: freeRank(B_{i+1} \|_L)
`term_MC_2_rhs`	`LiteralExpression`
`literalValue`: ≤ freeRank(B_i \|_L)
`term_MC_2_forAll`	`ForAllDeclaration`
`variableName`: ContextLease L held by Session S; binding step i within S restricted to leasedSites(L)
`term_MC_3_lhs`	`LiteralExpression`
`literalValue`: freeRank(compose(S_A, S_B))
`term_MC_3_rhs`	`LiteralExpression`
`literalValue`: freeRank(S_A) + freeRank(S_B) − \|pinnedSites(S_A) ∩ pinnedSites(S_B)\|
`term_MC_3_forAll`	`ForAllDeclaration`
`variableName`: S_A, S_B: Session; compose(S_A, S_B) valid (SR_8 satisfied)
`term_MC_4_lhs`	`LiteralExpression`
`literalValue`: freeRank(compose(S_A, S_B))
`term_MC_4_rhs`	`LiteralExpression`
`literalValue`: = freeRank(S_A) + freeRank(S_B)
`term_MC_4_forAll`	`ForAllDeclaration`
`variableName`: S_A, S_B on ContextLeases L_A, L_B within SharedContext C; SR_9 holds
`term_MC_5_lhs`	`LiteralExpression`
`literalValue`: finalBindings(R, P_1, Q)
`term_MC_5_rhs`	`LiteralExpression`
`literalValue`: = finalBindings(R, P_2, Q)
`term_MC_5_forAll`	`ForAllDeclaration`
`variableName`: SessionResolver R; pending query set Q; ExecutionPolicy P_1, P_2
`term_MC_6_lhs`	`LiteralExpression`
`literalValue`: σ(compose(S_1, …, S_k))
`term_MC_6_rhs`	`LiteralExpression`
`literalValue`: = 1 (FullGrounding)
`term_MC_6_forAll`	`ForAllDeclaration`
`variableName`: SharedContext C; leases {L_1, …, L_k} pairwise disjoint (SR_9) and fully covering C; each S_i with freeRank = 0 within L_i
`term_MC_7_lhs`	`LiteralExpression`
`literalValue`: stepCount(q, C*)
`term_MC_7_rhs`	`LiteralExpression`
`literalValue`: = 0
`term_MC_7_forAll`	`ForAllDeclaration`
`variableName`: q: RelationQuery; C* = compose(S_1, …, S_k) with σ(C*) = 1 by MC_6
`term_MC_8_lhs`	`LiteralExpression`
`literalValue`: max_i stepCount(S_i to convergence within L_i)
`term_MC_8_rhs`	`LiteralExpression`
`literalValue`: ≤ ⌈n/k⌉
`term_MC_8_forAll`	`ForAllDeclaration`
`variableName`: SharedContext C with totalSites = n; uniform partition into k leases
`term_WC_1_lhs`	`LiteralExpression`
`literalValue`: a_k(x)
`term_WC_1_rhs`	`LiteralExpression`
`literalValue`: x_k (k-th bit of x)
`term_WC_1_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n, 0 ≤ k < n
`term_WC_2_lhs`	`LiteralExpression`
`literalValue`: S_k − x_k − y_k (mod 2)
`term_WC_2_rhs`	`LiteralExpression`
`literalValue`: c_k(x,y)
`term_WC_2_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n, 0 ≤ k < n
`term_WC_3_lhs`	`LiteralExpression`
`literalValue`: CA_2 recurrence
`term_WC_3_rhs`	`LiteralExpression`
`literalValue`: S_{k+1} ghost equation at p=2
`term_WC_3_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_WC_4_lhs`	`LiteralExpression`
`literalValue`: δ_k(x+y) correction
`term_WC_4_rhs`	`LiteralExpression`
`literalValue`: c_{k+1}(x,y)
`term_WC_4_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_WC_5_lhs`	`LiteralExpression`
`literalValue`: obstruction_trivial = false
`term_WC_5_rhs`	`LiteralExpression`
`literalValue`: δ_k ≠ 0 for some pair
`term_WC_5_forAll`	`ForAllDeclaration`
`variableName`: Q_k, k ≥ 1
`term_WC_6_lhs`	`LiteralExpression`
`literalValue`: d_Δ(x,y) > 0
`term_WC_6_rhs`	`LiteralExpression`
`literalValue`: ghost defect nonzero
`term_WC_6_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_WC_7_lhs`	`LiteralExpression`
`literalValue`: succ^{2ⁿ}(x) = x
`term_WC_7_rhs`	`LiteralExpression`
`literalValue`: r^{2ⁿ} = 1 in Witt-Burnside ring
`term_WC_7_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n, n ≥ 1
`term_WC_8_lhs`	`LiteralExpression`
`literalValue`: neg(succ(neg(x)))
`term_WC_8_rhs`	`LiteralExpression`
`literalValue`: srs = r⁻¹ relation
`term_WC_8_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n, n ≥ 1
`term_WC_9_lhs`	`LiteralExpression`
`literalValue`: bnot(neg(x)) = pred(x)
`term_WC_9_rhs`	`LiteralExpression`
`literalValue`: Product of Witt-Burnside reflections
`term_WC_9_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n, n ≥ 1
`term_WC_10_lhs`	`LiteralExpression`
`literalValue`: φ(x) on W_n(F_2)
`term_WC_10_rhs`	`LiteralExpression`
`literalValue`: x (identity, F_2 perfect)
`term_WC_10_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n, n ≥ 1
`term_WC_11_lhs`	`LiteralExpression`
`literalValue`: V(x) on W_n(F_2)
`term_WC_11_rhs`	`LiteralExpression`
`literalValue`: add(x, x) in Z/(2ⁿ)Z
`term_WC_11_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n, n ≥ 1
`term_WC_12_lhs`	`LiteralExpression`
`literalValue`: δ(x) on W_n(F_2)
`term_WC_12_rhs`	`LiteralExpression`
`literalValue`: (x − mul(x,x)) / 2
`term_WC_12_forAll`	`ForAllDeclaration`
`variableName`: x ∈ R_n, n ≥ 2
`term_OA_1_lhs`	`LiteralExpression`
`literalValue`: \|2\|_2 · \|2\|_∞
`term_OA_1_rhs`	`LiteralExpression`
`literalValue`: 1 in Q×
`term_OA_1_forAll`	`ForAllDeclaration`
`variableName`: p = 2
`term_OA_2_lhs`	`LiteralExpression`
`literalValue`: CrossingCost(p=2)
`term_OA_2_rhs`	`LiteralExpression`
`literalValue`: ln 2 = −ln\|2\|_2
`term_OA_2_forAll`	`ForAllDeclaration`
`variableName`: p = 2
`term_OA_3_lhs`	`LiteralExpression`
`literalValue`: β* in Cost_Landauer
`term_OA_3_rhs`	`LiteralExpression`
`literalValue`: CrossingCost(p=2)
`term_OA_3_forAll`	`ForAllDeclaration`
`variableName`: p = 2
`term_OA_4_lhs`	`LiteralExpression`
`literalValue`: P(outcome k) = \|α_k\|_∞²
`term_OA_4_rhs`	`LiteralExpression`
`literalValue`: Archimedean image of 2-adic amplitude
`term_OA_4_forAll`	`ForAllDeclaration`
`variableName`: rational amplitudes
`term_OA_5_lhs`	`LiteralExpression`
`literalValue`: Information cost of δ (division by 2)
`term_OA_5_rhs`	`LiteralExpression`
`literalValue`: ln 2 nats
`term_OA_5_forAll`	`ForAllDeclaration`
`variableName`: p = 2
`term_HT_1_lhs`	`LiteralExpression`
`literalValue`: N(C)
`term_HT_1_rhs`	`LiteralExpression`
`literalValue`: KanComplex
`term_HT_1_forAll`	`ForAllDeclaration`
`variableName`: constraint configuration C
`term_HT_2_lhs`	`LiteralExpression`
`literalValue`: π₀(N(C))
`term_HT_2_rhs`	`LiteralExpression`
`literalValue`: Z^{β₀}
`term_HT_2_forAll`	`ForAllDeclaration`
`variableName`: constraint configuration C
`term_HT_3_lhs`	`LiteralExpression`
`literalValue`: π₁(N(C)) → D_{2^n}
`term_HT_3_rhs`	`LiteralExpression`
`literalValue`: HolonomyGroup factorization
`term_HT_3_forAll`	`ForAllDeclaration`
`variableName`: constraint configuration C
`term_HT_4_lhs`	`LiteralExpression`
`literalValue`: π_k(N(C)) for k > dim(N(C))
`term_HT_4_rhs`	`LiteralExpression`
`literalValue`: 0
`term_HT_4_forAll`	`ForAllDeclaration`
`variableName`: constraint configuration C, k > dim(N(C))
`term_HT_5_lhs`	`LiteralExpression`
`literalValue`: τ_{≤1}(N(C))
`term_HT_5_rhs`	`LiteralExpression`
`literalValue`: FlatType/TwistedType classification
`term_HT_5_forAll`	`ForAllDeclaration`
`variableName`: constraint configuration C
`term_HT_6_lhs`	`LiteralExpression`
`literalValue`: κ_k trivial for all k > d
`term_HT_6_rhs`	`LiteralExpression`
`literalValue`: spectral sequence collapses at E_{d+2}
`term_HT_6_forAll`	`ForAllDeclaration`
`variableName`: constraint configuration C, d = max simplex dim
`term_HT_7_lhs`	`LiteralExpression`
`literalValue`: [α, β] ≠ 0 in π_{p+q−1}
`term_HT_7_rhs`	`LiteralExpression`
`literalValue`: LiftObstruction non-trivial
`term_HT_7_forAll`	`ForAllDeclaration`
`variableName`: α ∈ π_p, β ∈ π_q
`term_HT_8_lhs`	`LiteralExpression`
`literalValue`: π_k(N(C)) ⊗ Z
`term_HT_8_rhs`	`LiteralExpression`
`literalValue`: H_k(N(C); Z) for smallest k with π_k ≠ 0
`term_HT_8_forAll`	`ForAllDeclaration`
`variableName`: constraint configuration C
`term_psi_7_lhs`	`LiteralExpression`
`literalValue`: KanComplex(N(C))
`term_psi_7_rhs`	`LiteralExpression`
`literalValue`: PostnikovTower
`term_psi_7_forAll`	`ForAllDeclaration`
`variableName`: constraint configuration C
`term_psi_8_lhs`	`LiteralExpression`
`literalValue`: PostnikovTower(τ≤k)
`term_psi_8_rhs`	`LiteralExpression`
`literalValue`: HomotopyGroups(π_k)
`term_psi_8_forAll`	`ForAllDeclaration`
`variableName`: constraint configuration C
`term_psi_9_lhs`	`LiteralExpression`
`literalValue`: HomotopyGroups(π_k)
`term_psi_9_rhs`	`LiteralExpression`
`literalValue`: KInvariants(κ_k)
`term_psi_9_forAll`	`ForAllDeclaration`
`variableName`: constraint configuration C
`term_HP_1_lhs`	`LiteralExpression`
`literalValue`: ψ_7 ∘ ψ_1
`term_HP_1_rhs`	`LiteralExpression`
`literalValue`: Kan promotion of nerve
`term_HP_1_forAll`	`ForAllDeclaration`
`variableName`: constraint configuration C
`term_HP_2_lhs`	`LiteralExpression`
`literalValue`: ψ_8(τ≤k) restricted
`term_HP_2_rhs`	`LiteralExpression`
`literalValue`: ψ_3(C≤k)
`term_HP_2_forAll`	`ForAllDeclaration`
`variableName`: constraint configuration C, truncation level k
`term_HP_3_lhs`	`LiteralExpression`
`literalValue`: ψ_9 detects convergence
`term_HP_3_rhs`	`LiteralExpression`
`literalValue`: spectral sequence converges at E_{d+2}
`term_HP_3_forAll`	`ForAllDeclaration`
`variableName`: constraint configuration C
`term_HP_4_lhs`	`LiteralExpression`
`literalValue`: HomotopyResolver time
`term_HP_4_rhs`	`LiteralExpression`
`literalValue`: O(n^{d+1})
`term_HP_4_forAll`	`ForAllDeclaration`
`variableName`: d = max simplex dimension
`term_MD_1_lhs`	`LiteralExpression`
`literalValue`: dim(M_n)
`term_MD_1_rhs`	`LiteralExpression`
`literalValue`: basisSize(T)
`term_MD_1_forAll`	`ForAllDeclaration`
`variableName`: T in M_n
`term_MD_2_lhs`	`LiteralExpression`
`literalValue`: H^0(Def(T))
`term_MD_2_rhs`	`LiteralExpression`
`literalValue`: Aut(T) ∩ D_{2^n}
`term_MD_2_forAll`	`ForAllDeclaration`
`variableName`: CompleteType T
`term_MD_3_lhs`	`LiteralExpression`
`literalValue`: H^1(Def(T))
`term_MD_3_rhs`	`LiteralExpression`
`literalValue`: T_T(M_n)
`term_MD_3_forAll`	`ForAllDeclaration`
`variableName`: CompleteType T
`term_MD_4_lhs`	`LiteralExpression`
`literalValue`: H^2(Def(T))
`term_MD_4_rhs`	`LiteralExpression`
`literalValue`: LiftObstruction space
`term_MD_4_forAll`	`ForAllDeclaration`
`variableName`: CompleteType T
`term_MD_5_lhs`	`LiteralExpression`
`literalValue`: FlatType stratum codimension
`term_MD_5_rhs`	`LiteralExpression`
`literalValue`: 0
`term_MD_5_forAll`	`ForAllDeclaration`
`variableName`: M_n at any quantum level
`term_MD_6_lhs`	`LiteralExpression`
`literalValue`: TwistedType stratum codimension
`term_MD_6_rhs`	`LiteralExpression`
`literalValue`: ≥ 1
`term_MD_6_forAll`	`ForAllDeclaration`
`variableName`: M_n at any quantum level
`term_MD_7_lhs`	`LiteralExpression`
`literalValue`: VersalDeformation existence
`term_MD_7_rhs`	`LiteralExpression`
`literalValue`: guaranteed when H^2 = 0
`term_MD_7_forAll`	`ForAllDeclaration`
`variableName`: CompleteType T
`term_MD_8_lhs`	`LiteralExpression`
`literalValue`: familyPreservesCompleteness
`term_MD_8_rhs`	`LiteralExpression`
`literalValue`: H^2(Def(T_t)) = 0 along path
`term_MD_8_forAll`	`ForAllDeclaration`
`variableName`: DeformationFamily {C_t}
`term_MD_9_lhs`	`LiteralExpression`
`literalValue`: site(ModuliTowerMap, T) dimension
`term_MD_9_rhs`	`LiteralExpression`
`literalValue`: 1 when obstructionTrivial
`term_MD_9_forAll`	`ForAllDeclaration`
`variableName`: CompleteType T, obstruction = 0
`term_MD_10_lhs`	`LiteralExpression`
`literalValue`: site(ModuliTowerMap, T)
`term_MD_10_rhs`	`LiteralExpression`
`literalValue`: empty iff TwistedType at every level
`term_MD_10_forAll`	`ForAllDeclaration`
`variableName`: CompleteType T
`term_MR_1_lhs`	`LiteralExpression`
`literalValue`: ModuliResolver boundary
`term_MR_1_rhs`	`LiteralExpression`
`literalValue`: MorphospaceBoundary
`term_MR_1_forAll`	`ForAllDeclaration`
`variableName`: M_n
`term_MR_2_lhs`	`LiteralExpression`
`literalValue`: StratificationRecord coverage
`term_MR_2_rhs`	`LiteralExpression`
`literalValue`: every CompleteType in exactly one stratum
`term_MR_2_forAll`	`ForAllDeclaration`
`variableName`: M_n
`term_MR_3_lhs`	`LiteralExpression`
`literalValue`: ModuliResolver complexity
`term_MR_3_rhs`	`LiteralExpression`
`literalValue`: O(n × basisSize²)
`term_MR_3_forAll`	`ForAllDeclaration`
`variableName`: CompleteType T
`term_MR_4_lhs`	`LiteralExpression`
`literalValue`: achievabilityStatus = Achievable
`term_MR_4_rhs`	`LiteralExpression`
`literalValue`: signature in some HolonomyStratum
`term_MR_4_forAll`	`ForAllDeclaration`
`variableName`: MorphospaceRecord
`term_CY_1_lhs`	`LiteralExpression`
`literalValue`: generate(k)
`term_CY_1_rhs`	`LiteralExpression`
`literalValue`: and(x_k, y_k) = 1
`term_CY_1_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n, 0 ≤ k < n
`term_CY_2_lhs`	`LiteralExpression`
`literalValue`: propagate(k)
`term_CY_2_rhs`	`LiteralExpression`
`literalValue`: xor(x_k, y_k) = 1 ∧ c_k = 1
`term_CY_2_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n, 0 ≤ k < n
`term_CY_3_lhs`	`LiteralExpression`
`literalValue`: kill(k)
`term_CY_3_rhs`	`LiteralExpression`
`literalValue`: and(x_k, y_k) = 0 ∧ xor(x_k, y_k) = 0
`term_CY_3_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n, 0 ≤ k < n
`term_CY_4_lhs`	`LiteralExpression`
`literalValue`: d_Δ(x, y)
`term_CY_4_rhs`	`LiteralExpression`
`literalValue`: \|carryCount(x+y) − hammingDistance(x, y)\|
`term_CY_4_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_CY_5_lhs`	`LiteralExpression`
`literalValue`: argmin_enc Σ d_Δ(enc(s_i), enc(s_j))
`term_CY_5_rhs`	`LiteralExpression`
`literalValue`: enc where carry significance ≅ domain dependency
`term_CY_5_forAll`	`ForAllDeclaration`
`variableName`: finite symbol set S, observed pairs (s_i, s_j)
`term_CY_6_lhs`	`LiteralExpression`
`literalValue`: min d_Δ site ordering
`term_CY_6_rhs`	`LiteralExpression`
`literalValue`: high-significance sites → most informative observables
`term_CY_6_forAll`	`ForAllDeclaration`
`variableName`: EncodingConfiguration over ordered domain
`term_CY_7_lhs`	`LiteralExpression`
`literalValue`: T(carry_chain(n))
`term_CY_7_rhs`	`LiteralExpression`
`literalValue`: O(log n) via prefix computation on (g_k, p_k) pairs
`term_CY_7_forAll`	`ForAllDeclaration`
`variableName`: CarryChain of length n
`term_BM_1_lhs`	`LiteralExpression`
`literalValue`: σ(C)
`term_BM_1_rhs`	`LiteralExpression`
`literalValue`: (n − freeRank(C)) / n
`term_BM_1_forAll`	`ForAllDeclaration`
`variableName`: Context C with n sites
`term_BM_2_lhs`	`LiteralExpression`
`literalValue`: χ(nerve(C))
`term_BM_2_rhs`	`LiteralExpression`
`literalValue`: Σ(−1)^k β_k(nerve(C))
`term_BM_2_forAll`	`ForAllDeclaration`
`variableName`: constraint set C
`term_BM_3_lhs`	`LiteralExpression`
`literalValue`: Σκ_k − χ
`term_BM_3_rhs`	`LiteralExpression`
`literalValue`: S_residual / ln 2
`term_BM_3_forAll`	`ForAllDeclaration`
`variableName`: computation state
`term_BM_4_lhs`	`LiteralExpression`
`literalValue`: J_k (pinned site k)
`term_BM_4_rhs`	`LiteralExpression`
`literalValue`: 0
`term_BM_4_forAll`	`ForAllDeclaration`
`variableName`: pinned site k
`term_BM_5_lhs`	`LiteralExpression`
`literalValue`: d_Δ(x, y) > 0
`term_BM_5_rhs`	`LiteralExpression`
`literalValue`: carry(x + y) ≠ 0
`term_BM_5_forAll`	`ForAllDeclaration`
`variableName`: x, y ∈ R_n
`term_BM_6_lhs`	`LiteralExpression`
`literalValue`: metric tower
`term_BM_6_rhs`	`LiteralExpression`
`literalValue`: d_Δ → {σ, J_k} → β_k → χ → r
`term_BM_6_forAll`	`ForAllDeclaration`
`variableName`: computation state
`term_GL_1_lhs`	`LiteralExpression`
`literalValue`: σ(T)
`term_GL_1_rhs`	`LiteralExpression`
`literalValue`: lower_adjoint(T)
`term_GL_1_forAll`	`ForAllDeclaration`
`variableName`: type T in type lattice
`term_GL_2_lhs`	`LiteralExpression`
`literalValue`: r(T)
`term_GL_2_rhs`	`LiteralExpression`
`literalValue`: 1 − upper_adjoint(T)
`term_GL_2_forAll`	`ForAllDeclaration`
`variableName`: type T in type lattice
`term_GL_3_lhs`	`LiteralExpression`
`literalValue`: upper(lower(T))
`term_GL_3_rhs`	`LiteralExpression`
`literalValue`: T (fixpoint: σ=1, r=0)
`term_GL_3_forAll`	`ForAllDeclaration`
`variableName`: CompleteType T
`term_GL_4_lhs`	`LiteralExpression`
`literalValue`: T₁ ≤ T₂ in type lattice
`term_GL_4_rhs`	`LiteralExpression`
`literalValue`: site(T₂) ⊆ site(T₁)
`term_GL_4_forAll`	`ForAllDeclaration`
`variableName`: types T₁, T₂
`term_NV_1_lhs`	`LiteralExpression`
`literalValue`: nerve(C₁ ∪ C₂)
`term_NV_1_rhs`	`LiteralExpression`
`literalValue`: nerve(C₁) ∪ nerve(C₂)
`term_NV_1_forAll`	`ForAllDeclaration`
`variableName`: disjoint constraint domains C₁, C₂
`term_NV_2_lhs`	`LiteralExpression`
`literalValue`: β_k(C₁ ∪ C₂)
`term_NV_2_rhs`	`LiteralExpression`
`literalValue`: β_k(C₁) + β_k(C₂) − β_k(C₁ ∩ C₂)
`term_NV_2_forAll`	`ForAllDeclaration`
`variableName`: constraint sets C₁, C₂
`term_NV_3_lhs`	`LiteralExpression`
`literalValue`: Δβ_k
`term_NV_3_rhs`	`LiteralExpression`
`literalValue`: ∈ {−1, 0, +1}
`term_NV_3_forAll`	`ForAllDeclaration`
`variableName`: single constraint addition, dimension k
`term_NV_4_lhs`	`LiteralExpression`
`literalValue`: β_k(C ∪ {c})
`term_NV_4_rhs`	`LiteralExpression`
`literalValue`: ≤ β_k(C)
`term_NV_4_forAll`	`ForAllDeclaration`
`variableName`: constraint set C, new constraint c
`term_SD_1_lhs`	`LiteralExpression`
`literalValue`: quantize(value, range, bits)
`term_SD_1_rhs`	`LiteralExpression`
`literalValue`: ring element with d_R ∝ \|v₁ − v₂\|
`term_SD_1_forAll`	`ForAllDeclaration`
`variableName`: values v in ordered domain
`term_SD_2_lhs`	`LiteralExpression`
`literalValue`: encoding(alphabet)
`term_SD_2_rhs`	`LiteralExpression`
`literalValue`: argmin_{e} Σ d_Δ(e(a), e(b))
`term_SD_2_forAll`	`ForAllDeclaration`
`variableName`: symbol pairs (a,b) in alphabet
`term_SD_3_lhs`	`LiteralExpression`
`literalValue`: Seq(T)
`term_SD_3_rhs`	`LiteralExpression`
`literalValue`: Free(T) with backbone ordering
`term_SD_3_forAll`	`ForAllDeclaration`
`variableName`: element type T
`term_SD_4_lhs`	`LiteralExpression`
`literalValue`: sites(Tuple(f₁,...,fₖ))
`term_SD_4_rhs`	`LiteralExpression`
`literalValue`: Σᵢ sites(fᵢ)
`term_SD_4_forAll`	`ForAllDeclaration`
`variableName`: fields f_1,...,f_k of tuple type
`term_SD_5_lhs`	`LiteralExpression`
`literalValue`: nerve(Graph(V,E))
`term_SD_5_rhs`	`LiteralExpression`
`literalValue`: constraint_nerve(Graph(V,E))
`term_SD_5_forAll`	`ForAllDeclaration`
`variableName`: graph (V,E) with typed nodes
`term_SD_6_lhs`	`LiteralExpression`
`literalValue`: d_Δ(Set(a,b,c))
`term_SD_6_rhs`	`LiteralExpression`
`literalValue`: d_Δ(Set(σ(a,b,c)))
`term_SD_6_forAll`	`ForAllDeclaration`
`variableName`: permutation σ of set elements
`term_SD_7_lhs`	`LiteralExpression`
`literalValue`: β_1(Tree(V,E))
`term_SD_7_rhs`	`LiteralExpression`
`literalValue`: 0
`term_SD_7_forAll`	`ForAllDeclaration`
`variableName`: tree (V,E) with beta_0=1
`term_SD_8_lhs`	`LiteralExpression`
`literalValue`: Table(S)
`term_SD_8_rhs`	`LiteralExpression`
`literalValue`: Seq(Tuple(S))
`term_SD_8_forAll`	`ForAllDeclaration`
`variableName`: schema S defining tuple fields
`term_DD_1_lhs`	`LiteralExpression`
`literalValue`: δ(q, R)
`term_DD_1_rhs`	`LiteralExpression`
`literalValue`: δ(q, R)
`term_DD_1_forAll`	`ForAllDeclaration`
`variableName`: query q, registry R
`term_DD_2_lhs`	`LiteralExpression`
`literalValue`: dom(R)
`term_DD_2_rhs`	`LiteralExpression`
`literalValue`: {q \| ∃r. δ(q,R)=r}
`term_DD_2_forAll`	`ForAllDeclaration`
`variableName`: registry R
`term_PI_1_lhs`	`LiteralExpression`
`literalValue`: ι(ι(s,C),C)
`term_PI_1_rhs`	`LiteralExpression`
`literalValue`: ι(s,C)
`term_PI_1_forAll`	`ForAllDeclaration`
`variableName`: symbol s, GroundedContext C
`term_PI_2_lhs`	`LiteralExpression`
`literalValue`: type(ι(s,C))
`term_PI_2_rhs`	`LiteralExpression`
`literalValue`: consistent(C)
`term_PI_2_forAll`	`ForAllDeclaration`
`variableName`: symbol s, context C
`term_PI_3_lhs`	`LiteralExpression`
`literalValue`: ι(s,C)
`term_PI_3_rhs`	`LiteralExpression`
`literalValue`: P(Π(G(s,C)))
`term_PI_3_forAll`	`ForAllDeclaration`
`variableName`: symbol s, context C
`term_PI_4_lhs`	`LiteralExpression`
`literalValue`: complexity(ι(s,C))
`term_PI_4_rhs`	`LiteralExpression`
`literalValue`: O(\|C\|)
`term_PI_4_forAll`	`ForAllDeclaration`
`variableName`: symbol s, context C
`term_PI_5_lhs`	`LiteralExpression`
`literalValue`: roundTrip(P(Π(G(s))))
`term_PI_5_rhs`	`LiteralExpression`
`literalValue`: s
`term_PI_5_forAll`	`ForAllDeclaration`
`variableName`: symbol s
`term_PA_1_lhs`	`LiteralExpression`
`literalValue`: α(b₁,α(b₂,C))
`term_PA_1_rhs`	`LiteralExpression`
`literalValue`: α(b₂,α(b₁,C))
`term_PA_1_forAll`	`ForAllDeclaration`
`variableName`: bindings b₁,b₂, context C at saturation
`term_PA_2_lhs`	`LiteralExpression`
`literalValue`: sites(α(b,C))
`term_PA_2_rhs`	`LiteralExpression`
`literalValue`: sites(C) ∪ {b.site}
`term_PA_2_forAll`	`ForAllDeclaration`
`variableName`: binding b, context C
`term_PA_3_lhs`	`LiteralExpression`
`literalValue`: constraints(α(b,C))
`term_PA_3_rhs`	`LiteralExpression`
`literalValue`: constraints(C) ∪ constraints(b)
`term_PA_3_forAll`	`ForAllDeclaration`
`variableName`: binding b, context C
`term_PA_4_lhs`	`LiteralExpression`
`literalValue`: α(b,C)\|_{pinned(C)}
`term_PA_4_rhs`	`LiteralExpression`
`literalValue`: C\|_{pinned(C)}
`term_PA_4_forAll`	`ForAllDeclaration`
`variableName`: binding b, context C
`term_PA_5_lhs`	`LiteralExpression`
`literalValue`: α(∅, C)
`term_PA_5_rhs`	`LiteralExpression`
`literalValue`: C
`term_PA_5_forAll`	`ForAllDeclaration`
`variableName`: context C
`term_PL_1_lhs`	`LiteralExpression`
`literalValue`: Lᵢ ∩ Lⱼ
`term_PL_1_rhs`	`LiteralExpression`
`literalValue`: ∅
`term_PL_1_forAll`	`ForAllDeclaration`
`variableName`: leases Lᵢ, Lⱼ with i ≠ j
`term_PL_2_lhs`	`LiteralExpression`
`literalValue`: ⋃ᵢ Lᵢ
`term_PL_2_rhs`	`LiteralExpression`
`literalValue`: S
`term_PL_2_forAll`	`ForAllDeclaration`
`variableName`: shared context S, leases Lᵢ
`term_PL_3_lhs`	`LiteralExpression`
`literalValue`: \|{i \| f ∈ Lᵢ}\|
`term_PL_3_rhs`	`LiteralExpression`
`literalValue`: 1
`term_PL_3_forAll`	`ForAllDeclaration`
`variableName`: site f in shared context S
`term_PK_1_lhs`	`LiteralExpression`
`literalValue`: valid(κ(S₁,S₂))
`term_PK_1_rhs`	`LiteralExpression`
`literalValue`: disjoint(S₁,S₂)
`term_PK_1_forAll`	`ForAllDeclaration`
`variableName`: sessions S₁,S₂
`term_PK_2_lhs`	`LiteralExpression`
`literalValue`: resolve(s, κ(S₁,S₂))
`term_PK_2_rhs`	`LiteralExpression`
`literalValue`: resolve(s, S₁) ∨ resolve(s, S₂)
`term_PK_2_forAll`	`ForAllDeclaration`
`variableName`: symbol s, sessions S₁,S₂
`term_PP_1_lhs`	`LiteralExpression`
`literalValue`: κ(λₖ(α*(ι(s,·))), C)
`term_PP_1_rhs`	`LiteralExpression`
`literalValue`: resolve(s, C)
`term_PP_1_forAll`	`ForAllDeclaration`
`variableName`: symbol s, context C
`term_PE_1_lhs`	`LiteralExpression`
`literalValue`: state(ψ, 0)
`term_PE_1_rhs`	`LiteralExpression`
`literalValue`: 1
`term_PE_1_forAll`	`ForAllDeclaration`
`variableName`: reduction ψ
`term_PE_2_lhs`	`LiteralExpression`
`literalValue`: ψ_1(q)
`term_PE_2_rhs`	`LiteralExpression`
`literalValue`: δ(q, R)
`term_PE_2_forAll`	`ForAllDeclaration`
`variableName`: query q, registry R
`term_PE_3_lhs`	`LiteralExpression`
`literalValue`: ψ_2(r)
`term_PE_3_rhs`	`LiteralExpression`
`literalValue`: G(r)
`term_PE_3_forAll`	`ForAllDeclaration`
`variableName`: resolver r
`term_PE_4_lhs`	`LiteralExpression`
`literalValue`: ψ_3(a)
`term_PE_4_rhs`	`LiteralExpression`
`literalValue`: Π(a)
`term_PE_4_forAll`	`ForAllDeclaration`
`variableName`: address a
`term_PE_5_lhs`	`LiteralExpression`
`literalValue`: ψ_4(c)
`term_PE_5_rhs`	`LiteralExpression`
`literalValue`: α*(c)
`term_PE_5_forAll`	`ForAllDeclaration`
`variableName`: constraint set c
`term_PE_6_lhs`	`LiteralExpression`
`literalValue`: ψ_5(b)
`term_PE_6_rhs`	`LiteralExpression`
`literalValue`: P(b)
`term_PE_6_forAll`	`ForAllDeclaration`
`variableName`: binding b
`term_PE_7_lhs`	`LiteralExpression`
`literalValue`: ψ_5 ∘ ψ_4 ∘ ψ_3 ∘ ψ_2 ∘ ψ_1 ∘ ψ_0
`term_PE_7_rhs`	`LiteralExpression`
`literalValue`: ψ
`term_PE_7_forAll`	`ForAllDeclaration`
`variableName`: reduction ψ
`term_PM_1_lhs`	`LiteralExpression`
`literalValue`: phase(stage_k)
`term_PM_1_rhs`	`LiteralExpression`
`literalValue`: Ω^k
`term_PM_1_forAll`	`ForAllDeclaration`
`variableName`: stage index k in 0..5
`term_PM_2_lhs`	`LiteralExpression`
`literalValue`: gate(k)
`term_PM_2_rhs`	`LiteralExpression`
`literalValue`: phase(k) == Ω^k
`term_PM_2_forAll`	`ForAllDeclaration`
`variableName`: stage boundary k
`term_PM_3_lhs`	`LiteralExpression`
`literalValue`: fail(gate(k))
`term_PM_3_rhs`	`LiteralExpression`
`literalValue`: rollback(z → z̄)
`term_PM_3_forAll`	`ForAllDeclaration`
`variableName`: stage k with gate failure
`term_PM_4_lhs`	`LiteralExpression`
`literalValue`: conj(conj(z))
`term_PM_4_rhs`	`LiteralExpression`
`literalValue`: z
`term_PM_4_forAll`	`ForAllDeclaration`
`variableName`: complex value z
`term_PM_5_lhs`	`LiteralExpression`
`literalValue`: sat(epoch_n)
`term_PM_5_rhs`	`LiteralExpression`
`literalValue`: sat(epoch_{n+1})
`term_PM_5_forAll`	`ForAllDeclaration`
`variableName`: consecutive epochs n, n+1
`term_PM_6_lhs`	`LiteralExpression`
`literalValue`: context(window)
`term_PM_6_rhs`	`LiteralExpression`
`literalValue`: base_context
`term_PM_6_forAll`	`ForAllDeclaration`
`variableName`: service window
`term_PM_7_lhs`	`LiteralExpression`
`literalValue`: ψ(s₀)
`term_PM_7_rhs`	`LiteralExpression`
`literalValue`: ψ(s₀)
`term_PM_7_forAll`	`ForAllDeclaration`
`variableName`: initial state s₀
`term_ER_1_lhs`	`LiteralExpression`
`literalValue`: advance(k, k+1)
`term_ER_1_rhs`	`LiteralExpression`
`literalValue`: guard(k) = true
`term_ER_1_forAll`	`ForAllDeclaration`
`variableName`: stage transition k to k+1
`term_ER_2_lhs`	`LiteralExpression`
`literalValue`: apply(effect(k))
`term_ER_2_rhs`	`LiteralExpression`
`literalValue`: atomic(effect(k))
`term_ER_2_forAll`	`ForAllDeclaration`
`variableName`: transition effect at stage k
`term_ER_3_lhs`	`LiteralExpression`
`literalValue`: eval(guard(k), s)
`term_ER_3_rhs`	`LiteralExpression`
`literalValue`: s (state unchanged)
`term_ER_3_forAll`	`ForAllDeclaration`
`variableName`: guard evaluation at stage k with state s
`term_ER_4_lhs`	`LiteralExpression`
`literalValue`: apply(e1; e2)
`term_ER_4_rhs`	`LiteralExpression`
`literalValue`: apply(e2; e1)
`term_ER_4_forAll`	`ForAllDeclaration`
`variableName`: effects e1, e2 within same stage
`term_EA_1_lhs`	`LiteralExpression`
`literalValue`: free(epoch(n+1))
`term_EA_1_rhs`	`LiteralExpression`
`literalValue`: free(epoch(0))
`term_EA_1_forAll`	`ForAllDeclaration`
`variableName`: epoch boundary n to n+1
`term_EA_2_lhs`	`LiteralExpression`
`literalValue`: grounded(epoch(n))
`term_EA_2_rhs`	`LiteralExpression`
`literalValue`: grounded(epoch(n+1))
`term_EA_2_forAll`	`ForAllDeclaration`
`variableName`: grounded sites across epoch boundary
`term_EA_3_lhs`	`LiteralExpression`
`literalValue`: \|context(w)\|
`term_EA_3_rhs`	`LiteralExpression`
`literalValue`: windowSize(w)
`term_EA_3_forAll`	`ForAllDeclaration`
`variableName`: service window w
`term_EA_4_lhs`	`LiteralExpression`
`literalValue`: admit(epoch(n))
`term_EA_4_rhs`	`LiteralExpression`
`literalValue`: datum \| refinement
`term_EA_4_forAll`	`ForAllDeclaration`
`variableName`: epoch admission at epoch n
`term_OE_1_lhs`	`LiteralExpression`
`literalValue`: stage(k); stage(k+1)
`term_OE_1_rhs`	`LiteralExpression`
`literalValue`: fused(k, k+1)
`term_OE_1_forAll`	`ForAllDeclaration`
`variableName`: adjacent stages k, k+1 with compatible guards
`term_OE_2_lhs`	`LiteralExpression`
`literalValue`: effect(a); effect(b)
`term_OE_2_rhs`	`LiteralExpression`
`literalValue`: effect(b); effect(a)
`term_OE_2_forAll`	`ForAllDeclaration`
`variableName`: independent effects a, b
`term_OE_3_lhs`	`LiteralExpression`
`literalValue`: lease(A); lease(B)
`term_OE_3_rhs`	`LiteralExpression`
`literalValue`: lease(A) \|\| lease(B)
`term_OE_3_forAll`	`ForAllDeclaration`
`variableName`: disjoint lease sets A, B
`term_OE_4a_lhs`	`LiteralExpression`
`literalValue`: sem(fused(k, k+1))
`term_OE_4a_rhs`	`LiteralExpression`
`literalValue`: sem(stage(k)); sem(stage(k+1))
`term_OE_4a_forAll`	`ForAllDeclaration`
`variableName`: fused stages k, k+1
`term_OE_4b_lhs`	`LiteralExpression`
`literalValue`: outcome(a; b)
`term_OE_4b_rhs`	`LiteralExpression`
`literalValue`: outcome(b; a)
`term_OE_4b_forAll`	`ForAllDeclaration`
`variableName`: commuting effects a, b
`term_OE_4c_lhs`	`LiteralExpression`
`literalValue`: coverage(A \|\| B)
`term_OE_4c_rhs`	`LiteralExpression`
`literalValue`: coverage(A) + coverage(B)
`term_OE_4c_forAll`	`ForAllDeclaration`
`variableName`: parallel leases A, B
`term_CS_1_lhs`	`LiteralExpression`
`literalValue`: cost(stage(k))
`term_CS_1_rhs`	`LiteralExpression`
`literalValue`: O(1)
`term_CS_1_forAll`	`ForAllDeclaration`
`variableName`: reduction step k
`term_CS_2_lhs`	`LiteralExpression`
`literalValue`: cost(pipeline)
`term_CS_2_rhs`	`LiteralExpression`
`literalValue`: sum(cost(stage(k)))
`term_CS_2_forAll`	`ForAllDeclaration`
`variableName`: reduction pipeline
`term_CS_3_lhs`	`LiteralExpression`
`literalValue`: cost(rollback)
`term_CS_3_rhs`	`LiteralExpression`
`literalValue`: cost(forward)
`term_CS_3_forAll`	`ForAllDeclaration`
`variableName`: reduction rollback operation
`term_CS_4_lhs`	`LiteralExpression`
`literalValue`: cost(preflight)
`term_CS_4_rhs`	`LiteralExpression`
`literalValue`: O(1)
`term_CS_4_forAll`	`ForAllDeclaration`
`variableName`: preflight check
`term_CS_5_lhs`	`LiteralExpression`
`literalValue`: cost(reduction)
`term_CS_5_rhs`	`LiteralExpression`
`literalValue`: n * max(cost(stage(k)))
`term_CS_5_forAll`	`ForAllDeclaration`
`variableName`: reduction with n stages
`term_CS_6_lhs`	`LiteralExpression`
`literalValue`: thermodynamicBudget(U) < bitsWidth(unitWittLevel(U)) × ln 2
`term_CS_6_rhs`	`LiteralExpression`
`literalValue`: reject(U) at BudgetSolvencyCheck
`term_CS_6_forAll`	`ForAllDeclaration`
`variableName`: CompileUnit U
`term_CS_7_lhs`	`LiteralExpression`
`literalValue`: unitAddress(U)
`term_CS_7_rhs`	`LiteralExpression`
`literalValue`: address(canonicalBytes(transitiveClosure(rootTerm(U))))
`term_CS_7_forAll`	`ForAllDeclaration`
`variableName`: CompileUnit U
`term_FA_1_lhs`	`LiteralExpression`
`literalValue`: pending(q)
`term_FA_1_rhs`	`LiteralExpression`
`literalValue`: reaches_gate(q)
`term_FA_1_forAll`	`ForAllDeclaration`
`variableName`: query q in reduction
`term_FA_2_lhs`	`LiteralExpression`
`literalValue`: admitted(q, epoch)
`term_FA_2_rhs`	`LiteralExpression`
`literalValue`: served(q, epoch + k)
`term_FA_2_forAll`	`ForAllDeclaration`
`variableName`: query q, bounded k
`term_FA_3_lhs`	`LiteralExpression`
`literalValue`: lease_alloc(p1 + p2)
`term_FA_3_rhs`	`LiteralExpression`
`literalValue`: lease_alloc(p1) + lease_alloc(p2)
`term_FA_3_forAll`	`ForAllDeclaration`
`variableName`: disjoint partitions p1, p2
`term_SW_1_lhs`	`LiteralExpression`
`literalValue`: memory(window(w))
`term_SW_1_rhs`	`LiteralExpression`
`literalValue`: O(w)
`term_SW_1_forAll`	`ForAllDeclaration`
`variableName`: service window of size w
`term_SW_2_lhs`	`LiteralExpression`
`literalValue`: saturated(slide(w))
`term_SW_2_rhs`	`LiteralExpression`
`literalValue`: saturated(w)
`term_SW_2_forAll`	`ForAllDeclaration`
`variableName`: window slide operation
`term_SW_3_lhs`	`LiteralExpression`
`literalValue`: resources(evict(e))
`term_SW_3_rhs`	`LiteralExpression`
`literalValue`: 0
`term_SW_3_forAll`	`ForAllDeclaration`
`variableName`: evicted epoch e
`term_SW_4_lhs`	`LiteralExpression`
`literalValue`: size(window)
`term_SW_4_rhs`	`LiteralExpression`
`literalValue`: >= 1
`term_SW_4_forAll`	`ForAllDeclaration`
`variableName`: service window
`term_LS_1_lhs`	`LiteralExpression`
`literalValue`: pinned(suspend(lease))
`term_LS_1_rhs`	`LiteralExpression`
`literalValue`: pinned(lease)
`term_LS_1_forAll`	`ForAllDeclaration`
`variableName`: lease suspension
`term_LS_2_lhs`	`LiteralExpression`
`literalValue`: resources(expire(lease))
`term_LS_2_rhs`	`LiteralExpression`
`literalValue`: 0
`term_LS_2_forAll`	`ForAllDeclaration`
`variableName`: expired lease
`term_LS_3_lhs`	`LiteralExpression`
`literalValue`: restore(restore(checkpoint))
`term_LS_3_rhs`	`LiteralExpression`
`literalValue`: restore(checkpoint)
`term_LS_3_forAll`	`ForAllDeclaration`
`variableName`: checkpoint restore
`term_LS_4_lhs`	`LiteralExpression`
`literalValue`: resume(suspend(lease))
`term_LS_4_rhs`	`LiteralExpression`
`literalValue`: lease
`term_LS_4_forAll`	`ForAllDeclaration`
`variableName`: active lease
`term_TJ_1_lhs`	`LiteralExpression`
`literalValue`: all_or_nothing(fail)
`term_TJ_1_rhs`	`LiteralExpression`
`literalValue`: rollback
`term_TJ_1_forAll`	`ForAllDeclaration`
`variableName`: AllOrNothing transaction with failure
`term_TJ_2_lhs`	`LiteralExpression`
`literalValue`: best_effort(partial_fail)
`term_TJ_2_rhs`	`LiteralExpression`
`literalValue`: commit(succeeded)
`term_TJ_2_forAll`	`ForAllDeclaration`
`variableName`: BestEffort transaction
`term_TJ_3_lhs`	`LiteralExpression`
`literalValue`: scope(transaction)
`term_TJ_3_rhs`	`LiteralExpression`
`literalValue`: single_epoch
`term_TJ_3_forAll`	`ForAllDeclaration`
`variableName`: reduction transaction
`term_AP_1_lhs`	`LiteralExpression`
`literalValue`: sat(stage(k+1))
`term_AP_1_rhs`	`LiteralExpression`
`literalValue`: >= sat(stage(k))
`term_AP_1_forAll`	`ForAllDeclaration`
`variableName`: consecutive stages k, k+1
`term_AP_2_lhs`	`LiteralExpression`
`literalValue`: quality(epoch(n+1))
`term_AP_2_rhs`	`LiteralExpression`
`literalValue`: >= quality(epoch(n))
`term_AP_2_forAll`	`ForAllDeclaration`
`variableName`: consecutive epochs n, n+1
`term_AP_3_lhs`	`LiteralExpression`
`literalValue`: deferred(q)
`term_AP_3_rhs`	`LiteralExpression`
`literalValue`: processed(q) \| dropped(q)
`term_AP_3_forAll`	`ForAllDeclaration`
`variableName`: deferred query q
`term_EC_1_lhs`	`LiteralExpression`
`literalValue`: Ω⁶
`term_EC_1_rhs`	`LiteralExpression`
`literalValue`: −1
`term_EC_1_forAll`	`ForAllDeclaration`
`variableName`: reduction phase angle Ω = e^{iπ/6}
`term_EC_2_lhs`	`LiteralExpression`
`literalValue`: conj(conj(z))
`term_EC_2_rhs`	`LiteralExpression`
`literalValue`: z
`term_EC_2_forAll`	`ForAllDeclaration`
`variableName`: complex z in reduction
`term_EC_3_lhs`	`LiteralExpression`
`literalValue`: [q_A, q_B]^inf
`term_EC_3_rhs`	`LiteralExpression`
`literalValue`: 1
`term_EC_3_forAll`	`ForAllDeclaration`
`variableName`: quaternion pair q_A, q_B
`term_EC_4_lhs`	`LiteralExpression`
`literalValue`: [q_A, q_B, q_C]^inf
`term_EC_4_rhs`	`LiteralExpression`
`literalValue`: 0
`term_EC_4_forAll`	`ForAllDeclaration`
`variableName`: octonion triple q_A, q_B, q_C
`term_EC_4a_lhs`	`LiteralExpression`
`literalValue`: \|\|[a,b,c]_{n+1}\|\|
`term_EC_4a_rhs`	`LiteralExpression`
`literalValue`: <= \|\|[a,b,c]_n\|\|
`term_EC_4a_forAll`	`ForAllDeclaration`
`variableName`: successive associator iterates
`term_EC_4b_lhs`	`LiteralExpression`
`literalValue`: steps_to_zero([a,b,c])
`term_EC_4b_rhs`	`LiteralExpression`
`literalValue`: <= \|three_way_sites\|
`term_EC_4b_forAll`	`ForAllDeclaration`
`variableName`: octonion triple a, b, c
`term_EC_4c_lhs`	`LiteralExpression`
`literalValue`: [a,b,c] = 0
`term_EC_4c_rhs`	`LiteralExpression`
`literalValue`: associative(resolved_site_space)
`term_EC_4c_forAll`	`ForAllDeclaration`
`variableName`: resolved site space
`term_EC_5_lhs`	`LiteralExpression`
`literalValue`: max_level(convergence_tower)
`term_EC_5_rhs`	`LiteralExpression`
`literalValue`: L3_Self
`term_EC_5_forAll`	`ForAllDeclaration`
`variableName`: convergence tower
`term_DA_1_lhs`	`LiteralExpression`
`literalValue`: CD(R, i)
`term_DA_1_rhs`	`LiteralExpression`
`literalValue`: C
`term_DA_1_forAll`	`ForAllDeclaration`
`variableName`: Cayley-Dickson doubling
`term_DA_2_lhs`	`LiteralExpression`
`literalValue`: CD(C, j)
`term_DA_2_rhs`	`LiteralExpression`
`literalValue`: H
`term_DA_2_forAll`	`ForAllDeclaration`
`variableName`: Cayley-Dickson doubling
`term_DA_3_lhs`	`LiteralExpression`
`literalValue`: CD(H, l)
`term_DA_3_rhs`	`LiteralExpression`
`literalValue`: O
`term_DA_3_forAll`	`ForAllDeclaration`
`variableName`: Cayley-Dickson doubling
`term_DA_4_lhs`	`LiteralExpression`
`literalValue`: dim(normed_div_alg)
`term_DA_4_rhs`	`LiteralExpression`
`literalValue`: ∈ {1, 2, 4, 8}
`term_DA_4_forAll`	`ForAllDeclaration`
`variableName`: normed division algebras over R
`term_DA_5_lhs`	`LiteralExpression`
`literalValue`: algebra(L_k)
`term_DA_5_rhs`	`LiteralExpression`
`literalValue`: division_algebra[k]
`term_DA_5_forAll`	`ForAllDeclaration`
`variableName`: convergence level L_k
`term_DA_6_lhs`	`LiteralExpression`
`literalValue`: [a,b] = 0
`term_DA_6_rhs`	`LiteralExpression`
`literalValue`: isCommutative(algebra(L_k))
`term_DA_6_forAll`	`ForAllDeclaration`
`variableName`: elements a, b in division algebra at level k
`term_DA_7_lhs`	`LiteralExpression`
`literalValue`: [a,b,c] = 0
`term_DA_7_rhs`	`LiteralExpression`
`literalValue`: isAssociative(algebra(L_k))
`term_DA_7_forAll`	`ForAllDeclaration`
`variableName`: elements a, b, c in division algebra at level k
`term_IN_1_lhs`	`LiteralExpression`
`literalValue`: d_Δ(A,B)
`term_IN_1_rhs`	`LiteralExpression`
`literalValue`: interaction_cost(A,B)
`term_IN_1_forAll`	`ForAllDeclaration`
`variableName`: entity pairs A, B
`term_IN_2_lhs`	`LiteralExpression`
`literalValue`: disjoint_leases(A,B)
`term_IN_2_rhs`	`LiteralExpression`
`literalValue`: commutator(A,B) = 0
`term_IN_2_forAll`	`ForAllDeclaration`
`variableName`: entity pairs with disjoint leases
`term_IN_3_lhs`	`LiteralExpression`
`literalValue`: shared_sites(A,B) ≠ ∅
`term_IN_3_rhs`	`LiteralExpression`
`literalValue`: commutator(A,B) > 0
`term_IN_3_forAll`	`ForAllDeclaration`
`variableName`: entity pairs with shared sites
`term_IN_4_lhs`	`LiteralExpression`
`literalValue`: SR_8_session(A,B)
`term_IN_4_rhs`	`LiteralExpression`
`literalValue`: commutator(A,B,t+1) ≤ commutator(A,B,t)
`term_IN_4_forAll`	`ForAllDeclaration`
`variableName`: entity pairs in session
`term_IN_5_lhs`	`LiteralExpression`
`literalValue`: converged_negotiation(A,B)
`term_IN_5_rhs`	`LiteralExpression`
`literalValue`: U(1) ⊂ SU(2)
`term_IN_5_forAll`	`ForAllDeclaration`
`variableName`: converged pairwise interactions
`term_IN_6_lhs`	`LiteralExpression`
`literalValue`: outcome_space(pairwise_negotiation)
`term_IN_6_rhs`	`LiteralExpression`
`literalValue`: S²
`term_IN_6_forAll`	`ForAllDeclaration`
`variableName`: pairwise negotiations
`term_IN_7_lhs`	`LiteralExpression`
`literalValue`: converged_mutual_model(A,B,C)
`term_IN_7_rhs`	`LiteralExpression`
`literalValue`: H ⊂ O
`term_IN_7_forAll`	`ForAllDeclaration`
`variableName`: converged triple interactions
`term_IN_8_lhs`	`LiteralExpression`
`literalValue`: β_k(interaction_nerve)
`term_IN_8_rhs`	`LiteralExpression`
`literalValue`: coupling_complexity(k)
`term_IN_8_forAll`	`ForAllDeclaration`
`variableName`: interaction nerve at dimension k
`term_IN_9_lhs`	`LiteralExpression`
`literalValue`: β_2(nerve) × max_disagreement
`term_IN_9_rhs`	`LiteralExpression`
`literalValue`: upper_bound(associator_norm)
`term_IN_9_forAll`	`ForAllDeclaration`
`variableName`: interaction nerves with β_2 > 0
`term_AS_1_lhs`	`LiteralExpression`
`literalValue`: (δ ∘ ι) ∘ κ
`term_AS_1_rhs`	`LiteralExpression`
`literalValue`: δ ∘ (ι ∘ κ)
`term_AS_1_forAll`	`ForAllDeclaration`
`variableName`: triple δ, ι, κ with shared registry
`term_AS_2_lhs`	`LiteralExpression`
`literalValue`: (ι ∘ α) ∘ λ
`term_AS_2_rhs`	`LiteralExpression`
`literalValue`: ι ∘ (α ∘ λ)
`term_AS_2_forAll`	`ForAllDeclaration`
`variableName`: triple ι, α, λ with shared lease
`term_AS_3_lhs`	`LiteralExpression`
`literalValue`: (λ ∘ κ) ∘ δ
`term_AS_3_rhs`	`LiteralExpression`
`literalValue`: λ ∘ (κ ∘ δ)
`term_AS_3_forAll`	`ForAllDeclaration`
`variableName`: triple λ, κ, δ with shared state
`term_AS_4_lhs`	`LiteralExpression`
`literalValue`: associator(A,B,C) ≠ 0
`term_AS_4_rhs`	`LiteralExpression`
`literalValue`: ∃ mediating read-write interleaving
`term_AS_4_forAll`	`ForAllDeclaration`
`variableName`: triples with non-zero associator
`term_MO_1_lhs`	`LiteralExpression`
`literalValue`: I ⊗ A
`term_MO_1_rhs`	`LiteralExpression`
`literalValue`: A
`term_MO_1_forAll`	`ForAllDeclaration`
`variableName`: computations A
`term_MO_2_lhs`	`LiteralExpression`
`literalValue`: (A⊗B)⊗C
`term_MO_2_rhs`	`LiteralExpression`
`literalValue`: A⊗(B⊗C)
`term_MO_2_forAll`	`ForAllDeclaration`
`variableName`: computations A, B, C
`term_MO_3_lhs`	`LiteralExpression`
`literalValue`: cert(A⊗B)
`term_MO_3_rhs`	`LiteralExpression`
`literalValue`: cert(A) ∧ cert(B)
`term_MO_3_forAll`	`ForAllDeclaration`
`variableName`: certified computations A, B
`term_MO_4_lhs`	`LiteralExpression`
`literalValue`: σ(A⊗B)
`term_MO_4_rhs`	`LiteralExpression`
`literalValue`: max(σ(A), σ(B))
`term_MO_4_forAll`	`ForAllDeclaration`
`variableName`: computations A, B
`term_MO_5_lhs`	`LiteralExpression`
`literalValue`: r(A⊗B)
`term_MO_5_rhs`	`LiteralExpression`
`literalValue`: min(r(A), r(B))
`term_MO_5_forAll`	`ForAllDeclaration`
`variableName`: computations A, B
`term_OP_1_lhs`	`LiteralExpression`
`literalValue`: siteCount(F(G))
`term_OP_1_rhs`	`LiteralExpression`
`literalValue`: F.sites + Σ_i G_i.sites
`term_OP_1_forAll`	`ForAllDeclaration`
`variableName`: structural types F, G
`term_OP_2_lhs`	`LiteralExpression`
`literalValue`: grounding(F(G(x)))
`term_OP_2_rhs`	`LiteralExpression`
`literalValue`: F.ground(G.ground(x))
`term_OP_2_forAll`	`ForAllDeclaration`
`variableName`: structural types F, G, element x
`term_OP_3_lhs`	`LiteralExpression`
`literalValue`: d_Δ(F(G))
`term_OP_3_rhs`	`LiteralExpression`
`literalValue`: d_Δ(F) ∘ G + F ∘ d_Δ(G)
`term_OP_3_forAll`	`ForAllDeclaration`
`variableName`: structural types F, G
`term_OP_4_lhs`	`LiteralExpression`
`literalValue`: Table(Tuple(fields))
`term_OP_4_rhs`	`LiteralExpression`
`literalValue`: Sequence(Tuple(fields))
`term_OP_4_forAll`	`ForAllDeclaration`
`variableName`: tabular data
`term_OP_5_lhs`	`LiteralExpression`
`literalValue`: Tree(Symbol(leaves))
`term_OP_5_rhs`	`LiteralExpression`
`literalValue`: Graph(Symbol(leaves), acyclic)
`term_OP_5_forAll`	`ForAllDeclaration`
`variableName`: hierarchical data
`term_FX_1_lhs`	`LiteralExpression`
`literalValue`: freeRank(postContext(e))
`term_FX_1_rhs`	`LiteralExpression`
`literalValue`: freeRank(preContext(e)) − 1
`term_FX_1_forAll`	`ForAllDeclaration`
`variableName`: PinningEffect e
`term_FX_2_lhs`	`LiteralExpression`
`literalValue`: freeRank(postContext(e))
`term_FX_2_rhs`	`LiteralExpression`
`literalValue`: freeRank(preContext(e)) + 1
`term_FX_2_forAll`	`ForAllDeclaration`
`variableName`: UnbindingEffect e
`term_FX_3_lhs`	`LiteralExpression`
`literalValue`: freeRank(postContext(e))
`term_FX_3_rhs`	`LiteralExpression`
`literalValue`: freeRank(preContext(e))
`term_FX_3_forAll`	`ForAllDeclaration`
`variableName`: PhaseEffect e
`term_FX_4_lhs`	`LiteralExpression`
`literalValue`: apply(A ; B, ctx)
`term_FX_4_rhs`	`LiteralExpression`
`literalValue`: apply(B ; A, ctx)
`term_FX_4_forAll`	`ForAllDeclaration`
`variableName`: Effects A, B with DisjointnessWitness(target(A), target(B))
`term_FX_5_lhs`	`LiteralExpression`
`literalValue`: freeRankDelta(E₁ ; E₂)
`term_FX_5_rhs`	`LiteralExpression`
`literalValue`: freeRankDelta(E₁) + freeRankDelta(E₂)
`term_FX_5_forAll`	`ForAllDeclaration`
`variableName`: CompositeEffect (E₁ ; E₂)
`term_FX_6_lhs`	`LiteralExpression`
`literalValue`: apply(e, apply(e⁻¹, ctx))
`term_FX_6_rhs`	`LiteralExpression`
`literalValue`: ctx
`term_FX_6_forAll`	`ForAllDeclaration`
`variableName`: ReversibleEffect e
`term_FX_7_lhs`	`LiteralExpression`
`literalValue`: freeRankDelta(e)
`term_FX_7_rhs`	`LiteralExpression`
`literalValue`: declared freeRankDelta in EffectShape
`term_FX_7_forAll`	`ForAllDeclaration`
`variableName`: ExternalEffect e satisfying conformance:EffectShape
`term_PR_1_lhs`	`LiteralExpression`
`literalValue`: eval(p, x)
`term_PR_1_rhs`	`LiteralExpression`
`literalValue`: ∈ {true, false}
`term_PR_1_forAll`	`ForAllDeclaration`
`variableName`: Predicate p, input x
`term_PR_2_lhs`	`LiteralExpression`
`literalValue`: state(eval(p, x, s))
`term_PR_2_rhs`	`LiteralExpression`
`literalValue`: s
`term_PR_2_forAll`	`ForAllDeclaration`
`variableName`: Predicate p, input x, state s
`term_PR_3_lhs`	`LiteralExpression`
`literalValue`: dispatch(D, x)
`term_PR_3_rhs`	`LiteralExpression`
`literalValue`: exactly one DispatchRule
`term_PR_3_forAll`	`ForAllDeclaration`
`variableName`: DispatchTable D with isExhaustive=true, isMutuallyExclusive=true
`term_PR_4_lhs`	`LiteralExpression`
`literalValue`: eval(M)
`term_PR_4_rhs`	`LiteralExpression`
`literalValue`: armResult(first matching arm)
`term_PR_4_forAll`	`ForAllDeclaration`
`variableName`: MatchExpression M with exhaustive arms
`term_PR_5_lhs`	`LiteralExpression`
`literalValue`: advance(k, guardTarget(g))
`term_PR_5_rhs`	`LiteralExpression`
`literalValue`: requires guardPredicate(g) = true
`term_PR_5_forAll`	`ForAllDeclaration`
`variableName`: GuardedTransition g at reduction step k
`term_CG_1_lhs`	`LiteralExpression`
`literalValue`: advance_to(s)
`term_CG_1_rhs`	`LiteralExpression`
`literalValue`: requires eval(g, currentState) = true
`term_CG_1_forAll`	`ForAllDeclaration`
`variableName`: ReductionStep s with entryGuard g
`term_CG_2_lhs`	`LiteralExpression`
`literalValue`: advance_from(s)
`term_CG_2_rhs`	`LiteralExpression`
`literalValue`: requires eval(g, currentState) = true, then apply(e)
`term_CG_2_forAll`	`ForAllDeclaration`
`variableName`: ReductionStep s with exitGuard g and stageEffect e
`term_DIS_1_lhs`	`LiteralExpression`
`literalValue`: isExhaustive(D) ∧ isMutuallyExclusive(D)
`term_DIS_1_rhs`	`LiteralExpression`
`literalValue`: true
`term_DIS_1_forAll`	`ForAllDeclaration`
`variableName`: Root DispatchTable D
`term_DIS_2_lhs`	`LiteralExpression`
`literalValue`: dispatch(D, T)
`term_DIS_2_rhs`	`LiteralExpression`
`literalValue`: exactly one Resolver
`term_DIS_2_forAll`	`ForAllDeclaration`
`variableName`: TypeDefinition T, DispatchTable D
`term_PAR_1_lhs`	`LiteralExpression`
`literalValue`: apply(A ⊗ B, ctx)
`term_PAR_1_rhs`	`LiteralExpression`
`literalValue`: apply(B ⊗ A, ctx)
`term_PAR_1_forAll`	`ForAllDeclaration`
`variableName`: ParallelProduct A ∥ B with DisjointnessCertificate
`term_PAR_2_lhs`	`LiteralExpression`
`literalValue`: freeRankDelta(A ∥ B)
`term_PAR_2_rhs`	`LiteralExpression`
`literalValue`: freeRankDelta(A) + freeRankDelta(B)
`term_PAR_2_forAll`	`ForAllDeclaration`
`variableName`: ParallelProduct A ∥ B
`term_PAR_3_lhs`	`LiteralExpression`
`literalValue`: Σ \|component_i\|
`term_PAR_3_rhs`	`LiteralExpression`
`literalValue`: n
`term_PAR_3_forAll`	`ForAllDeclaration`
`variableName`: SitePartitioning P over n sites
`term_PAR_4_lhs`	`LiteralExpression`
`literalValue`: finalContext(σ(A, B))
`term_PAR_4_rhs`	`LiteralExpression`
`literalValue`: finalContext(A ⊗ B)
`term_PAR_4_forAll`	`ForAllDeclaration`
`variableName`: ParallelProduct A ∥ B, any interleaving σ
`term_PAR_5_lhs`	`LiteralExpression`
`literalValue`: cert(A ∥ B)
`term_PAR_5_rhs`	`LiteralExpression`
`literalValue`: cert(A) ∧ cert(B) ∧ DisjointnessCertificate(A, B)
`term_PAR_5_forAll`	`ForAllDeclaration`
`variableName`: cert(A ∥ B)
`term_HO_1_lhs`	`LiteralExpression`
`literalValue`: value(c)
`term_HO_1_rhs`	`LiteralExpression`
`literalValue`: contentHash(referencedCertificate(c))
`term_HO_1_forAll`	`ForAllDeclaration`
`variableName`: ComputationDatum c
`term_HO_2_lhs`	`LiteralExpression`
`literalValue`: cert(output(app))
`term_HO_2_rhs`	`LiteralExpression`
`literalValue`: cert(applicationTarget(app))
`term_HO_2_forAll`	`ForAllDeclaration`
`variableName`: ApplicationMorphism app
`term_HO_3_lhs`	`LiteralExpression`
`literalValue`: cert(f ∘ g)
`term_HO_3_rhs`	`LiteralExpression`
`literalValue`: cert(f) ∧ cert(g) ∧ range(g) = domain(f)
`term_HO_3_forAll`	`ForAllDeclaration`
`variableName`: TransformComposition f ∘ g
`term_HO_4_lhs`	`LiteralExpression`
`literalValue`: p
`term_HO_4_rhs`	`LiteralExpression`
`literalValue`: ApplicationMorphism(partialBase(p), boundArguments(p))
`term_HO_4_forAll`	`ForAllDeclaration`
`variableName`: PartialApplication p with remainingArity = 0
`term_STR_1_lhs`	`LiteralExpression`
`literalValue`: reduction(e_k) converges to π
`term_STR_1_rhs`	`LiteralExpression`
`literalValue`: true
`term_STR_1_forAll`	`ForAllDeclaration`
`variableName`: Epoch e_k in ProductiveStream
`term_STR_2_lhs`	`LiteralExpression`
`literalValue`: saturation(continuationContext(b))
`term_STR_2_rhs`	`LiteralExpression`
`literalValue`: saturation(postContext(e_k))
`term_STR_2_forAll`	`ForAllDeclaration`
`variableName`: EpochBoundary b between e_k and e_{k+1}
`term_STR_3_lhs`	`LiteralExpression`
`literalValue`: computationTime(P)
`term_STR_3_rhs`	`LiteralExpression`
`literalValue`: Σ_{i=0}^{k−1} computationTime(epoch_i)
`term_STR_3_forAll`	`ForAllDeclaration`
`variableName`: StreamPrefix P of length k
`term_STR_4_lhs`	`LiteralExpression`
`literalValue`: epoch_0.context
`term_STR_4_rhs`	`LiteralExpression`
`literalValue`: seed
`term_STR_4_forAll`	`ForAllDeclaration`
`variableName`: Unfold(seed, step)
`term_STR_5_lhs`	`LiteralExpression`
`literalValue`: epoch_{k+1}.context
`term_STR_5_rhs`	`LiteralExpression`
`literalValue`: continuationContext(boundary(e_k))
`term_STR_5_forAll`	`ForAllDeclaration`
`variableName`: Unfold(seed, step), epoch e_k
`term_STR_6_lhs`	`LiteralExpression`
`literalValue`: linearBudget(epoch_{k+1})
`term_STR_6_rhs`	`LiteralExpression`
`literalValue`: linearBudget(epoch_k) + leaseCardinality(L)
`term_STR_6_forAll`	`ForAllDeclaration`
`variableName`: EpochBoundary b with LeaseAllocation L expiring at b
`term_FLR_1_lhs`	`LiteralExpression`
`literalValue`: result(P)
`term_FLR_1_rhs`	`LiteralExpression`
`literalValue`: ∈ {Success, Failure}
`term_FLR_1_forAll`	`ForAllDeclaration`
`variableName`: PartialComputation P
`term_FLR_2_lhs`	`LiteralExpression`
`literalValue`: result(T)
`term_FLR_2_rhs`	`LiteralExpression`
`literalValue`: Success
`term_FLR_2_forAll`	`ForAllDeclaration`
`variableName`: TotalComputation T
`term_FLR_3_lhs`	`LiteralExpression`
`literalValue`: result(A ⊗ B)
`term_FLR_3_rhs`	`LiteralExpression`
`literalValue`: Failure(A)
`term_FLR_3_forAll`	`ForAllDeclaration`
`variableName`: A ⊗ B where result(A) = Failure
`term_FLR_4_lhs`	`LiteralExpression`
`literalValue`: result(A ∥ B)
`term_FLR_4_rhs`	`LiteralExpression`
`literalValue`: Failure(A) (left component)
`term_FLR_4_forAll`	`ForAllDeclaration`
`variableName`: A ∥ B where result(A) = Failure, result(B) = Success
`term_FLR_5_lhs`	`LiteralExpression`
`literalValue`: result(apply(recoveryEffect(r), failureState(f)))
`term_FLR_5_rhs`	`LiteralExpression`
`literalValue`: ComputationResult
`term_FLR_5_forAll`	`ForAllDeclaration`
`variableName`: Recovery r on Failure f
`term_FLR_6_lhs`	`LiteralExpression`
`literalValue`: recoveryEffect(rollback(f))
`term_FLR_6_rhs`	`LiteralExpression`
`literalValue`: PhaseEffect(conjugate)
`term_FLR_6_forAll`	`ForAllDeclaration`
`variableName`: ComplexConjugateRollback on Failure f
`term_LN_1_lhs`	`LiteralExpression`
`literalValue`: Σ targetCount(site_i)
`term_LN_1_rhs`	`LiteralExpression`
`literalValue`: n
`term_LN_1_forAll`	`ForAllDeclaration`
`variableName`: LinearTrace T over n-bit type
`term_LN_2_lhs`	`LiteralExpression`
`literalValue`: status(f, postContext(e))
`term_LN_2_rhs`	`LiteralExpression`
`literalValue`: pinned
`term_LN_2_forAll`	`ForAllDeclaration`
`variableName`: LinearEffect e on site f
`term_LN_3_lhs`	`LiteralExpression`
`literalValue`: target(e′) = f
`term_LN_3_rhs`	`LiteralExpression`
`literalValue`: forbidden
`term_LN_3_forAll`	`ForAllDeclaration`
`variableName`: LinearEffect e on site f, any subsequent effect e′
`term_LN_4_lhs`	`LiteralExpression`
`literalValue`: remainingCount(budget after L)
`term_LN_4_rhs`	`LiteralExpression`
`literalValue`: remainingCount(budget before L) − k
`term_LN_4_forAll`	`ForAllDeclaration`
`variableName`: LeaseAllocation L with leaseCardinality k
`term_LN_5_lhs`	`LiteralExpression`
`literalValue`: remainingCount(budget after expiry)
`term_LN_5_rhs`	`LiteralExpression`
`literalValue`: remainingCount(budget before expiry) + leaseCardinality(L)
`term_LN_5_forAll`	`ForAllDeclaration`
`variableName`: Lease expiry on LeaseAllocation L
`term_LN_6_lhs`	`LiteralExpression`
`literalValue`: G
`term_LN_6_rhs`	`LiteralExpression`
`literalValue`: LinearTrace
`term_LN_6_forAll`	`ForAllDeclaration`
`variableName`: GeodesicTrace G
`term_SB_1_lhs`	`LiteralExpression`
`literalValue`: constraints(T₁)
`term_SB_1_rhs`	`LiteralExpression`
`literalValue`: ⊇ constraints(T₂)
`term_SB_1_forAll`	`ForAllDeclaration`
`variableName`: TypeInclusion T₁ ≤ T₂
`term_SB_2_lhs`	`LiteralExpression`
`literalValue`: resolutions(T₁)
`term_SB_2_rhs`	`LiteralExpression`
`literalValue`: ⊆ resolutions(T₂)
`term_SB_2_forAll`	`ForAllDeclaration`
`variableName`: TypeInclusion T₁ ≤ T₂, resolution R
`term_SB_3_lhs`	`LiteralExpression`
`literalValue`: N(C(T₂))
`term_SB_3_rhs`	`LiteralExpression`
`literalValue`: sub-complex of N(C(T₁))
`term_SB_3_forAll`	`ForAllDeclaration`
`variableName`: TypeInclusion T₁ ≤ T₂
`term_SB_4_lhs`	`LiteralExpression`
`literalValue`: F(T₁)
`term_SB_4_rhs`	`LiteralExpression`
`literalValue`: ≤ F(T₂)
`term_SB_4_forAll`	`ForAllDeclaration`
`variableName`: Covariant position F(_), T₁ ≤ T₂
`term_SB_5_lhs`	`LiteralExpression`
`literalValue`: F(T₂)
`term_SB_5_rhs`	`LiteralExpression`
`literalValue`: ≤ F(T₁)
`term_SB_5_forAll`	`ForAllDeclaration`
`variableName`: Contravariant position F(_), T₁ ≤ T₂
`term_SB_6_lhs`	`LiteralExpression`
`literalValue`: latticeDepth
`term_SB_6_rhs`	`LiteralExpression`
`literalValue`: n
`term_SB_6_forAll`	`ForAllDeclaration`
`variableName`: SubtypingLattice at quantum level n
`term_BR_1_lhs`	`LiteralExpression`
`literalValue`: measureValue(stepMeasurePost(s))
`term_BR_1_rhs`	`LiteralExpression`
`literalValue`: < measureValue(stepMeasurePre(s))
`term_BR_1_forAll`	`ForAllDeclaration`
`variableName`: RecursiveStep s
`term_BR_2_lhs`	`LiteralExpression`
`literalValue`: depth(RecursionTrace(R))
`term_BR_2_rhs`	`LiteralExpression`
`literalValue`: ≤ m
`term_BR_2_forAll`	`ForAllDeclaration`
`variableName`: BoundedRecursion R with initialMeasure m
`term_BR_3_lhs`	`LiteralExpression`
`literalValue`: terminates(R)
`term_BR_3_rhs`	`LiteralExpression`
`literalValue`: true
`term_BR_3_forAll`	`ForAllDeclaration`
`variableName`: BoundedRecursion R
`term_BR_4_lhs`	`LiteralExpression`
`literalValue`: initialMeasure(R)
`term_BR_4_rhs`	`LiteralExpression`
`literalValue`: structuralSize(T)
`term_BR_4_forAll`	`ForAllDeclaration`
`variableName`: StructuralRecursion R on type T
`term_BR_5_lhs`	`LiteralExpression`
`literalValue`: eval(p, state) = true
`term_BR_5_rhs`	`LiteralExpression`
`literalValue`: measureValue = 0
`term_BR_5_forAll`	`ForAllDeclaration`
`variableName`: BoundedRecursion R with basePredicate p
`term_RG_1_lhs`	`LiteralExpression`
`literalValue`: workingSetRegions(W)
`term_RG_1_rhs`	`LiteralExpression`
`literalValue`: computable from N(C(T)) and stage k site targets
`term_RG_1_forAll`	`ForAllDeclaration`
`variableName`: WorkingSet W for type T at stage k
`term_RG_2_lhs`	`LiteralExpression`
`literalValue`: ∀ a, b ∈ R: d_R(a, b)
`term_RG_2_rhs`	`LiteralExpression`
`literalValue`: ≤ diameter(R)
`term_RG_2_forAll`	`ForAllDeclaration`
`variableName`: AddressRegion R with LocalityMetric d_R
`term_RG_3_lhs`	`LiteralExpression`
`literalValue`: Σ workingSetSize(stage_k)
`term_RG_3_rhs`	`LiteralExpression`
`literalValue`: ≤ totalAddressableSpace(quantumLevel)
`term_RG_3_forAll`	`ForAllDeclaration`
`variableName`: RegionAllocation A for computation C
`term_RG_4_lhs`	`LiteralExpression`
`literalValue`: addresses accessed by resolver at stage k
`term_RG_4_rhs`	`LiteralExpression`
`literalValue`: ⊆ addresses(W_k)
`term_RG_4_forAll`	`ForAllDeclaration`
`variableName`: Reduction step k with WorkingSet W_k
`term_IO_1_lhs`	`LiteralExpression`
`literalValue`: type(resultDatum(e))
`term_IO_1_rhs`	`LiteralExpression`
`literalValue`: conformsTo(sourceType(s))
`term_IO_1_forAll`	`ForAllDeclaration`
`variableName`: IngestEffect e from Source s
`term_IO_2_lhs`	`LiteralExpression`
`literalValue`: type(emittedDatum(e))
`term_IO_2_rhs`	`LiteralExpression`
`literalValue`: conformsTo(sinkType(s))
`term_IO_2_forAll`	`ForAllDeclaration`
`variableName`: EmitEffect e to Sink s
`term_IO_3_lhs`	`LiteralExpression`
`literalValue`: apply(g, ingest(s))
`term_IO_3_rhs`	`LiteralExpression`
`literalValue`: Datum in R_n
`term_IO_3_forAll`	`ForAllDeclaration`
`variableName`: Source s with GroundingMap g
`term_IO_4_lhs`	`LiteralExpression`
`literalValue`: apply(p, d)
`term_IO_4_rhs`	`LiteralExpression`
`literalValue`: surface symbol conforming to sinkType(s)
`term_IO_4_forAll`	`ForAllDeclaration`
`variableName`: Sink s with ProjectionMap p, Datum d
`term_IO_5_lhs`	`LiteralExpression`
`literalValue`: effect:effectTarget(e)
`term_IO_5_rhs`	`LiteralExpression`
`literalValue`: non-empty EffectTarget
`term_IO_5_forAll`	`ForAllDeclaration`
`variableName`: BoundaryEffect e
`term_boundarySquaredZero_lhs`	`LiteralExpression`
`literalValue`: ∂_k(∂_{k+1}(c))
`term_boundarySquaredZero_rhs`	`LiteralExpression`
`literalValue`: 0
`term_boundarySquaredZero_forAll`	`ForAllDeclaration`
`variableName`: c ∈ C_{k+1}
`term_psi_4_lhs`	`LiteralExpression`
`literalValue`: β_k(K)
`term_psi_4_rhs`	`LiteralExpression`
`literalValue`: rank(H_k(K))
`term_psi_4_forAll`	`ForAllDeclaration`
`variableName`: simplicial complex K
`term_indexBridge_lhs`	`LiteralExpression`
`literalValue`: χ(K)
`term_indexBridge_rhs`	`LiteralExpression`
`literalValue`: Σ_k (-1)^k β_k
`term_indexBridge_forAll`	`ForAllDeclaration`
`variableName`: finite simplicial complex K
`term_coboundarySquaredZero_lhs`	`LiteralExpression`
`literalValue`: δ^{k+1}(δ^k(f))
`term_coboundarySquaredZero_rhs`	`LiteralExpression`
`literalValue`: 0
`term_coboundarySquaredZero_forAll`	`ForAllDeclaration`
`variableName`: f ∈ C^k
`term_deRhamDuality_lhs`	`LiteralExpression`
`literalValue`: H^k(K; R)
`term_deRhamDuality_rhs`	`LiteralExpression`
`literalValue`: Hom(H_k(K), R)
`term_deRhamDuality_forAll`	`ForAllDeclaration`
`variableName`: simplicial complex K, ring R
`term_sheafCohomologyBridge_lhs`	`LiteralExpression`
`literalValue`: H^k(K; F_R)
`term_sheafCohomologyBridge_rhs`	`LiteralExpression`
`literalValue`: H^k(K; R)
`term_sheafCohomologyBridge_forAll`	`ForAllDeclaration`
`variableName`: constant sheaf F_R over K
`term_localGlobalPrinciple_lhs`	`LiteralExpression`
`literalValue`: H^1(K; F) = 0
`term_localGlobalPrinciple_rhs`	`LiteralExpression`
`literalValue`: all local sections glue
`term_localGlobalPrinciple_forAll`	`ForAllDeclaration`
`variableName`: sheaf F over K

UOR Schema

Imports

Classes

Properties

Named Individuals

Related Concepts