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.

Imports

  • https://uor.foundation/u/

Classes

NameIRISubclass OfDisjoint WithComment
Datumhttps://uor.foundation/schema/Datumhttp://www.w3.org/2002/07/owl#Thinghttps://uor.foundation/schema/TermAn 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.
Termhttps://uor.foundation/schema/Termhttp://www.w3.org/2002/07/owl#Thinghttps://uor.foundation/schema/DatumA syntactic expression in the UOR term language. Terms are evaluated to produce Datums. Disjoint from Datum.
Triadhttps://uor.foundation/schema/Triadhttp://www.w3.org/2002/07/owl#ThingA three-component structure encoding an element's position in the UOR address space: stratum (ring layer), spectrum (bit pattern), and glyph (Braille address).
Literalhttps://uor.foundation/schema/Literalhttps://uor.foundation/schema/Term, https://uor.foundation/schema/SurfaceSymbolA 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.
Applicationhttps://uor.foundation/schema/Applicationhttps://uor.foundation/schema/TermA 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.
Ringhttps://uor.foundation/schema/Ringhttp://www.w3.org/2002/07/owl#ThingThe 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.
W16Ringhttps://uor.foundation/schema/W16Ringhttps://uor.foundation/schema/RingThe 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.
WittLevelhttps://uor.foundation/schema/WittLevelhttp://www.w3.org/2002/07/owl#ThingA 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 -> ...
TermExpressionhttps://uor.foundation/schema/TermExpressionhttp://www.w3.org/2002/07/owl#ThingRoot 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.
LiteralExpressionhttps://uor.foundation/schema/LiteralExpressionhttps://uor.foundation/schema/TermExpressionA leaf AST node: an integer literal, variable reference, or named constant.
ApplicationExpressionhttps://uor.foundation/schema/ApplicationExpressionhttps://uor.foundation/schema/TermExpressionAn AST node representing operator application: an operator applied to an argument list (e.g., add(x, y)).
InfixExpressionhttps://uor.foundation/schema/InfixExpressionhttps://uor.foundation/schema/TermExpressionAn AST node for infix relations and logical connectives (e.g., x <= y, P -> Q, a = b).
SetExpressionhttps://uor.foundation/schema/SetExpressionhttps://uor.foundation/schema/TermExpressionAn AST node for set-builder notation (e.g., {x : P(x)}).
CompositionExpressionhttps://uor.foundation/schema/CompositionExpressionhttps://uor.foundation/schema/TermExpressionAn AST node for function composition (f compose g).
ForAllDeclarationhttps://uor.foundation/schema/ForAllDeclarationhttp://www.w3.org/2002/07/owl#ThingA structured quantifier binding: typed variable declarations with a domain and quantifier kind (universal or existential). Replaces the string-valued op:forAll property.
VariableBindinghttps://uor.foundation/schema/VariableBindinghttp://www.w3.org/2002/07/owl#ThingA single variable binding: a variable name bound to a domain type (e.g., x in R_n).
QuantifierKindhttps://uor.foundation/schema/QuantifierKindhttp://www.w3.org/2002/07/owl#ThingThe kind of quantifier: Universal (forall) or Existential (exists). Controlled vocabulary with exactly 2 individuals.
SurfaceSymbolhttps://uor.foundation/schema/SurfaceSymbolhttp://www.w3.org/2002/07/owl#ThingAn 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.
HostValuehttps://uor.foundation/schema/HostValuehttps://uor.foundation/schema/SurfaceSymbolhttps://uor.foundation/schema/Term, https://uor.foundation/schema/DatumAn 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.
HostStringLiteralhttps://uor.foundation/schema/HostStringLiteralhttps://uor.foundation/schema/HostValueA host string literal carrying an xsd:string value.
HostBooleanLiteralhttps://uor.foundation/schema/HostBooleanLiteralhttps://uor.foundation/schema/HostValueA host boolean literal carrying an xsd:boolean value.

Properties

NameKindFunctionalDomainRangeComment
valueDatatypetruehttps://uor.foundation/schema/Datumhttp://www.w3.org/2001/XMLSchema#nonNegativeIntegerThe integer value of a datum element. For a Datum in Z/(2^n)Z, this is an integer in [0, 2^n).
wittLengthDatatypetruehttps://uor.foundation/schema/Datumhttp://www.w3.org/2001/XMLSchema#positiveIntegerThe 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.
stratumDatatypetruehttps://uor.foundation/schema/Datumhttp://www.w3.org/2001/XMLSchema#nonNegativeIntegerThe ring-layer index of a datum, indicating its position in the stratification of Z/(2^n)Z.
spectrumDatatypetruehttps://uor.foundation/schema/Datumhttp://www.w3.org/2001/XMLSchema#nonNegativeIntegerThe bit-pattern representation of a datum, encoding its position in the hypercube geometry of Z/(2^n)Z.
elementObjecttruehttps://uor.foundation/schema/Datumhttps://uor.foundation/u/ElementThe content-addressable element associated with this datum, linking the algebraic value to its identifier.
operatorObjecttruehttps://uor.foundation/schema/Applicationhttps://uor.foundation/op/OperationThe operation applied in an Application term.
argumentObjectfalsehttps://uor.foundation/schema/Applicationhttps://uor.foundation/schema/TermAn argument term in an Application. The ordering of arguments follows rdf:List semantics.
ringWittLengthDatatypetruehttps://uor.foundation/schema/Ringhttp://www.w3.org/2001/XMLSchema#positiveIntegerThe 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.
modulusDatatypetruehttps://uor.foundation/schema/Ringhttp://www.w3.org/2001/XMLSchema#positiveIntegerThe modulus 2^n of the ring. Equals 2 raised to the power of ringWittLength.
generatorObjecttruehttps://uor.foundation/schema/Ringhttps://uor.foundation/schema/DatumThe generator element π₁ (value = 1) of the ring. Under iterated successor application, π₁ generates all ring elements.
negationObjecttruehttps://uor.foundation/schema/Ringhttps://uor.foundation/op/InvolutionThe ring reflection involution: neg(x) = (-x) mod 2^n. One of the two generators of the dihedral group D_{2^n}.
complementObjecttruehttps://uor.foundation/schema/Ringhttps://uor.foundation/op/InvolutionThe hypercube reflection involution: bnot(x) = (2^n - 1) ⊕ x. The second generator of the dihedral group D_{2^n}.
denotesObjecttruehttps://uor.foundation/schema/Literalhttps://uor.foundation/schema/DatumThe 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.
bitsWidthDatatypetruehttps://uor.foundation/schema/WittLevelhttp://www.w3.org/2001/XMLSchema#positiveIntegerThe bit width 8*(k+1) of this Witt level.
cycleSizeDatatypetruehttps://uor.foundation/schema/WittLevelhttp://www.w3.org/2001/XMLSchema#positiveIntegerThe number of distinct states 2^(8*(k+1)) at this Witt level.
nextWittLevelObjecttruehttps://uor.foundation/schema/WittLevelhttps://uor.foundation/schema/WittLevelThe 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.
wittLevelPredecessorObjecttruehttps://uor.foundation/schema/WittLevelhttps://uor.foundation/schema/WittLevelThe 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).
atWittLevelObjecttruehttps://uor.foundation/schema/Ringhttps://uor.foundation/schema/WittLevelThe Witt level at which this Ring instance operates. Links a concrete Ring individual to its WittLevel.
W16bitWidthDatatypetruehttps://uor.foundation/schema/W16Ringhttp://www.w3.org/2001/XMLSchema#positiveIntegerBit width of the Q1 ring: 16.
W16capacityDatatypetruehttps://uor.foundation/schema/W16Ringhttp://www.w3.org/2001/XMLSchema#positiveIntegerCarrier set size of the Q1 ring: 65,536 elements.
boundVariablesObjectfalsehttps://uor.foundation/schema/ForAllDeclarationhttps://uor.foundation/schema/VariableBindingThe variable bindings in a quantifier declaration. Non-functional: a ForAllDeclaration may bind multiple variables.
variableDomainObjecttruehttps://uor.foundation/schema/VariableBindinghttp://www.w3.org/2002/07/owl#ClassThe domain type of a variable binding (e.g., schema:Ring, type:ConstrainedType).
variableNameDatatypetruehttps://uor.foundation/schema/VariableBindinghttp://www.w3.org/2001/XMLSchema#stringThe name of a bound variable (e.g., 'x', 'y', 'n').
quantifierKindObjecttruehttps://uor.foundation/schema/ForAllDeclarationhttps://uor.foundation/schema/QuantifierKindThe kind of quantifier: Universal or Existential.
expressionOperatorObjecttruehttps://uor.foundation/schema/ApplicationExpressionhttps://uor.foundation/op/OperationThe operator in an application expression (e.g., op:add, op:neg).
leftOperandObjecttruehttps://uor.foundation/schema/InfixExpressionhttps://uor.foundation/schema/TermExpressionThe left operand of an infix expression.
rightOperandObjecttruehttps://uor.foundation/schema/InfixExpressionhttps://uor.foundation/schema/TermExpressionThe right operand of an infix expression.
argumentsObjectfalsehttps://uor.foundation/schema/ApplicationExpressionhttps://uor.foundation/schema/TermExpressionThe argument list of an application expression. Non-functional: an application may take multiple arguments.
literalValueDatatypetruehttps://uor.foundation/schema/LiteralExpressionhttp://www.w3.org/2001/XMLSchema#stringThe string representation of a literal expression value (e.g., '42', 'x', 'pi1').
infixOperatorDatatypetruehttps://uor.foundation/schema/InfixExpressionhttp://www.w3.org/2001/XMLSchema#stringThe operator symbol in an infix expression (e.g., '=', '\u{2264}', '\u{2192}').
hostStringDatatypetruehttps://uor.foundation/schema/HostStringLiteralhttp://www.w3.org/2001/XMLSchema#stringThe string value carried by a HostStringLiteral.
hostBooleanDatatypetruehttps://uor.foundation/schema/HostBooleanLiteralhttp://www.w3.org/2001/XMLSchema#booleanThe boolean value carried by a HostBooleanLiteral.

Named Individuals

NameTypePropertiesComment
Universalhttps://uor.foundation/schema/QuantifierKind—Universal quantification (forall).
Existentialhttps://uor.foundation/schema/QuantifierKind—Existential quantification (exists).
π₁https://uor.foundation/schema/Datum
  • value: 1
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.
zerohttps://uor.foundation/schema/Datum
  • value: 0
The additive identity of the ring. Value = 0 at every Witt level. op:add(x, zero) = x for all x in R_n.
W8https://uor.foundation/schema/WittLevel
  • bitsWidth: 8
  • cycleSize: 256
  • nextWittLevel: https://uor.foundation/schema/W16
Witt level 0: 8-bit ring Z/256Z, 256 states. The reference level for all ComputationCertificate proofs in the spec.
W16https://uor.foundation/schema/WittLevel
  • bitsWidth: 16
  • cycleSize: 65536
  • nextWittLevel: https://uor.foundation/schema/W24
  • wittLevelPredecessor: https://uor.foundation/schema/W8
Witt level 1: 16-bit ring Z/65536Z, 65,536 states.
W24https://uor.foundation/schema/WittLevel
  • bitsWidth: 24
  • cycleSize: 16777216
  • nextWittLevel: https://uor.foundation/schema/W32
  • wittLevelPredecessor: https://uor.foundation/schema/W16
Witt level 2: 24-bit ring Z/16777216Z, 16,777,216 states.
W32https://uor.foundation/schema/WittLevel
  • bitsWidth: 32
  • cycleSize: 4294967296
  • wittLevelPredecessor: https://uor.foundation/schema/W24
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.
term_criticalIdentity_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_AD_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: addresses(glyph(d))
term_AD_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d
term_AD_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: d ∈ R_n
term_AD_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: glyph(ι(addresses(a)))
term_AD_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ι_addr(a)
term_AD_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: a ∈ Addr(R_n), ι : R_n → R_{n'}
term_R_A1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: add(x, add(y, z))
term_R_A1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: add(add(x, y), z)
term_R_A1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y, z ∈ R_n
term_R_A2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: add(x, 0)
term_R_A2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x
term_R_A2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_R_A3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: add(x, neg(x))
term_R_A3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 0
term_R_A3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_R_A4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: add(x, y)
term_R_A4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: add(y, x)
term_R_A4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_R_A5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: sub(x, y)
term_R_A5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: add(x, neg(y))
term_R_A5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_R_A6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: neg(neg(x))
term_R_A6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x
term_R_A6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_R_M1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: mul(x, mul(y, z))
term_R_M1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: mul(mul(x, y), z)
term_R_M1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y, z ∈ R_n
term_R_M2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: mul(x, 1)
term_R_M2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x
term_R_M2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_R_M3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: mul(x, y)
term_R_M3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: mul(y, x)
term_R_M3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_R_M4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: mul(x, add(y, z))
term_R_M4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: add(mul(x, y), mul(x, z))
term_R_M4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y, z ∈ R_n
term_R_M5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: mul(x, 0)
term_R_M5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 0
term_R_M5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_B_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: xor(x, xor(y, z))
term_B_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: xor(xor(x, y), z)
term_B_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y, z ∈ R_n
term_B_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: xor(x, 0)
term_B_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x
term_B_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_B_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: xor(x, x)
term_B_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 0
term_B_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_B_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: and(x, and(y, z))
term_B_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: and(and(x, y), z)
term_B_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y, z ∈ R_n
term_B_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: and(x, 2^n - 1)
term_B_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x
term_B_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_B_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: and(x, 0)
term_B_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 0
term_B_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_B_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: or(x, or(y, z))
term_B_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: or(or(x, y), z)
term_B_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y, z ∈ R_n
term_B_8_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: or(x, 0)
term_B_8_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x
term_B_8_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_B_9_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: and(x, or(x, y))
term_B_9_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x
term_B_9_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_B_10_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: and(x, or(y, z))
term_B_10_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: or(and(x, y), and(x, z))
term_B_10_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y, z ∈ R_n
term_B_11_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: bnot(and(x, y))
term_B_11_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: or(bnot(x), bnot(y))
term_B_11_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_B_12_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: bnot(or(x, y))
term_B_12_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: and(bnot(x), bnot(y))
term_B_12_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_B_13_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: bnot(bnot(x))
term_B_13_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x
term_B_13_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_X_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: neg(x)
term_X_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: sub(0, x)
term_X_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_X_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: bnot(x)
term_X_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: xor(x, 2^n - 1)
term_X_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_X_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: succ(x)
term_X_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: add(x, 1)
term_X_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_X_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pred(x)
term_X_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: sub(x, 1)
term_X_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_X_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: neg(x)
term_X_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: add(bnot(x), 1)
term_X_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_X_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: bnot(x)
term_X_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pred(neg(x))
term_X_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_X_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: xor(x, y)
term_X_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: add(x, y) - 2 * and(x, y)
term_X_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ Z (before mod)
term_D_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: succ^{2^n}(x)
term_D_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x
term_D_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_D_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: neg(succ(neg(x)))
term_D_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pred(x)
term_D_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_D_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: bnot(neg(x))
term_D_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pred(x)
term_D_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_D_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: D_{2^n}
term_D_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: {succ^k, neg ∘ succ^k : 0 ≤ k < 2^n}
term_D_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: n ≥ 1
term_U_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: R_n×
term_U_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Z/2 × Z/2^{n-2}
term_U_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: n ≥ 3
term_U_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: R_1× ≅ {1}; R_2× ≅ Z/2
term_U_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: special cases for small n
term_U_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: n ∈ {1, 2}
term_U_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ord(u)
term_U_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: lcm(ord((-1)^a), ord(3^b))
term_U_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: u = (-1)^a · 3^b ∈ R_n×
term_U_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ord_g(2)
term_U_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: divides φ(g)
term_U_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: g odd
term_U_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: step_g
term_U_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 2 * ((g - (2^n mod g)) mod g) + 1
term_U_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: g odd, g > 1
term_AG_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: μ_u
term_AG_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∉ D_{2^n}
term_AG_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: u ∈ R_n×, u ≠ ±1
term_AG_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Aff(R_n)
term_AG_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: R_n× ⋉ R_n
term_AG_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: n ≥ 1
term_AG_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: |Aff(R_n)|
term_AG_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 2^{2n-1}
term_AG_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: n ≥ 1
term_AG_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: D_{2^n}
term_AG_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ⊂ Aff(R_n), u ∈ {±1}
term_AG_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: n ≥ 1
term_CA_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: add(x,y)_k
term_CA_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: xor(x_k, xor(y_k, c_k(x,y)))
term_CA_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n, 0 ≤ k < n
term_CA_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: c_{k+1}(x,y)
term_CA_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: or(and(x_k,y_k), and(xor(x_k,y_k), c_k))
term_CA_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_CA_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: c(x, y)
term_CA_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: c(y, x)
term_CA_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_CA_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: c(x, 0)
term_CA_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 0
term_CA_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n, all positions
term_CA_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: c(x, neg(x))_k
term_CA_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 1
term_CA_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n, k > v_2(x)
term_CA_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_Δ(x, y) > 0
term_CA_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∃ k : c_k(x,y) = 1
term_CA_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_C_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pins(compose(A, B))
term_C_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pins(A) ∪ pins(B)
term_C_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraints A, B
term_C_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: compose(A, B)
term_C_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: compose(B, A)
term_C_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraints A, B
term_C_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: compose(compose(A,B), C)
term_C_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: compose(A, compose(B,C))
term_C_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraints A, B, C
term_C_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: compose(A, A)
term_C_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: A
term_C_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint A
term_C_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: compose(A, ε)
term_C_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: A
term_C_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint A, identity ε
term_C_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: compose(A, Ω)
term_C_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Ω
term_C_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint A, annihilator Ω
term_CDI_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: carry(residue(T))
term_CDI_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: depth(T)
term_CDI_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T ∈ T_n
term_CL_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Constraint/≡
term_CL_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 2^{[n]}
term_CL_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint equivalence classes
term_CL_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: A ∨ B
term_CL_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: compose(A, B)
term_CL_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraints A, B
term_CL_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pins(A ∧ B)
term_CL_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pins(A) ∩ pins(B)
term_CL_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraints A, B
term_CL_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: (A ∨ B) ∧ C
term_CL_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: (A ∧ C) ∨ (B ∧ C)
term_CL_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraints A, B, C
term_CL_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: A ∧ A̅ = ε, A ∨ A̅ = Ω
term_CL_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∃ A̅ (complement)
term_CL_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint A
term_CM_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: C_i redundant in {C_1,...,C_k}
term_CM_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pins(C_i) ⊆ ∪_{j≠i} pins(C_j)
term_CM_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint set {C_1,...,C_k}
term_CM_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: minimal cover
term_CM_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: irredundant sub-collection (greedy removal)
term_CM_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: CompositeConstraint
term_CM_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: min constraints to cover n sites
term_CM_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ⌈n / max_k pins_per_constraint_k⌉
term_CM_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: n sites, constraint set
term_CR_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cost(ResidueConstraint(m, r))
term_CR_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: step_m = 2 × ((−2^n) mod m) + 1
term_CR_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ResidueConstraint
term_CR_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cost(CarryConstraint(p))
term_CR_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: popcount(p)
term_CR_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: CarryConstraint
term_CR_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cost(DepthConstraint(d_min, d_max))
term_CR_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cost(residue) + cost(carry)
term_CR_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: DepthConstraint
term_CR_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cost(compose(A, B))
term_CR_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ cost(A) + cost(B)
term_CR_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraints A, B
term_CR_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: optimal resolution order
term_CR_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: increasing cost order
term_CR_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint set
term_F_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pinned site
term_F_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cannot be unpinned
term_F_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: SiteIndex
term_F_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pin operations to close
term_F_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ n
term_F_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: FreeRank
term_F_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pinnedCount + freeRank
term_F_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: totalSites = n
term_F_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: FreeRank
term_F_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: isClosed
term_F_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRank = 0 ⇔ pinnedCount = n
term_F_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: FreeRank
term_FL_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ⊥
term_FL_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: all sites free (freeRank = n)
term_FL_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: FreeRank lattice
term_FL_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ⊤
term_FL_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: all sites pinned (pinnedCount = n)
term_FL_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: FreeRank lattice
term_FL_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: join(S₁, S₂)
term_FL_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: union of pinnings from S₁ and S₂
term_FL_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: FreeRank states S₁, S₂
term_FL_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: lattice height
term_FL_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: n
term_FL_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: FreeRank lattice
term_FPM_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x ∈ Unit
term_FPM_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: site_0(x) = 1 (x is odd)
term_FPM_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_FPM_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x ∈ Exterior
term_FPM_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x ∉ carrier(T)
term_FPM_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n, type T
term_FPM_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x ∈ Irreducible
term_FPM_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x ∉ Unit ∪ Exterior AND no non-trivial factorization
term_FPM_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_FPM_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x ∈ Reducible
term_FPM_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x ∉ Unit ∪ Exterior ∪ Irreducible
term_FPM_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_FPM_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x = 2^{v(x)} ⋅ u
term_FPM_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: u odd, v(x) = min position of 1-bit
term_FPM_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_FPM_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: |{x: v(x) = k}|
term_FPM_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 2^{n−k−1} for 0 < k < n; 1 for k = n
term_FPM_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: R_n
term_FPM_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: base type partition
term_FPM_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: |Unit| = 2^{n−1}; |Irr| = 2^{n−2}; |Red| = 2^{n−2}
term_FPM_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: R_n, n ≥ 3
term_FS_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: site_k(x)
term_FS_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: (x >> k) AND 1
term_FS_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n, 0 ≤ k < n
term_FS_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: site_0(x)
term_FS_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x mod 2 (parity)
term_FS_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_FS_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: site_k(x) given sites 0..k−1
term_FS_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: determines x mod 2^{k+1}
term_FS_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_FS_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: sites 0..k together
term_FS_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: determine x mod 2^{k+1}
term_FS_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_FS_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: all n sites
term_FS_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: determine x uniquely
term_FS_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_FS_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: stratum(x)
term_FS_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: v_2(x) = min{k : site_k(x) = 1}
term_FS_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_FS_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: depth(x)
term_FS_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ v_2(x) for irreducible elements
term_FS_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n, base type
term_RE_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Π_D(T)
term_RE_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Π_C(T) = Π_E(T)
term_RE_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T ∈ T_n
term_IR_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pinnedCount(state_{i+1})
term_IR_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≥ pinnedCount(state_i)
term_IR_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: resolution states
term_IR_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: iterations to converge
term_IR_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ n
term_IR_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: resolution loop
term_IR_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: convergenceRate
term_IR_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pinnedCount / iterationCount
term_IR_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ResolutionState
term_IR_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: constraint set spans all sites
term_IR_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: loop terminates
term_IR_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: complete constraint set
term_SF_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: n ≡ 0 (mod ord_g(2))
term_SF_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: factor g has optimal resolution at level n
term_SF_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: factor g, quantum n
term_SF_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: constraints with smaller step_g
term_SF_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: are more constraining, apply first
term_SF_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint ordering
term_RD_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: same type T and constraint sequence
term_RD_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: unique resolved partition
term_RD_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T ∈ T_n, [C₁,...,Cₖ]
term_RD_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: complete constraint set, any order
term_RD_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: same final partition
term_RD_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: closing constraint set
term_SE_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: EvaluationResolver
term_SE_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: directly computes set-theoretic partition
term_SE_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T ∈ T_n
term_SE_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: DihedralFactorizationResolver
term_SE_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: orbit decomposition yields same partition
term_SE_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T ∈ T_n
term_SE_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: CanonicalFormResolver
term_SE_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: confluent rewrite → same partition
term_SE_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T ∈ T_n
term_SE_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Π_D(T) = Π_C(T) = Π_E(T)
term_SE_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: all compute same set-theoretic partition
term_SE_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T ∈ T_n
term_OO_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: benefit(C_i, S)
term_OO_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: |pins(C_i) ∖ S|
term_OO_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint C_i, pinned set S
term_OO_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cost(C_i)
term_OO_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: step_{m_i} or popcount(p_i)
term_OO_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ResidueConstraint or CarryConstraint
term_OO_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: greedy selection
term_OO_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: argmax benefit(C_i, S) / cost(C_i)
term_OO_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: each resolution step
term_OO_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: greedy approximation
term_OO_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: (1 − 1/e) ≈ 63% of optimal
term_OO_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: weighted set cover
term_OO_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: equal cost tiebreaker
term_OO_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: prefer vertical (residue) before horizontal (carry)
term_OO_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: cost-tied constraints
term_CB_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: min convergenceRate
term_CB_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 1 site per iteration
term_CB_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: worst case
term_CB_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: max convergenceRate
term_CB_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: n sites in 1 iteration
term_CB_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: best case
term_CB_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: expected rate (residue)
term_CB_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ⌊log_2(m)⌋ sites per constraint
term_CB_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ResidueConstraint(m, r)
term_CB_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: convergenceRate < 1 for 2 iterations
term_CB_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: constraint set may be insufficient
term_CB_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: stall detection
term_CB_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∪_i pins(C_i) = {0,...,n−1}
term_CB_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: constraint set closes budget
term_CB_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: sufficiency criterion
term_CB_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: iterations for k constraints
term_CB_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ min(k, n)
term_CB_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: well-formed model
term_OB_M1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_R(x, z)
term_OB_M1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ d_R(x, y) + d_R(y, z)
term_OB_M1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y, z ∈ R_n
term_OB_M2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_H(x, z)
term_OB_M2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ d_H(x, y) + d_H(y, z)
term_OB_M2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y, z ∈ R_n
term_OB_M3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_Δ(x, y)
term_OB_M3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: |d_R(x, y) − d_H(x, y)|
term_OB_M3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_OB_M4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_R(neg(x), neg(y))
term_OB_M4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_R(x, y)
term_OB_M4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_OB_M5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_H(bnot(x), bnot(y))
term_OB_M5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_H(x, y)
term_OB_M5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_OB_M6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_R(succ(x), succ(y))
term_OB_M6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_R(x, y) but d_H may differ
term_OB_M6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_OB_C1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: [neg, bnot](x)
term_OB_C1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 2
term_OB_C1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_OB_C2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: [neg, add(•,k)](x)
term_OB_C2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: −2k mod 2^n
term_OB_C2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n, constant k
term_OB_C3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: [bnot, xor(•,k)](x)
term_OB_C3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 0
term_OB_C3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n, constant k
term_OB_H1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: closed additive path monodromy
term_OB_H1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: trivial (abelian ⇒ path-independent)
term_OB_H1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: additive group
term_OB_H2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: closed {neg,bnot} path monodromy
term_OB_H2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∈ D_{2^n}
term_OB_H2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: dihedral generators
term_OB_H3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: succ-only path WindingNumber
term_OB_H3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: path length / 2^n
term_OB_H3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: closed succ path
term_OB_P1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: PathLength(p₁ ⋅ p₂)
term_OB_P1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: PathLength(p₁) + PathLength(p₂)
term_OB_P1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: paths p₁, p₂
term_OB_P2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: TotalVariation(p₁ ⋅ p₂)
term_OB_P2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ TotalVariation(p₁) + TotalVariation(p₂)
term_OB_P2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: paths p₁, p₂
term_OB_P3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ReductionLength(c₁ ; c₂)
term_OB_P3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ReductionLength(c₁) + ReductionLength(c₂)
term_OB_P3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: reductions c₁, c₂
term_CT_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: catastrophe boundaries
term_CT_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: g = 2^k for 1 ≤ k ≤ n−1
term_CT_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: stratum transitions
term_CT_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: odd prime catastrophe
term_CT_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ResidueConstraint(p, •) transitions visibility
term_CT_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: odd prime p
term_CT_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: CatastropheThreshold(g)
term_CT_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: step_g / n
term_CT_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: factor g
term_CT_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: composite catastrophe g = p⋅q
term_CT_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: max(step_p, step_q) / n
term_CT_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: composite g
term_CF_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: CurvatureFlux(γ)
term_CF_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σ |d_R(x_i, x_{i+1}) − d_H(x_i, x_{i+1})|
term_CF_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: path γ
term_CF_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ResolutionCost(T)
term_CF_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≥ CurvatureFlux(γ_opt)
term_CF_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: type T
term_CF_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: CurvatureFlux(x, succ(x))
term_CF_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: trailing_ones(x) for t < n; n−1 for x = 2^n−1
term_CF_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_CF_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σ_{x ∈ R_n} CurvatureFlux(x, succ(x))
term_CF_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 2^n − 2
term_CF_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: n ≥ 1
term_HG_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: additive holonomy
term_HG_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: trivial (abelian ⇒ path-independent)
term_HG_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: additive group
term_HG_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: {neg, bnot, succ, pred} holonomy
term_HG_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: D_{2^n}
term_HG_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: dihedral generators
term_HG_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: {mul(•, u) : u ∈ R_n×} holonomy
term_HG_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: R_n× ≅ Z/2 × Z/2^{n−2}
term_HG_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: unit group
term_HG_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Hol(R_n)
term_HG_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Aff(R_n) = R_n× ⋉ R_n
term_HG_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: n ≥ 1
term_HG_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Hol(R_n) decomposition
term_HG_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: D_{2^n} ⋅ {mul(•,u) : u ∈ R_n×, u ≠ ±1}
term_HG_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: n ≥ 1
term_T_C1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: compose(id, f)
term_T_C1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: f
term_T_C1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: f ∈ Transform
term_T_C2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: compose(f, id)
term_T_C2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: f
term_T_C2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: f ∈ Transform
term_T_C3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: compose(f, compose(g, h))
term_T_C3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: compose(compose(f, g), h)
term_T_C3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: f, g, h ∈ Transform
term_T_C4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: f composesWith g
term_T_C4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: target(f) = source(g)
term_T_C4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: f, g ∈ Transform
term_T_I1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_R(neg(x), neg(y))
term_T_I1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_R(x, y)
term_T_I1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_T_I2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_H(bnot(x), bnot(y))
term_T_I2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_H(x, y)
term_T_I2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_T_I3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: succ = neg ∘ bnot
term_T_I3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: preserves d_R but not d_H
term_T_I3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_T_I4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ring isometries
term_T_I4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: form a group under composition
term_T_I4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Isometry
term_T_I5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: CurvatureObservable
term_T_I5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: measures failure of ring isometry to be Hamming isometry
term_T_I5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Isometry
term_T_E1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ι(x) = ι(y)
term_T_E1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x = y
term_T_E1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n (injectivity)
term_T_E2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ι(add(x,y))
term_T_E2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: add(ι(x), ι(y)); ι(mul(x,y)) = mul(ι(x), ι(y))
term_T_E2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_T_E3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ι₂ ∘ ι₁ : R_n → R_k
term_T_E3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: is an embedding (transitivity)
term_T_E3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ι₁: R_n → R_m, ι₂: R_m → R_k
term_T_E4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: glyph ∘ ι ∘ addresses
term_T_E4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: well-defined
term_T_E4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: embedding ι
term_T_A1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: g ∈ D_{2^n} on Constraint C
term_T_A1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: g⋅C (transformed constraint)
term_T_A1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: g ∈ D_{2^n}, C ∈ Constraint
term_T_A2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: g ∈ D_{2^n} on Partition
term_T_A2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: permutes components
term_T_A2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: g ∈ D_{2^n}
term_T_A3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: D_{2^n} orbits on R_n
term_T_A3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: determine irreducibility boundaries
term_T_A3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: DihedralFactorizationResolver
term_T_A4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: fixed points of neg
term_T_A4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: {0, 2^{n−1}}; bnot has none (n > 0)
term_T_A4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: R_n
term_AU_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Aut(R_n)
term_AU_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: {μ_u : x ↦ mul(u, x) | u ∈ R_n×}
term_AU_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: n ≥ 1
term_AU_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Aut(R_n)
term_AU_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≅ R_n× ≅ Z/2 × Z/2^{n−2}
term_AU_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: n ≥ 3
term_AU_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: |Aut(R_n)|
term_AU_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 2^{n−1}
term_AU_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: n ≥ 1
term_AU_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Aut(R_n) ∩ D_{2^n}
term_AU_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: {id, neg}
term_AU_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: n ≥ 1
term_AU_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Aff(R_n)
term_AU_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ⟨D_{2^n}, μ_3⟩
term_AU_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: n ≥ 1
term_EF_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: F_ι(f)
term_EF_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ι ∘ f ∘ ι⁻¹ on Im(ι)
term_EF_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ι: R_n → R_m, f ∈ Cat(R_n)
term_EF_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: F_ι(f ∘ g)
term_EF_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: F_ι(f) ∘ F_ι(g)
term_EF_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ι: R_n → R_m
term_EF_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: F_ι(id_{R_n})
term_EF_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: id_{Im(ι)}
term_EF_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ι: R_n → R_m
term_EF_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: F_{ι₂ ∘ ι₁}
term_EF_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: F_{ι₂} ∘ F_{ι₁}
term_EF_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ι₁: R_n → R_m, ι₂: R_m → R_k
term_EF_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: F_ι(ring isometry)
term_EF_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ring isometry at level m
term_EF_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ι: R_n → R_m
term_EF_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: F_ι(D_{2^n})
term_EF_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ⊆ D_{2^m} as subgroup
term_EF_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ι: R_n → R_m
term_EF_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: F_ι(R_n×)
term_EF_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ⊆ R_m× as subgroup
term_EF_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ι: R_n → R_m
term_AA_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: glyph(x)
term_AA_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: [braille(x[0:5]), braille(x[6:11]), ...]
term_AA_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n (6-bit blocks)
term_AA_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: braille(a ⊕ b)
term_AA_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: braille(a) ⊕ braille(b)
term_AA_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: a, b ∈ {0,1}^6
term_AA_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: glyph(bnot(x))
term_AA_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: complement each Braille character of glyph(x)
term_AA_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_AA_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: glyph(add(x, y))
term_AA_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≠ f(glyph(x), glyph(y)) in general
term_AA_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_AA_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: liftable operations
term_AA_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: {xor, and, or, bnot}; NOT {add, sub, mul, neg, succ, pred}
term_AA_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: operations on R_n
term_AA_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: neg(x) = succ(bnot(x))
term_AA_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: bnot lifts, succ does not
term_AA_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_AM_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_addr(a, b)
term_AM_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σ_i popcount(braille_i(a) ⊕ braille_i(b))
term_AM_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: addresses a, b
term_AM_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_addr(glyph(x), glyph(y))
term_AM_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_H(x, y)
term_AM_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_AM_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_addr
term_AM_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: does NOT preserve d_R in general
term_AM_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: addresses
term_AM_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_Δ(x, y)
term_AM_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: |d_R(x,y) − d_addr(glyph(x), glyph(y))|
term_AM_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_TH_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: S(state)
term_TH_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRank × ln 2
term_TH_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: state ∈ FreeRank
term_TH_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: S(⊥)
term_TH_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: n × ln 2
term_TH_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: unconstrained type
term_TH_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: S(⊤)
term_TH_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 0
term_TH_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: fully resolved type
term_TH_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: total resolution cost
term_TH_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: n × k_B T × ln 2
term_TH_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Landauer bound
term_TH_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: β*
term_TH_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ln 2
term_TH_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: UOR site system
term_TH_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: constraint application
term_TH_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: removes entropy; convergenceRate = cooling rate
term_TH_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: resolution loop
term_TH_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: CatastropheThreshold
term_TH_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: temperature of partition phase transition
term_TH_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: partition bifurcation
term_TH_8_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: step_g
term_TH_8_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: free-energy cost of constraint boundary
term_TH_8_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint boundary g
term_TH_9_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: computational hardness
term_TH_9_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: type incompleteness (high temperature)
term_TH_9_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: type specification
term_TH_10_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: type resolution
term_TH_10_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: measurement; cost ≥ entropy removed
term_TH_10_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: resolution process
term_AR_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: adiabatic schedule
term_AR_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: decreasing freeRank × cost-per-site order
term_AR_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint ordering
term_AR_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Cost_adiabatic
term_AR_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σ_i cost(C_{σ(i)}) where σ is optimal
term_AR_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: optimal ordering
term_AR_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Cost_adiabatic
term_AR_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≥ n × k_B T × ln 2
term_AR_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Landauer bound
term_AR_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: η = (n × ln 2) / Cost_adiabatic
term_AR_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ 1
term_AR_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: adiabatic efficiency
term_AR_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: greedy vs adiabatic difference
term_AR_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ 5% for n ≤ 16
term_AR_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: empirical, Q0–Q4
term_PD_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: phase space
term_PD_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: {(n, g) : n ∈ Z₊, g constraint boundary}
term_PD_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: UOR phase diagram
term_PD_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: phase boundaries
term_PD_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: g | (2^n − 1) or g = 2^k
term_PD_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: (n, g) plane
term_PD_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: parity boundary
term_PD_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: |Unit| = 2^{n−1}, |non-Unit| = 2^{n−1}
term_PD_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: g = 2
term_PD_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: resonance lines
term_PD_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: n = k ⋅ ord_g(2)
term_PD_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: (n, g) plane
term_PD_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: phase count at level n
term_PD_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ 2^n (typical O(n))
term_PD_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: quantum level n
term_RC_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: reversible pinning of site k
term_RC_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: store prior state in ancilla site k'
term_RC_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: SiteIndex k
term_RC_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: reversible pinning entropy
term_RC_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ΔS_total = 0
term_RC_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: reversible strategy
term_RC_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: deferred Landauer cost
term_RC_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: n × k_B T × ln 2 at ancilla erasure
term_RC_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ancilla cleanup
term_RC_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: reversible total cost
term_RC_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: = irreversible total cost (redistributed)
term_RC_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: reversible strategy
term_RC_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: quantum UOR
term_RC_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: superposed sites, cost ∝ winning path
term_RC_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: hypothetical quantum
term_DC_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∂_R f(x)
term_DC_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: f(succ(x)) - f(x)
term_DC_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: f : R_n → R_n, x ∈ R_n
term_DC_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∂_H f(x)
term_DC_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: f(bnot(x)) - f(x)
term_DC_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: f : R_n → R_n, x ∈ R_n
term_DC_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∂_H id(x)
term_DC_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: bnot(x) - x = -(2x + 1) mod 2^n
term_DC_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_DC_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: [neg, bnot](x)
term_DC_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∂_R neg(x) - ∂_H neg(x)
term_DC_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_DC_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∂_R f - ∂_H f
term_DC_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σ carry contributions
term_DC_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: f : R_n → R_n
term_DC_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: J_k(x)
term_DC_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∂_R f_k(x) where f_k = site_k
term_DC_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n, 0 ≤ k < n
term_DC_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: J_{n-1}(x)
term_DC_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: may differ from lower sites
term_DC_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_DC_8_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: rank(J(x))
term_DC_8_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: = d_H(x, succ(x)) - 1 for generic x
term_DC_8_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_DC_9_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: κ(x)
term_DC_9_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σ_k J_k(x)
term_DC_9_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n
term_DC_10_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: optimal next constraint
term_DC_10_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: argmax J_k over free sites
term_DC_10_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: resolution step
term_DC_11_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σ_{x} J_k(x)
term_DC_11_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≈ (2^n - 2)/n for each k
term_DC_11_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: 0 ≤ k < n
term_HA_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: N(C)
term_HA_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: simplicial complex on constraints
term_HA_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint set C
term_HA_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: resolution stalls
term_HA_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ⟺ H_k(N(C)) ≠ 0 for some k > 0
term_HA_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint set C
term_HA_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: S_residual
term_HA_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≥ Σ_k β_k × ln 2
term_HA_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint configuration C
term_IT_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: χ(N(C))
term_IT_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σ_k (-1)^k β_k
term_IT_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint nerve N(C)
term_IT_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: χ(N(C))
term_IT_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σ_k (-1)^k dim(H_k)
term_IT_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint nerve N(C)
term_IT_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: λ_1(N(C))
term_IT_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: lower bounds convergence rate
term_IT_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint nerve N(C)
term_IT_7a_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σ κ_k - χ(N(C))
term_IT_7a_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: = S_residual / ln 2
term_IT_7a_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint configuration C
term_IT_7b_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: S_residual
term_IT_7b_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: = (Σ κ_k - χ) × ln 2
term_IT_7b_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint configuration C
term_IT_7c_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: resolution cost
term_IT_7c_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≥ n - χ(N(C))
term_IT_7c_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint configuration C
term_IT_7d_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: resolution complete
term_IT_7d_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ⟺ χ(N(C)) = n and all β_k = 0
term_IT_7d_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint nerve N(C)
term_phi_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: φ₁(neg, ResidueConstraint(m,r))
term_phi_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ResidueConstraint(m, m-r)
term_phi_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ring op, constraint
term_phi_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: φ₂(compose(A,B))
term_phi_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: φ₂(A) ∪ φ₂(B)
term_phi_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraints A, B
term_phi_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: φ₃(closed site state)
term_phi_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: unique 4-component partition
term_phi_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: closed FreeRank
term_phi_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: φ₄(T, x)
term_phi_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: φ₃(φ₂(φ₁(T, x)))
term_phi_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T ∈ T_n, x ∈ R_n
term_phi_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: φ₅(neg)
term_phi_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: preserves d_R, may change d_H
term_phi_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: op ∈ Operation
term_phi_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: φ₆(state, observables)
term_phi_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: RefinementSuggestion
term_phi_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ResolutionState
term_psi_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: N(constraints)
term_psi_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: SimplicialComplex
term_psi_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint set
term_psi_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: C(K)
term_psi_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ChainComplex
term_psi_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: simplicial complex K
term_psi_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: H_k(C)
term_psi_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ker(∂_k) / im(∂_{k+1})
term_psi_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: chain complex C
term_psi_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: C^k
term_psi_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Hom(C_k, R)
term_psi_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: chain complex C, ring R
term_psi_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: H^k(C)
term_psi_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ker(δ^k) / im(δ^{k-1})
term_psi_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: cochain complex C
term_surfaceSymmetry_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: P(Π(G(s)))
term_surfaceSymmetry_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: s' where type(s') ≡ type(s) under F.constraint
term_surfaceSymmetry_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: G: GroundingMap, P: ProjectionMap, F: Frame, s: Literal, G.symbolConstraints = P.projectionOrder
term_CC_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: resolution(x, T)
term_CC_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: O(1) for CompleteType T
term_CC_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n, T: CompleteType
term_CC_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: completeness(T)
term_CC_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: implies completeness(T')
term_CC_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T, T': ConstrainedType, T ⊆ T'
term_CC_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: sitesClosed(W₁) + sitesClosed(W₂)
term_CC_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: = n for valid concat(W₁, W₂)
term_CC_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: W₁, W₂: CompletenessWitness
term_CC_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: CompletenessResolver
term_CC_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: fix(ψ-pipeline, CompletenessCandidate)
term_CC_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: CompletenessCandidate
term_CC_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cert.verified = true
term_CC_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: implies χ(N(C)) = n ∧ ∀k: β_k = 0
term_CC_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: cert: CompletenessCertificate
term_QL_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: neg(bnot(x))
term_QL_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: succ(x) in Z/(2ⁿ)Z
term_QL_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n, n ≥ 1
term_QL_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: |D_{2ⁿ}|
term_QL_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 2ⁿ⁺¹ for all n ≥ 1
term_QL_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: n ≥ 1
term_QL_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: P(j) = 2^{-j}
term_QL_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Boltzmann distribution at β* = ln 2, all n ≥ 1
term_QL_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: j ∈ R_n, n ≥ 1
term_QL_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: siteBudget(PrimitiveType, n)
term_QL_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: = n (one site per bit)
term_QL_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: PrimitiveType, n ≥ 1
term_QL_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: resolution(CompleteType, n)
term_QL_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: O(1) for all n ≥ 1
term_QL_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: CompleteType, n ≥ 1
term_QL_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: contentAddress(x, n)
term_QL_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: bijection for all n ≥ 1
term_QL_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n, n ≥ 1
term_QL_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ψ-pipeline(ConstrainedType, n)
term_QL_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: valid ChainComplex for all n ≥ 1
term_QL_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ConstrainedType, n ≥ 1
term_GR_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRank(B_{i+1})
term_GR_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ freeRank(B_i)
term_GR_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: i in Session S
term_GR_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: b.datum resolves under b.constraint
term_GR_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: in O(1) iff Binding b is sound
term_GR_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: b: Binding
term_GR_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∃ i: freeRank(B_i) = 0
term_GR_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Session S converges
term_GR_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Session S
term_GR_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: bindings(C_fresh) ∩ bindings(C_prior)
term_GR_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: = ∅ after SessionBoundary
term_GR_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: C_prior, C_fresh: Context, SessionBoundary event
term_GR_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ContradictionBoundary
term_GR_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: iff ∃ b, b': same address, different datum, same constraint
term_GR_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: b, b': Binding in same Context
term_TS_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: nerve(T, target)
term_TS_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∃ ConstrainedType T over R_n realising target
term_TS_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: target: χ* ≤ n, β₀* = 1, β_k* = 0 for k ≥ 1
term_TS_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: basisSize(T, IT_7d target)
term_TS_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: n
term_TS_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: IT_7d target, n-site types
term_TS_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: χ(N(C + constraint))
term_TS_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≥ χ(N(C))
term_TS_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: C: synthesis candidate constraint set
term_TS_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: steps(TypeSynthesisResolver, target)
term_TS_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ n
term_TS_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: target: realisable n-site type synthesis goal
term_TS_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: SynthesizedType achieves IT_7d
term_TS_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: iff CompletenessResolver certifies CompleteType
term_TS_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T: SynthesizedType
term_TS_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: E[steps, Jacobian-guided synthesis]
term_TS_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: O(n log n) vs O(n²) uninformed
term_TS_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T: n-site type synthesis goal
term_TS_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: β₀(N(C)) for non-empty C
term_TS_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≥ 1
term_TS_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: C: non-empty constraint set
term_WLS_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: WittLift T' is CompleteType
term_WLS_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: iff spectral sequence collapses at E_2
term_WLS_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T: CompleteType at Q_n, T': WittLift to Q_{n+1}
term_WLS_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: non-trivial LiftObstruction location
term_WLS_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: specific site at bit position n+1
term_WLS_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: non-trivial LiftObstruction
term_WLS_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: basisSize(T') for trivial lift
term_WLS_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: basisSize(T) + 1
term_WLS_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T: CompleteType at Q_n with closed constraint set
term_WLS_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: spectral sequence convergence page
term_WLS_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ E_{d+2}
term_WLS_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: depth-d constraint configuration
term_WLS_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: universallyValid identity in R_{n+1}
term_WLS_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: holds with lifted constraint set
term_WLS_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: every op:universallyValid identity, WittLift T'
term_WLS_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ψ-pipeline ChainComplex(T')
term_WLS_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: valid and restricts to ChainComplex(T) on base nerve
term_WLS_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T': any WittLift of a CompleteType T
term_MN_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: HolonomyGroup(T)
term_MN_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ D_{2^n}
term_MN_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T: ConstrainedType over R_n
term_MN_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: HolonomyGroup(T) for additive constraints
term_MN_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: {id} (trivial: T is FlatType)
term_MN_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T: all ResidueConstraint or DepthConstraint
term_MN_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: HolonomyGroup(T) with neg + bnot in closed path
term_MN_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: D_{2^n} (full dihedral holonomy)
term_MN_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T: ConstrainedType with neg-related and bnot-related constraints in closed path
term_MN_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: HolonomyGroup(T) ≠ {id}
term_MN_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ⟹ β₁(N(C(T))) ≥ 1
term_MN_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T: ConstrainedType
term_MN_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: CompleteType (IT_7d) ⟹ β₁ = 0 ⟹ holonomy
term_MN_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: trivial ⟹ FlatType
term_MN_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T: CompleteType
term_MN_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: monodromy(p₁ · p₂)
term_MN_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: monodromy(p₁) · monodromy(p₂) in D_{2^n}
term_MN_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: p₁, p₂: ClosedConstraintPath
term_MN_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: TwistedType T ⟹ H²(N(C(T')); ℤ/2ℤ)
term_MN_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: non-zero class (non-trivial LiftObstruction)
term_MN_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T': any WittLift of TwistedType T
term_PT_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: siteBudget(A × B)
term_PT_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: siteBudget(A) + siteBudget(B)
term_PT_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: A, B: TypeDefinition
term_PT_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: partition(A × B)
term_PT_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: partition(A) ⊗ partition(B)
term_PT_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: A, B: TypeDefinition
term_PT_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: χ(N(C(A × B)))
term_PT_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: χ(N(C(A))) + χ(N(C(B)))
term_PT_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: A, B: TypeDefinition
term_PT_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: S(A × B)
term_PT_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: S(A) + S(B)
term_PT_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: A, B: TypeDefinition
term_ST_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: siteBudget(A + B)
term_ST_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: max(siteBudget(A), siteBudget(B))
term_ST_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: A, B: TypeDefinition
term_ST_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: S(A + B)
term_ST_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ln 2 + max(S(A), S(B))
term_ST_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: A, B: TypeDefinition
term_GS_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: T_ctx(C)
term_GS_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRank(C) × ln 2 / n
term_GS_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: C: Context, n = siteBudget
term_GS_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: σ(C)
term_GS_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: (n − freeRank(C)) / n
term_GS_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: C: Context, n = siteBudget
term_GS_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: σ(B_{i+1})
term_GS_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≥ σ(B_i)
term_GS_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: i in Session S
term_GS_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: σ(C) = 1
term_GS_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRank(C) = 0 ↔ S(C) = 0 ↔ T_ctx(C) = 0
term_GS_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: C: Context
term_GS_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: stepCount(q, C) at freeRank(C) = 0
term_GS_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 0
term_GS_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: q: Query, C: GroundedContext
term_GS_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: effectiveBudget(q, C)
term_GS_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: max(0, siteBudget(q.type) − |pinnedSites(C) ∩ q.siteSet|)
term_GS_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: q: Query, C: Context
term_GS_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Cost_saturation(C)
term_GS_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: n × k_B T × ln 2
term_GS_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: C: GroundedContext, n = siteBudget
term_MS_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: β₀(N(C))
term_MS_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≥ 1
term_MS_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: C: non-empty ConstrainedType
term_MS_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: χ(N(C))
term_MS_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ n
term_MS_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: C: ConstrainedType at quantum level n
term_MS_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: χ(N(C + c))
term_MS_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≥ χ(N(C))
term_MS_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: C: ConstrainedType, c: Constraint
term_MS_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: achievable(χ*, β_k*, n)
term_MS_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: → achievable(χ*, β_k*, n+1)
term_MS_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: (χ*, β_k*) achievable at level n
term_MS_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: verified SynthesisSignature set
term_MS_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: → exact morphospace boundary in the limit
term_MS_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: all quantum levels
term_GD_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: isGeodesic(T)
term_GD_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: AR_1-ordered(T) ∧ DC_10-selected(T)
term_GD_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T: ComputationTrace
term_GD_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ΔS_step(i) on geodesic
term_GD_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ln 2
term_GD_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: step i of GeodesicTrace T
term_GD_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Cost_geodesic(T)
term_GD_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRank_initial × k_B T × ln 2
term_GD_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T: GeodesicTrace
term_GD_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Cost(T) for geodesic T
term_GD_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: = Cost(T') for any geodesic T' on same type
term_GD_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T, T': GeodesicTrace on same ConstrainedType
term_GD_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: isSubgeodesic(T)
term_GD_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∃ i: J_k(step_i) < max_{free} J_k(state_i)
term_GD_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T: ComputationTrace
term_QM_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: S_vonNeumann(ψ)
term_QM_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Cost_Landauer(collapse(ψ))
term_QM_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ψ: SuperposedSiteState
term_QM_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: collapse(ψ)
term_QM_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: apply(ResidueConstraint, collapsed_site)
term_QM_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ψ: SuperposedSiteState
term_QM_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: S_vN(ψ)
term_QM_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∈ [0, ln 2]
term_QM_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ψ: single-site SuperposedSiteState
term_QM_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: collapse(collapse(ψ))
term_QM_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: collapse(ψ)
term_QM_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ψ: SuperposedSiteState
term_QM_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σᵢ |αᵢ|²
term_QM_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 1
term_QM_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: SuperposedSiteState ψ
term_RC_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: normalize(ψ)
term_RC_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ψ / sqrt(Σ |αᵢ|²)
term_RC_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: SuperposedSiteState ψ
term_FPM_8_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: |Irr| + |Red| + |Unit| + |Ext|
term_FPM_8_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 2ⁿ
term_FPM_8_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Partition P over R_n
term_FPM_9_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x ∈ Ext(T)
term_FPM_9_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x ∉ carrier(T)
term_FPM_9_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: TypeDefinition T, Datum x
term_MN_8_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: holonomyClassified(T)
term_MN_8_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: isFlatType(T) xor isTwistedType(T)
term_MN_8_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ConstrainedType T with holonomyGroup
term_QL_8_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: wittLevelPredecessor(nextWittLevel(Q_k))
term_QL_8_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Q_k
term_QL_8_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: WittLevel W_n with nextWittLevel defined
term_D_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: compose(rᵃ sᵖ, rᵇ sᵠ)
term_D_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: r^((a + (-1)ᵖ b) mod 2ⁿ) s^(p xor q)
term_D_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: DihedralElement rᵃ sᵖ, rᵇ sᵠ in D_{2ⁿ}
term_SP_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: resolve_superposition(classical(x))
term_SP_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: resolve_classical(x)
term_SP_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Datum x
term_SP_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: collapse(resolve_superposition(ψ))
term_SP_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: resolve_classical(collapse(ψ))
term_SP_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: SuperposedSiteState ψ
term_SP_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: amplitudeVector(resolve_superposition(ψ))
term_SP_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: normalized
term_SP_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: SuperposedSiteState ψ
term_SP_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: P(collapse to site k)
term_SP_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: |α_k|²
term_SP_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: SuperposedSiteState ψ, site index k
term_PT_2a_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Π(A × B)
term_PT_2a_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: PartitionProduct(Π(A), Π(B))
term_PT_2a_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ProductType A × B
term_PT_2b_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Π(A + B)
term_PT_2b_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: PartitionCoproduct(Π(A), Π(B))
term_PT_2b_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: SumType A + B
term_GD_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: isGeodesic(trace)
term_GD_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: isAR1Ordered(trace) ∧ isDC10Selected(trace)
term_GD_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ComputationTrace trace
term_WT_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: LiftChain(Q_j, Q_k) valid
term_WT_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: every chainStep has trivial or resolved LiftObstruction
term_WT_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: LiftChain from Q_j to Q_k
term_WT_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: obstructionCount(chain)
term_WT_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: <= chainLength(chain)
term_WT_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: LiftChain
term_WT_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: resolvedBasisSize(Q_k)
term_WT_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: basisSize(Q_j) + chainLength + obstructionResolutionCost
term_WT_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: LiftChain with source Q_j, target Q_k
term_WT_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: isFlat(chain)
term_WT_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: obstructionCount = 0 iff HolonomyGroup trivial at every step
term_WT_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: LiftChain
term_WT_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: LiftChainCertificate exists
term_WT_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: CompleteType at Q_k satisfies IT_7d with witness chain
term_WT_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Q_k for arbitrary k
term_WT_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: QT_3 with chainLength=1, cost=0
term_WT_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: reduces to QLS_3
term_WT_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Single-step chains
term_WT_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: flat chain resolvedBasisSize(Q_k)
term_WT_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: basisSize(Q_j) + (k - j)
term_WT_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: LiftChain with isFlat = true
term_CC_PINS_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pinsSites(CarryConstraint(p))
term_CC_PINS_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: {k : p(k)=1} union {first-zero(p)}
term_CC_PINS_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: bit-pattern p in CarryConstraint
term_CC_COST_SITE_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: |pinsSites(CarryConstraint(p))|
term_CC_COST_SITE_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: popcount(p) + 1
term_CC_COST_SITE_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: bit-pattern p in CarryConstraint
term_jsat_RR_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: jointSat(Res(m1,r1), Res(m2,r2))
term_jsat_RR_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: gcd(m1,m2) | (r1 - r2)
term_jsat_RR_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ResidueConstraint pairs over R_n
term_jsat_CR_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: jointSat(Carry(p), Res(m,r))
term_jsat_CR_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pin-site intersection residue-class compatible
term_jsat_CR_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: CarryConstraint, ResidueConstraint pairs
term_jsat_CC_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: jointSat(Carry(p1), Carry(p2))
term_jsat_CC_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: p1 AND p2 conflict-free
term_jsat_CC_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: CarryConstraint pairs over R_n
term_D_8_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: (r^a s^p)^(-1)
term_D_8_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: r^(-(−1)^p a mod 2^n) s^p
term_D_8_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: a in 0..2^n, p in {0,1}
term_D_9_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ord(r^k s^1)
term_D_9_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 2
term_D_9_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: k in Z/(2^n)Z
term_EXP_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: carrier(C) is monotone
term_EXP_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: all residues of C = modulus - 1, no Carry/Depth
term_EXP_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ConstrainedType C over R_n
term_EXP_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: count of monotone ConstrainedTypes at Q_n
term_EXP_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 2^n
term_EXP_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: WittLevel W_n, n >= 1
term_EXP_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: carrier(SumType(A,B))
term_EXP_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: coproduct(carrier(A), carrier(B))
term_EXP_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: SumType A + B
term_ST_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: chi(N(C(A+B)))
term_ST_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: chi(N(C(A))) + chi(N(C(B)))
term_ST_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: disjoint SumType A + B
term_ST_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: beta_k(N(C(A+B)))
term_ST_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: beta_k(N(C(A))) + beta_k(N(C(B)))
term_ST_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: disjoint SumType A + B, k >= 0
term_ST_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: CompleteType(A + B)
term_ST_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: CompleteType(A) and CompleteType(B) and Q(A)=Q(B)
term_ST_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: SumType A + B
term_TS_8_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: min constraints for beta_1 = k
term_TS_8_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 2k + 1
term_TS_8_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: first Betti number k >= 1, n-site type
term_TS_9_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: TypeSynthesisResolver terminates
term_TS_9_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: within 2^n steps
term_TS_9_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: WittLevel W_n, any target signature
term_TS_10_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ForbiddenSignature(sigma)
term_TS_10_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: no ConstrainedType with <= n constraints realises sigma
term_TS_10_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: topological signature sigma at Q_n
term_WT_8_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ObstructionChain length from Q_j to Q_k
term_WT_8_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: <= (k-j) * C(basisSize(Q_j), 3)
term_WT_8_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: LiftChain from Q_j to Q_k
term_WT_9_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: TowerCompletenessResolver terminates
term_WT_9_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: within QT_8 bound
term_WT_9_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: LiftChain of finite length
term_COEFF_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: standard coefficient ring for psi-pipeline
term_COEFF_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Z/2Z
term_COEFF_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: CechNerve N(C) at any quantum level
term_GO_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pinsSites(killing constraint for obstruction c)
term_GO_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: superset of pinsSites(C_i) cap pinsSites(C_j)
term_GO_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: GluingObstruction c, cycle pair (C_i, C_j)
term_GR_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRank(q) after grounding
term_GR_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: sites of q not in BindingAccumulator
term_GR_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: grounded Session, new RelationQuery q
term_GR_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: sigma after re-entry with query q
term_GR_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: min(sigma, 1 - freeRank(q)/n)
term_GR_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: SessionResolver, new query q
term_QM_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: amplitude index set of SuperposedSiteState over T
term_QM_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: monotone pinning trajectories consistent with T
term_QM_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: SuperposedSiteState over ConstrainedType T at Q_n
term_CIC_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: valid(T) ∧ T: Transform
term_CIC_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∃ c: TransformCertificate. certifies(c, T)
term_CIC_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Transform T
term_CIC_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: isometry(T) ∧ metric-preserving(T)
term_CIC_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∃ c: IsometryCertificate. certifies(c, T)
term_CIC_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Isometry T
term_CIC_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: f(f(x)) = x ∀ x ∈ R_n
term_CIC_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∃ c: InvolutionCertificate. certifies(c, f)
term_CIC_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Involution f
term_CIC_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: σ(C) = 1 ∧ freeRank = 0
term_CIC_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∃ c: GroundingCertificate. certifies(c, C)
term_CIC_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: GroundedContext C
term_CIC_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: AR_1-ordered ∧ DC_10-selected trace
term_CIC_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∃ c: GeodesicCertificate. certifies(c, trace)
term_CIC_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: GeodesicTrace
term_CIC_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: S_vN = L_cost at β* = ln 2
term_CIC_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∃ c: MeasurementCertificate. certifies(c, event)
term_CIC_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: MeasurementEvent
term_CIC_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: P(k) = |α_k|² verified
term_CIC_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∃ c: BornRuleVerification. certifies(c, event)
term_CIC_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: MeasurementEvent with amplitude vector
term_GC_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: shared-frame grounding of symbol s
term_GC_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∃ c: GroundingCertificate. certifies(c, map)
term_GC_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: GroundingMap with valid ProjectionMap
term_GR_8_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: compose(S_A, S_B) valid at Q_k
term_GR_8_rhshttps://uor.foundation/schema/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_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: S_A, S_B: Session at quantum level Q_k (k ≥ 0)
term_GR_9_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: leasedSites(L_A) ∩ leasedSites(L_B)
term_GR_9_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: = ∅
term_GR_9_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: L_A, L_B: ContextLease on SharedContext C, L_A ≠ L_B
term_GR_10_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: finalState(R, P_1, Q)
term_GR_10_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: = finalState(R, P_2, Q) for any P_1, P_2: ExecutionPolicy
term_GR_10_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: SessionResolver R with ExecutionPolicy P, pending query set Q
term_MC_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σᵢ freeRank(leasedSites(L_i))
term_MC_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: = freeRank(C)
term_MC_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: SharedContext C; leaseSet {L_1, …, L_k} covering all sites of C
term_MC_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRank(B_{i+1} |_L)
term_MC_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ freeRank(B_i |_L)
term_MC_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ContextLease L held by Session S; binding step i within S restricted to leasedSites(L)
term_MC_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRank(compose(S_A, S_B))
term_MC_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRank(S_A) + freeRank(S_B) − |pinnedSites(S_A) ∩ pinnedSites(S_B)|
term_MC_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: S_A, S_B: Session; compose(S_A, S_B) valid (SR_8 satisfied)
term_MC_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRank(compose(S_A, S_B))
term_MC_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: = freeRank(S_A) + freeRank(S_B)
term_MC_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: S_A, S_B on ContextLeases L_A, L_B within SharedContext C; SR_9 holds
term_MC_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: finalBindings(R, P_1, Q)
term_MC_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: = finalBindings(R, P_2, Q)
term_MC_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: SessionResolver R; pending query set Q; ExecutionPolicy P_1, P_2
term_MC_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: σ(compose(S_1, …, S_k))
term_MC_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: = 1 (FullGrounding)
term_MC_6_forAllhttps://uor.foundation/schema/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_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: stepCount(q, C*)
term_MC_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: = 0
term_MC_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: q: RelationQuery; C* = compose(S_1, …, S_k) with σ(C*) = 1 by MC_6
term_MC_8_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: max_i stepCount(S_i to convergence within L_i)
term_MC_8_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ ⌈n/k⌉
term_MC_8_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: SharedContext C with totalSites = n; uniform partition into k leases
term_WC_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: a_k(x)
term_WC_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x_k (k-th bit of x)
term_WC_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n, 0 ≤ k < n
term_WC_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: S_k − x_k − y_k (mod 2)
term_WC_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: c_k(x,y)
term_WC_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n, 0 ≤ k < n
term_WC_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: CA_2 recurrence
term_WC_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: S_{k+1} ghost equation at p=2
term_WC_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_WC_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: δ_k(x+y) correction
term_WC_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: c_{k+1}(x,y)
term_WC_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_WC_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: obstruction_trivial = false
term_WC_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: δ_k ≠ 0 for some pair
term_WC_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Q_k, k ≥ 1
term_WC_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_Δ(x,y) > 0
term_WC_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ghost defect nonzero
term_WC_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_WC_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: succ^{2ⁿ}(x) = x
term_WC_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: r^{2ⁿ} = 1 in Witt-Burnside ring
term_WC_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n, n ≥ 1
term_WC_8_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: neg(succ(neg(x)))
term_WC_8_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: srs = r⁻¹ relation
term_WC_8_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n, n ≥ 1
term_WC_9_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: bnot(neg(x)) = pred(x)
term_WC_9_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Product of Witt-Burnside reflections
term_WC_9_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n, n ≥ 1
term_WC_10_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: φ(x) on W_n(F_2)
term_WC_10_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: x (identity, F_2 perfect)
term_WC_10_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n, n ≥ 1
term_WC_11_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: V(x) on W_n(F_2)
term_WC_11_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: add(x, x) in Z/(2ⁿ)Z
term_WC_11_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n, n ≥ 1
term_WC_12_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: δ(x) on W_n(F_2)
term_WC_12_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: (x − mul(x,x)) / 2
term_WC_12_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x ∈ R_n, n ≥ 2
term_OA_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: |2|_2 · |2|_∞
term_OA_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 1 in Q×
term_OA_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: p = 2
term_OA_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: CrossingCost(p=2)
term_OA_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ln 2 = −ln|2|_2
term_OA_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: p = 2
term_OA_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: β* in Cost_Landauer
term_OA_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: CrossingCost(p=2)
term_OA_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: p = 2
term_OA_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: P(outcome k) = |α_k|_∞²
term_OA_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Archimedean image of 2-adic amplitude
term_OA_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: rational amplitudes
term_OA_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Information cost of δ (division by 2)
term_OA_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ln 2 nats
term_OA_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: p = 2
term_HT_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: N(C)
term_HT_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: KanComplex
term_HT_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint configuration C
term_HT_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: π₀(N(C))
term_HT_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Z^{β₀}
term_HT_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint configuration C
term_HT_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: π₁(N(C)) → D_{2^n}
term_HT_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: HolonomyGroup factorization
term_HT_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint configuration C
term_HT_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: π_k(N(C)) for k > dim(N(C))
term_HT_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 0
term_HT_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint configuration C, k > dim(N(C))
term_HT_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: τ_{≤1}(N(C))
term_HT_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: FlatType/TwistedType classification
term_HT_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint configuration C
term_HT_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: κ_k trivial for all k > d
term_HT_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: spectral sequence collapses at E_{d+2}
term_HT_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint configuration C, d = max simplex dim
term_HT_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: [α, β] ≠ 0 in π_{p+q−1}
term_HT_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: LiftObstruction non-trivial
term_HT_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: α ∈ π_p, β ∈ π_q
term_HT_8_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: π_k(N(C)) ⊗ Z
term_HT_8_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: H_k(N(C); Z) for smallest k with π_k ≠ 0
term_HT_8_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint configuration C
term_psi_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: KanComplex(N(C))
term_psi_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: PostnikovTower
term_psi_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint configuration C
term_psi_8_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: PostnikovTower(τ≤k)
term_psi_8_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: HomotopyGroups(π_k)
term_psi_8_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint configuration C
term_psi_9_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: HomotopyGroups(π_k)
term_psi_9_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: KInvariants(κ_k)
term_psi_9_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint configuration C
term_HP_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ψ_7 ∘ ψ_1
term_HP_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Kan promotion of nerve
term_HP_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint configuration C
term_HP_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ψ_8(τ≤k) restricted
term_HP_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ψ_3(C≤k)
term_HP_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint configuration C, truncation level k
term_HP_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ψ_9 detects convergence
term_HP_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: spectral sequence converges at E_{d+2}
term_HP_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint configuration C
term_HP_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: HomotopyResolver time
term_HP_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: O(n^{d+1})
term_HP_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: d = max simplex dimension
term_MD_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: dim(M_n)
term_MD_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: basisSize(T)
term_MD_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: T in M_n
term_MD_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: H^0(Def(T))
term_MD_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Aut(T) ∩ D_{2^n}
term_MD_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: CompleteType T
term_MD_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: H^1(Def(T))
term_MD_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: T_T(M_n)
term_MD_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: CompleteType T
term_MD_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: H^2(Def(T))
term_MD_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: LiftObstruction space
term_MD_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: CompleteType T
term_MD_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: FlatType stratum codimension
term_MD_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 0
term_MD_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: M_n at any quantum level
term_MD_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: TwistedType stratum codimension
term_MD_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≥ 1
term_MD_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: M_n at any quantum level
term_MD_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: VersalDeformation existence
term_MD_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: guaranteed when H^2 = 0
term_MD_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: CompleteType T
term_MD_8_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: familyPreservesCompleteness
term_MD_8_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: H^2(Def(T_t)) = 0 along path
term_MD_8_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: DeformationFamily {C_t}
term_MD_9_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: site(ModuliTowerMap, T) dimension
term_MD_9_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 1 when obstructionTrivial
term_MD_9_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: CompleteType T, obstruction = 0
term_MD_10_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: site(ModuliTowerMap, T)
term_MD_10_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: empty iff TwistedType at every level
term_MD_10_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: CompleteType T
term_MR_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ModuliResolver boundary
term_MR_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: MorphospaceBoundary
term_MR_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: M_n
term_MR_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: StratificationRecord coverage
term_MR_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: every CompleteType in exactly one stratum
term_MR_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: M_n
term_MR_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ModuliResolver complexity
term_MR_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: O(n × basisSize²)
term_MR_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: CompleteType T
term_MR_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: achievabilityStatus = Achievable
term_MR_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: signature in some HolonomyStratum
term_MR_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: MorphospaceRecord
term_CY_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: generate(k)
term_CY_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: and(x_k, y_k) = 1
term_CY_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n, 0 ≤ k < n
term_CY_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: propagate(k)
term_CY_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: xor(x_k, y_k) = 1 ∧ c_k = 1
term_CY_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n, 0 ≤ k < n
term_CY_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: kill(k)
term_CY_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: and(x_k, y_k) = 0 ∧ xor(x_k, y_k) = 0
term_CY_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n, 0 ≤ k < n
term_CY_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_Δ(x, y)
term_CY_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: |carryCount(x+y) − hammingDistance(x, y)|
term_CY_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_CY_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: argmin_enc Σ d_Δ(enc(s_i), enc(s_j))
term_CY_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: enc where carry significance ≅ domain dependency
term_CY_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: finite symbol set S, observed pairs (s_i, s_j)
term_CY_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: min d_Δ site ordering
term_CY_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: high-significance sites → most informative observables
term_CY_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: EncodingConfiguration over ordered domain
term_CY_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: T(carry_chain(n))
term_CY_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: O(log n) via prefix computation on (g_k, p_k) pairs
term_CY_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: CarryChain of length n
term_BM_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: σ(C)
term_BM_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: (n − freeRank(C)) / n
term_BM_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Context C with n sites
term_BM_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: χ(nerve(C))
term_BM_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σ(−1)^k β_k(nerve(C))
term_BM_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint set C
term_BM_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σκ_k − χ
term_BM_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: S_residual / ln 2
term_BM_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: computation state
term_BM_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: J_k (pinned site k)
term_BM_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 0
term_BM_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: pinned site k
term_BM_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_Δ(x, y) > 0
term_BM_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: carry(x + y) ≠ 0
term_BM_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: x, y ∈ R_n
term_BM_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: metric tower
term_BM_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_Δ → {σ, J_k} → β_k → χ → r
term_BM_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: computation state
term_GL_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: σ(T)
term_GL_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: lower_adjoint(T)
term_GL_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: type T in type lattice
term_GL_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: r(T)
term_GL_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 1 − upper_adjoint(T)
term_GL_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: type T in type lattice
term_GL_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: upper(lower(T))
term_GL_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: T (fixpoint: σ=1, r=0)
term_GL_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: CompleteType T
term_GL_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: T₁ ≤ T₂ in type lattice
term_GL_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: site(T₂) ⊆ site(T₁)
term_GL_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: types T₁, T₂
term_NV_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: nerve(C₁ ∪ C₂)
term_NV_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: nerve(C₁) ∪ nerve(C₂)
term_NV_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: disjoint constraint domains C₁, C₂
term_NV_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: β_k(C₁ ∪ C₂)
term_NV_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: β_k(C₁) + β_k(C₂) − β_k(C₁ ∩ C₂)
term_NV_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint sets C₁, C₂
term_NV_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Δβ_k
term_NV_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∈ {−1, 0, +1}
term_NV_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: single constraint addition, dimension k
term_NV_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: β_k(C ∪ {c})
term_NV_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ β_k(C)
term_NV_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint set C, new constraint c
term_SD_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: quantize(value, range, bits)
term_SD_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ring element with d_R ∝ |v₁ − v₂|
term_SD_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: values v in ordered domain
term_SD_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: encoding(alphabet)
term_SD_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: argmin_{e} Σ d_Δ(e(a), e(b))
term_SD_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: symbol pairs (a,b) in alphabet
term_SD_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Seq(T)
term_SD_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Free(T) with backbone ordering
term_SD_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: element type T
term_SD_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: sites(Tuple(f₁,...,fₖ))
term_SD_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σᵢ sites(fᵢ)
term_SD_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: fields f_1,...,f_k of tuple type
term_SD_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: nerve(Graph(V,E))
term_SD_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: constraint_nerve(Graph(V,E))
term_SD_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: graph (V,E) with typed nodes
term_SD_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_Δ(Set(a,b,c))
term_SD_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_Δ(Set(σ(a,b,c)))
term_SD_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: permutation σ of set elements
term_SD_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: β_1(Tree(V,E))
term_SD_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 0
term_SD_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: tree (V,E) with beta_0=1
term_SD_8_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Table(S)
term_SD_8_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Seq(Tuple(S))
term_SD_8_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: schema S defining tuple fields
term_DD_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: δ(q, R)
term_DD_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: δ(q, R)
term_DD_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: query q, registry R
term_DD_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: dom(R)
term_DD_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: {q | ∃r. δ(q,R)=r}
term_DD_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: registry R
term_PI_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ι(ι(s,C),C)
term_PI_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ι(s,C)
term_PI_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: symbol s, GroundedContext C
term_PI_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: type(ι(s,C))
term_PI_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: consistent(C)
term_PI_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: symbol s, context C
term_PI_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ι(s,C)
term_PI_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: P(Π(G(s,C)))
term_PI_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: symbol s, context C
term_PI_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: complexity(ι(s,C))
term_PI_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: O(|C|)
term_PI_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: symbol s, context C
term_PI_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: roundTrip(P(Π(G(s))))
term_PI_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: s
term_PI_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: symbol s
term_PA_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: α(b₁,α(b₂,C))
term_PA_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: α(b₂,α(b₁,C))
term_PA_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: bindings b₁,b₂, context C at saturation
term_PA_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: sites(α(b,C))
term_PA_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: sites(C) ∪ {b.site}
term_PA_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: binding b, context C
term_PA_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: constraints(α(b,C))
term_PA_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: constraints(C) ∪ constraints(b)
term_PA_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: binding b, context C
term_PA_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: α(b,C)|_{pinned(C)}
term_PA_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: C|_{pinned(C)}
term_PA_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: binding b, context C
term_PA_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: α(∅, C)
term_PA_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: C
term_PA_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: context C
term_PL_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Lᵢ ∩ Lⱼ
term_PL_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∅
term_PL_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: leases Lᵢ, Lⱼ with i ≠ j
term_PL_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ⋃ᵢ Lᵢ
term_PL_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: S
term_PL_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: shared context S, leases Lᵢ
term_PL_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: |{i | f ∈ Lᵢ}|
term_PL_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 1
term_PL_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: site f in shared context S
term_PK_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: valid(κ(S₁,S₂))
term_PK_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: disjoint(S₁,S₂)
term_PK_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: sessions S₁,S₂
term_PK_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: resolve(s, κ(S₁,S₂))
term_PK_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: resolve(s, S₁) ∨ resolve(s, S₂)
term_PK_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: symbol s, sessions S₁,S₂
term_PP_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: κ(λₖ(α*(ι(s,·))), C)
term_PP_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: resolve(s, C)
term_PP_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: symbol s, context C
term_PE_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: state(ψ, 0)
term_PE_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 1
term_PE_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: reduction ψ
term_PE_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ψ_1(q)
term_PE_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: δ(q, R)
term_PE_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: query q, registry R
term_PE_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ψ_2(r)
term_PE_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: G(r)
term_PE_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: resolver r
term_PE_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ψ_3(a)
term_PE_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Π(a)
term_PE_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: address a
term_PE_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ψ_4(c)
term_PE_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: α*(c)
term_PE_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constraint set c
term_PE_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ψ_5(b)
term_PE_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: P(b)
term_PE_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: binding b
term_PE_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ψ_5 ∘ ψ_4 ∘ ψ_3 ∘ ψ_2 ∘ ψ_1 ∘ ψ_0
term_PE_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ψ
term_PE_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: reduction ψ
term_PM_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: phase(stage_k)
term_PM_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Ω^k
term_PM_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: stage index k in 0..5
term_PM_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: gate(k)
term_PM_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: phase(k) == Ω^k
term_PM_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: stage boundary k
term_PM_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: fail(gate(k))
term_PM_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: rollback(z → z̄)
term_PM_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: stage k with gate failure
term_PM_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: conj(conj(z))
term_PM_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: z
term_PM_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: complex value z
term_PM_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: sat(epoch_n)
term_PM_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: sat(epoch_{n+1})
term_PM_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: consecutive epochs n, n+1
term_PM_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: context(window)
term_PM_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: base_context
term_PM_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: service window
term_PM_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ψ(s₀)
term_PM_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ψ(s₀)
term_PM_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: initial state s₀
term_ER_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: advance(k, k+1)
term_ER_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: guard(k) = true
term_ER_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: stage transition k to k+1
term_ER_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: apply(effect(k))
term_ER_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: atomic(effect(k))
term_ER_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: transition effect at stage k
term_ER_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: eval(guard(k), s)
term_ER_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: s (state unchanged)
term_ER_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: guard evaluation at stage k with state s
term_ER_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: apply(e1; e2)
term_ER_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: apply(e2; e1)
term_ER_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: effects e1, e2 within same stage
term_EA_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: free(epoch(n+1))
term_EA_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: free(epoch(0))
term_EA_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: epoch boundary n to n+1
term_EA_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: grounded(epoch(n))
term_EA_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: grounded(epoch(n+1))
term_EA_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: grounded sites across epoch boundary
term_EA_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: |context(w)|
term_EA_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: windowSize(w)
term_EA_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: service window w
term_EA_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: admit(epoch(n))
term_EA_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: datum | refinement
term_EA_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: epoch admission at epoch n
term_OE_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: stage(k); stage(k+1)
term_OE_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: fused(k, k+1)
term_OE_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: adjacent stages k, k+1 with compatible guards
term_OE_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: effect(a); effect(b)
term_OE_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: effect(b); effect(a)
term_OE_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: independent effects a, b
term_OE_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: lease(A); lease(B)
term_OE_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: lease(A) || lease(B)
term_OE_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: disjoint lease sets A, B
term_OE_4a_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: sem(fused(k, k+1))
term_OE_4a_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: sem(stage(k)); sem(stage(k+1))
term_OE_4a_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: fused stages k, k+1
term_OE_4b_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: outcome(a; b)
term_OE_4b_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: outcome(b; a)
term_OE_4b_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: commuting effects a, b
term_OE_4c_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: coverage(A || B)
term_OE_4c_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: coverage(A) + coverage(B)
term_OE_4c_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: parallel leases A, B
term_CS_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cost(stage(k))
term_CS_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: O(1)
term_CS_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: reduction step k
term_CS_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cost(pipeline)
term_CS_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: sum(cost(stage(k)))
term_CS_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: reduction pipeline
term_CS_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cost(rollback)
term_CS_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cost(forward)
term_CS_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: reduction rollback operation
term_CS_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cost(preflight)
term_CS_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: O(1)
term_CS_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: preflight check
term_CS_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cost(reduction)
term_CS_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: n * max(cost(stage(k)))
term_CS_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: reduction with n stages
term_CS_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: thermodynamicBudget(U) < bitsWidth(unitWittLevel(U)) × ln 2
term_CS_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: reject(U) at BudgetSolvencyCheck
term_CS_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: CompileUnit U
term_CS_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: unitAddress(U)
term_CS_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: address(canonicalBytes(transitiveClosure(rootTerm(U))))
term_CS_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: CompileUnit U
term_FA_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pending(q)
term_FA_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: reaches_gate(q)
term_FA_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: query q in reduction
term_FA_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: admitted(q, epoch)
term_FA_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: served(q, epoch + k)
term_FA_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: query q, bounded k
term_FA_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: lease_alloc(p1 + p2)
term_FA_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: lease_alloc(p1) + lease_alloc(p2)
term_FA_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: disjoint partitions p1, p2
term_SW_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: memory(window(w))
term_SW_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: O(w)
term_SW_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: service window of size w
term_SW_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: saturated(slide(w))
term_SW_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: saturated(w)
term_SW_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: window slide operation
term_SW_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: resources(evict(e))
term_SW_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 0
term_SW_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: evicted epoch e
term_SW_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: size(window)
term_SW_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: >= 1
term_SW_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: service window
term_LS_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pinned(suspend(lease))
term_LS_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pinned(lease)
term_LS_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: lease suspension
term_LS_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: resources(expire(lease))
term_LS_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 0
term_LS_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: expired lease
term_LS_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: restore(restore(checkpoint))
term_LS_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: restore(checkpoint)
term_LS_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: checkpoint restore
term_LS_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: resume(suspend(lease))
term_LS_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: lease
term_LS_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: active lease
term_TJ_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: all_or_nothing(fail)
term_TJ_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: rollback
term_TJ_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: AllOrNothing transaction with failure
term_TJ_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: best_effort(partial_fail)
term_TJ_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: commit(succeeded)
term_TJ_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: BestEffort transaction
term_TJ_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: scope(transaction)
term_TJ_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: single_epoch
term_TJ_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: reduction transaction
term_AP_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: sat(stage(k+1))
term_AP_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: >= sat(stage(k))
term_AP_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: consecutive stages k, k+1
term_AP_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: quality(epoch(n+1))
term_AP_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: >= quality(epoch(n))
term_AP_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: consecutive epochs n, n+1
term_AP_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: deferred(q)
term_AP_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: processed(q) | dropped(q)
term_AP_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: deferred query q
term_EC_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Ω⁶
term_EC_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: −1
term_EC_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: reduction phase angle Ω = e^{iπ/6}
term_EC_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: conj(conj(z))
term_EC_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: z
term_EC_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: complex z in reduction
term_EC_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: [q_A, q_B]^inf
term_EC_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 1
term_EC_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: quaternion pair q_A, q_B
term_EC_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: [q_A, q_B, q_C]^inf
term_EC_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 0
term_EC_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: octonion triple q_A, q_B, q_C
term_EC_4a_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ||[a,b,c]_{n+1}||
term_EC_4a_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: <= ||[a,b,c]_n||
term_EC_4a_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: successive associator iterates
term_EC_4b_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: steps_to_zero([a,b,c])
term_EC_4b_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: <= |three_way_sites|
term_EC_4b_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: octonion triple a, b, c
term_EC_4c_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: [a,b,c] = 0
term_EC_4c_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: associative(resolved_site_space)
term_EC_4c_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: resolved site space
term_EC_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: max_level(convergence_tower)
term_EC_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: L3_Self
term_EC_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: convergence tower
term_DA_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: CD(R, i)
term_DA_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: C
term_DA_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Cayley-Dickson doubling
term_DA_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: CD(C, j)
term_DA_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: H
term_DA_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Cayley-Dickson doubling
term_DA_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: CD(H, l)
term_DA_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: O
term_DA_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Cayley-Dickson doubling
term_DA_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: dim(normed_div_alg)
term_DA_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∈ {1, 2, 4, 8}
term_DA_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: normed division algebras over R
term_DA_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: algebra(L_k)
term_DA_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: division_algebra[k]
term_DA_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: convergence level L_k
term_DA_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: [a,b] = 0
term_DA_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: isCommutative(algebra(L_k))
term_DA_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: elements a, b in division algebra at level k
term_DA_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: [a,b,c] = 0
term_DA_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: isAssociative(algebra(L_k))
term_DA_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: elements a, b, c in division algebra at level k
term_IN_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_Δ(A,B)
term_IN_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: interaction_cost(A,B)
term_IN_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: entity pairs A, B
term_IN_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: disjoint_leases(A,B)
term_IN_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: commutator(A,B) = 0
term_IN_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: entity pairs with disjoint leases
term_IN_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: shared_sites(A,B) ≠ ∅
term_IN_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: commutator(A,B) > 0
term_IN_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: entity pairs with shared sites
term_IN_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: SR_8_session(A,B)
term_IN_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: commutator(A,B,t+1) ≤ commutator(A,B,t)
term_IN_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: entity pairs in session
term_IN_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: converged_negotiation(A,B)
term_IN_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: U(1) ⊂ SU(2)
term_IN_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: converged pairwise interactions
term_IN_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: outcome_space(pairwise_negotiation)
term_IN_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: S²
term_IN_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: pairwise negotiations
term_IN_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: converged_mutual_model(A,B,C)
term_IN_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: H ⊂ O
term_IN_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: converged triple interactions
term_IN_8_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: β_k(interaction_nerve)
term_IN_8_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: coupling_complexity(k)
term_IN_8_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: interaction nerve at dimension k
term_IN_9_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: β_2(nerve) × max_disagreement
term_IN_9_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: upper_bound(associator_norm)
term_IN_9_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: interaction nerves with β_2 > 0
term_AS_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: (δ ∘ ι) ∘ κ
term_AS_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: δ ∘ (ι ∘ κ)
term_AS_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: triple δ, ι, κ with shared registry
term_AS_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: (ι ∘ α) ∘ λ
term_AS_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ι ∘ (α ∘ λ)
term_AS_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: triple ι, α, λ with shared lease
term_AS_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: (λ ∘ κ) ∘ δ
term_AS_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: λ ∘ (κ ∘ δ)
term_AS_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: triple λ, κ, δ with shared state
term_AS_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: associator(A,B,C) ≠ 0
term_AS_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∃ mediating read-write interleaving
term_AS_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: triples with non-zero associator
term_MO_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: I ⊗ A
term_MO_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: A
term_MO_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: computations A
term_MO_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: (A⊗B)⊗C
term_MO_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: A⊗(B⊗C)
term_MO_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: computations A, B, C
term_MO_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cert(A⊗B)
term_MO_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cert(A) ∧ cert(B)
term_MO_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: certified computations A, B
term_MO_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: σ(A⊗B)
term_MO_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: max(σ(A), σ(B))
term_MO_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: computations A, B
term_MO_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: r(A⊗B)
term_MO_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: min(r(A), r(B))
term_MO_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: computations A, B
term_OP_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: siteCount(F(G))
term_OP_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: F.sites + Σ_i G_i.sites
term_OP_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: structural types F, G
term_OP_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: grounding(F(G(x)))
term_OP_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: F.ground(G.ground(x))
term_OP_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: structural types F, G, element x
term_OP_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_Δ(F(G))
term_OP_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: d_Δ(F) ∘ G + F ∘ d_Δ(G)
term_OP_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: structural types F, G
term_OP_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Table(Tuple(fields))
term_OP_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Sequence(Tuple(fields))
term_OP_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: tabular data
term_OP_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Tree(Symbol(leaves))
term_OP_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Graph(Symbol(leaves), acyclic)
term_OP_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: hierarchical data
term_FX_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRank(postContext(e))
term_FX_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRank(preContext(e)) − 1
term_FX_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: PinningEffect e
term_FX_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRank(postContext(e))
term_FX_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRank(preContext(e)) + 1
term_FX_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: UnbindingEffect e
term_FX_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRank(postContext(e))
term_FX_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRank(preContext(e))
term_FX_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: PhaseEffect e
term_FX_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: apply(A ; B, ctx)
term_FX_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: apply(B ; A, ctx)
term_FX_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Effects A, B with DisjointnessWitness(target(A), target(B))
term_FX_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRankDelta(E₁ ; E₂)
term_FX_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRankDelta(E₁) + freeRankDelta(E₂)
term_FX_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: CompositeEffect (E₁ ; E₂)
term_FX_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: apply(e, apply(e⁻¹, ctx))
term_FX_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ctx
term_FX_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ReversibleEffect e
term_FX_7_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRankDelta(e)
term_FX_7_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: declared freeRankDelta in EffectShape
term_FX_7_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ExternalEffect e satisfying conformance:EffectShape
term_PR_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: eval(p, x)
term_PR_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∈ {true, false}
term_PR_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Predicate p, input x
term_PR_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: state(eval(p, x, s))
term_PR_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: s
term_PR_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Predicate p, input x, state s
term_PR_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: dispatch(D, x)
term_PR_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: exactly one DispatchRule
term_PR_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: DispatchTable D with isExhaustive=true, isMutuallyExclusive=true
term_PR_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: eval(M)
term_PR_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: armResult(first matching arm)
term_PR_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: MatchExpression M with exhaustive arms
term_PR_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: advance(k, guardTarget(g))
term_PR_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: requires guardPredicate(g) = true
term_PR_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: GuardedTransition g at reduction step k
term_CG_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: advance_to(s)
term_CG_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: requires eval(g, currentState) = true
term_CG_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ReductionStep s with entryGuard g
term_CG_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: advance_from(s)
term_CG_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: requires eval(g, currentState) = true, then apply(e)
term_CG_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ReductionStep s with exitGuard g and stageEffect e
term_DIS_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: isExhaustive(D) ∧ isMutuallyExclusive(D)
term_DIS_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: true
term_DIS_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Root DispatchTable D
term_DIS_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: dispatch(D, T)
term_DIS_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: exactly one Resolver
term_DIS_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: TypeDefinition T, DispatchTable D
term_PAR_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: apply(A ⊗ B, ctx)
term_PAR_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: apply(B ⊗ A, ctx)
term_PAR_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ParallelProduct A ∥ B with DisjointnessCertificate
term_PAR_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRankDelta(A ∥ B)
term_PAR_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: freeRankDelta(A) + freeRankDelta(B)
term_PAR_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ParallelProduct A ∥ B
term_PAR_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σ |component_i|
term_PAR_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: n
term_PAR_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: SitePartitioning P over n sites
term_PAR_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: finalContext(σ(A, B))
term_PAR_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: finalContext(A ⊗ B)
term_PAR_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ParallelProduct A ∥ B, any interleaving σ
term_PAR_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cert(A ∥ B)
term_PAR_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cert(A) ∧ cert(B) ∧ DisjointnessCertificate(A, B)
term_PAR_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: cert(A ∥ B)
term_HO_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: value(c)
term_HO_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: contentHash(referencedCertificate(c))
term_HO_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ComputationDatum c
term_HO_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cert(output(app))
term_HO_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cert(applicationTarget(app))
term_HO_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ApplicationMorphism app
term_HO_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cert(f ∘ g)
term_HO_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: cert(f) ∧ cert(g) ∧ range(g) = domain(f)
term_HO_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: TransformComposition f ∘ g
term_HO_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: p
term_HO_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ApplicationMorphism(partialBase(p), boundArguments(p))
term_HO_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: PartialApplication p with remainingArity = 0
term_STR_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: reduction(e_k) converges to π
term_STR_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: true
term_STR_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Epoch e_k in ProductiveStream
term_STR_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: saturation(continuationContext(b))
term_STR_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: saturation(postContext(e_k))
term_STR_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: EpochBoundary b between e_k and e_{k+1}
term_STR_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: computationTime(P)
term_STR_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σ_{i=0}^{k−1} computationTime(epoch_i)
term_STR_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: StreamPrefix P of length k
term_STR_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: epoch_0.context
term_STR_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: seed
term_STR_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Unfold(seed, step)
term_STR_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: epoch_{k+1}.context
term_STR_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: continuationContext(boundary(e_k))
term_STR_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Unfold(seed, step), epoch e_k
term_STR_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: linearBudget(epoch_{k+1})
term_STR_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: linearBudget(epoch_k) + leaseCardinality(L)
term_STR_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: EpochBoundary b with LeaseAllocation L expiring at b
term_FLR_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: result(P)
term_FLR_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∈ {Success, Failure}
term_FLR_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: PartialComputation P
term_FLR_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: result(T)
term_FLR_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Success
term_FLR_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: TotalComputation T
term_FLR_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: result(A ⊗ B)
term_FLR_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Failure(A)
term_FLR_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: A ⊗ B where result(A) = Failure
term_FLR_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: result(A ∥ B)
term_FLR_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Failure(A) (left component)
term_FLR_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: A ∥ B where result(A) = Failure, result(B) = Success
term_FLR_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: result(apply(recoveryEffect(r), failureState(f)))
term_FLR_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ComputationResult
term_FLR_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Recovery r on Failure f
term_FLR_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: recoveryEffect(rollback(f))
term_FLR_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: PhaseEffect(conjugate)
term_FLR_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: ComplexConjugateRollback on Failure f
term_LN_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σ targetCount(site_i)
term_LN_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: n
term_LN_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: LinearTrace T over n-bit type
term_LN_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: status(f, postContext(e))
term_LN_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: pinned
term_LN_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: LinearEffect e on site f
term_LN_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: target(e′) = f
term_LN_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: forbidden
term_LN_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: LinearEffect e on site f, any subsequent effect e′
term_LN_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: remainingCount(budget after L)
term_LN_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: remainingCount(budget before L) − k
term_LN_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: LeaseAllocation L with leaseCardinality k
term_LN_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: remainingCount(budget after expiry)
term_LN_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: remainingCount(budget before expiry) + leaseCardinality(L)
term_LN_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Lease expiry on LeaseAllocation L
term_LN_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: G
term_LN_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: LinearTrace
term_LN_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: GeodesicTrace G
term_SB_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: constraints(T₁)
term_SB_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ⊇ constraints(T₂)
term_SB_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: TypeInclusion T₁ ≤ T₂
term_SB_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: resolutions(T₁)
term_SB_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ⊆ resolutions(T₂)
term_SB_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: TypeInclusion T₁ ≤ T₂, resolution R
term_SB_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: N(C(T₂))
term_SB_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: sub-complex of N(C(T₁))
term_SB_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: TypeInclusion T₁ ≤ T₂
term_SB_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: F(T₁)
term_SB_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ F(T₂)
term_SB_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Covariant position F(_), T₁ ≤ T₂
term_SB_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: F(T₂)
term_SB_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ F(T₁)
term_SB_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Contravariant position F(_), T₁ ≤ T₂
term_SB_6_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: latticeDepth
term_SB_6_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: n
term_SB_6_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: SubtypingLattice at quantum level n
term_BR_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: measureValue(stepMeasurePost(s))
term_BR_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: < measureValue(stepMeasurePre(s))
term_BR_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: RecursiveStep s
term_BR_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: depth(RecursionTrace(R))
term_BR_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ m
term_BR_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: BoundedRecursion R with initialMeasure m
term_BR_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: terminates(R)
term_BR_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: true
term_BR_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: BoundedRecursion R
term_BR_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: initialMeasure(R)
term_BR_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: structuralSize(T)
term_BR_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: StructuralRecursion R on type T
term_BR_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: eval(p, state) = true
term_BR_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: measureValue = 0
term_BR_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: BoundedRecursion R with basePredicate p
term_RG_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: workingSetRegions(W)
term_RG_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: computable from N(C(T)) and stage k site targets
term_RG_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: WorkingSet W for type T at stage k
term_RG_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∀ a, b ∈ R: d_R(a, b)
term_RG_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ diameter(R)
term_RG_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: AddressRegion R with LocalityMetric d_R
term_RG_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σ workingSetSize(stage_k)
term_RG_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ≤ totalAddressableSpace(quantumLevel)
term_RG_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: RegionAllocation A for computation C
term_RG_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: addresses accessed by resolver at stage k
term_RG_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ⊆ addresses(W_k)
term_RG_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Reduction step k with WorkingSet W_k
term_IO_1_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: type(resultDatum(e))
term_IO_1_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: conformsTo(sourceType(s))
term_IO_1_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: IngestEffect e from Source s
term_IO_2_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: type(emittedDatum(e))
term_IO_2_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: conformsTo(sinkType(s))
term_IO_2_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: EmitEffect e to Sink s
term_IO_3_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: apply(g, ingest(s))
term_IO_3_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Datum in R_n
term_IO_3_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Source s with GroundingMap g
term_IO_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: apply(p, d)
term_IO_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: surface symbol conforming to sinkType(s)
term_IO_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: Sink s with ProjectionMap p, Datum d
term_IO_5_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: effect:effectTarget(e)
term_IO_5_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: non-empty EffectTarget
term_IO_5_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: BoundaryEffect e
term_boundarySquaredZero_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: ∂_k(∂_{k+1}(c))
term_boundarySquaredZero_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 0
term_boundarySquaredZero_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: c ∈ C_{k+1}
term_psi_4_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: β_k(K)
term_psi_4_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: rank(H_k(K))
term_psi_4_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: simplicial complex K
term_indexBridge_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: χ(K)
term_indexBridge_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Σ_k (-1)^k β_k
term_indexBridge_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: finite simplicial complex K
term_coboundarySquaredZero_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: δ^{k+1}(δ^k(f))
term_coboundarySquaredZero_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: 0
term_coboundarySquaredZero_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: f ∈ C^k
term_deRhamDuality_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: H^k(K; R)
term_deRhamDuality_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: Hom(H_k(K), R)
term_deRhamDuality_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: simplicial complex K, ring R
term_sheafCohomologyBridge_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: H^k(K; F_R)
term_sheafCohomologyBridge_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: H^k(K; R)
term_sheafCohomologyBridge_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: constant sheaf F_R over K
term_localGlobalPrinciple_lhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: H^1(K; F) = 0
term_localGlobalPrinciple_rhshttps://uor.foundation/schema/LiteralExpression
  • literalValue: all local sections glue
term_localGlobalPrinciple_forAllhttps://uor.foundation/schema/ForAllDeclaration
  • variableName: sheaf F over K