UOR Operations

IRI
https://uor.foundation/op/
Prefix
op:
Space
kernel
Comment
Ring operations, involutions, algebraic identities, and the dihedral symmetry group D_{2^n} generated by neg and bnot.

Imports

  • https://uor.foundation/schema/

Classes

NameIRISubclass OfDisjoint WithComment
Operationhttps://uor.foundation/op/Operationhttp://www.w3.org/2002/07/owl#ThingAn operation on the ring Z/(2^n)Z. The root class for all UOR kernel operations.
UnaryOphttps://uor.foundation/op/UnaryOphttps://uor.foundation/op/OperationA unary operation on the ring: takes one datum and produces one datum.
BinaryOphttps://uor.foundation/op/BinaryOphttps://uor.foundation/op/OperationA binary operation on the ring: takes two datums and produces one datum.
Involutionhttps://uor.foundation/op/Involutionhttps://uor.foundation/op/UnaryOpA unary operation f such that f(f(x)) = x for all x in R_n. The two UOR involutions are neg (ring reflection) and bnot (hypercube reflection).
Identityhttps://uor.foundation/op/Identityhttp://www.w3.org/2002/07/owl#ThingAn algebraic identity: a statement that two expressions are equal for all inputs. The critical identity is neg(bnot(x)) = succ(x) for all x in R_n.
Grouphttps://uor.foundation/op/Grouphttp://www.w3.org/2002/07/owl#ThingA group: a set with an associative binary operation, an identity element, and inverses for every element.
DihedralGrouphttps://uor.foundation/op/DihedralGrouphttps://uor.foundation/op/GroupThe dihedral group D_{2^n} of order 2^(n+1), generated by the ring reflection (neg) and the hypercube reflection (bnot). This group governs the symmetry of the UOR type space.
VerificationDomainhttps://uor.foundation/op/VerificationDomainhttp://www.w3.org/2002/07/owl#ThingA named mathematical discipline through which an algebraic identity is established and grounded. Every op:Identity individual references at least one VerificationDomain via op:verificationDomain. The nine canonical domain individuals are kernel-level constants defined in op/.
GeometricCharacterhttps://uor.foundation/op/GeometricCharacterhttp://www.w3.org/2002/07/owl#ThingThe geometric role of a ring operation in the UOR dual-geometry (ring + hypercube). Every op:Operation individual references exactly one GeometricCharacter via op:hasGeometricCharacter. The nine canonical individuals correspond to the action types of the dihedral group D_{2^n}.
WittLevelBindinghttps://uor.foundation/op/WittLevelBindinghttp://www.w3.org/2002/07/owl#ThingA record linking an op:Identity individual to a specific quantum level at which it has been verified. Non-functional: one WittLevelBinding per (Identity, WittLevel) pair verified.
QuantumThermodynamicDomainhttps://uor.foundation/op/QuantumThermodynamicDomainhttp://www.w3.org/2002/07/owl#ThingA verification domain at the intersection of quantum superposition and classical thermodynamics. Identities in this domain require both SuperpositionDomain and Thermodynamic reasoning simultaneously.
ValidityScopeKindhttps://uor.foundation/op/ValidityScopeKindhttp://www.w3.org/2002/07/owl#ThingRoot class for validity scope individuals. Instances are the four named scope kinds: Universal, ParametricLower, ParametricRange, and LevelSpecific.
ComposedOperationhttps://uor.foundation/op/ComposedOperationhttps://uor.foundation/op/Operation, https://uor.foundation/morphism/CompositionAn operation formed by composing ring operations, witnessed by op:composedOf and morphism/CompositionLaw.
DispatchOperationhttps://uor.foundation/op/DispatchOperationhttps://uor.foundation/op/ComposedOperationδ: Query × ResolverRegistry → Resolver. Non-commutative, non-associative, arity 2.
InferenceOperationhttps://uor.foundation/op/InferenceOperationhttps://uor.foundation/op/ComposedOperationι = P ∘ Π ∘ G (the φ-pipeline composed). Non-commutative, non-associative, arity 2.
AccumulationOperationhttps://uor.foundation/op/AccumulationOperationhttps://uor.foundation/op/ComposedOperationα: Binding × Context → Context. Non-commutative, associative at convergence (SR_10), arity 2.
LeasePartitionOperationhttps://uor.foundation/op/LeasePartitionOperationhttps://uor.foundation/op/ComposedOperationλ: SharedContext × ℕ → ContextLease^k. Non-commutative, non-associative, arity 2.
SessionCompositionOperationhttps://uor.foundation/op/SessionCompositionOperationhttps://uor.foundation/op/ComposedOperationκ: Session × Session → Session. Commutative (disjoint leases), associative (SR_8), arity 2.
GroupPresentationhttps://uor.foundation/op/GroupPresentationhttp://www.w3.org/2002/07/owl#ThingA structured group presentation: generators and relations as typed data rather than prose strings.

Properties

NameKindFunctionalDomainRangeComment
arityDatatypetruehttps://uor.foundation/op/Operationhttp://www.w3.org/2001/XMLSchema#nonNegativeIntegerThe number of arguments this operation takes. 1 for unary operations, 2 for binary operations.
hasGeometricCharacterObjecttruehttps://uor.foundation/op/Operationhttps://uor.foundation/op/GeometricCharacterThe geometric role of this operation in the UOR ring and hypercube geometry. Functional: each operation has exactly one geometric character.
commutativeDatatypetruehttps://uor.foundation/op/BinaryOphttp://www.w3.org/2001/XMLSchema#booleanWhether this binary operation satisfies op(x,y) = op(y,x) for all x, y in R_n.
associativeDatatypetruehttps://uor.foundation/op/BinaryOphttp://www.w3.org/2001/XMLSchema#booleanWhether this binary operation satisfies op(op(x,y),z) = op(x,op(y,z)) for all x, y, z in R_n.
identityDatatypetruehttps://uor.foundation/op/BinaryOphttp://www.w3.org/2001/XMLSchema#integerThe identity element of this binary operation: the value e such that op(x, e) = op(e, x) = x for all x in R_n.
inverseObjecttruehttps://uor.foundation/op/Operationhttps://uor.foundation/op/OperationThe inverse operation: the operation inv_op such that op(x, inv_op(x)) = e for all x, where e is the identity.
composedOfObjecttruehttps://uor.foundation/op/Operationhttp://www.w3.org/1999/02/22-rdf-syntax-ns#ListOrdered list of operations this operation is composed from. Uses rdf:List to preserve application order (first element applied innermost). E.g., succ = neg ∘ bnot is encoded as [op:neg, op:bnot] meaning neg applied to the result of bnot.
lhsObjecttruehttps://uor.foundation/op/Identityhttps://uor.foundation/schema/TermExpressionThe left-hand side of an algebraic identity as a typed AST node (schema:TermExpression).
rhsObjecttruehttps://uor.foundation/op/Identityhttps://uor.foundation/schema/TermExpressionThe right-hand side of an algebraic identity as a typed AST node (schema:TermExpression).
forAllObjecttruehttps://uor.foundation/op/Identityhttps://uor.foundation/schema/ForAllDeclarationThe quantifier scope: a typed declaration of the variable(s) over which this identity holds.
generatedByObjectfalsehttps://uor.foundation/op/Grouphttps://uor.foundation/op/OperationAn operation that generates this group. The dihedral group D_{2^n} is generated by op:neg and op:bnot.
orderDatatypetruehttps://uor.foundation/op/Grouphttp://www.w3.org/2001/XMLSchema#positiveIntegerThe number of elements in the group. For D_{2^n}, the order is 2^(n+1).
presentationAnnotationtruehttps://uor.foundation/op/Grouphttp://www.w3.org/2001/XMLSchema#stringThe group presentation (generators and relations). Example: ⟨r, s | r^{2^n} = s² = e, srs = r⁻¹⟩
verificationDomainObjectfalsehttps://uor.foundation/op/Identityhttps://uor.foundation/op/VerificationDomainThe mathematical discipline(s) through which this identity is established. Range is op:VerificationDomain. Non-functional: composite identities (e.g. IT_7a–IT_7d) reference multiple domain individuals.
verifiedAtLevelObjectfalsehttps://uor.foundation/op/Identityhttps://uor.foundation/op/WittLevelBindingLinks an Identity individual to a WittLevelBinding attesting verification at a specific quantum level. Non-functional: one binding per (Identity, WittLevel) pair.
bindingLevelObjecttruehttps://uor.foundation/op/WittLevelBindinghttps://uor.foundation/schema/WittLevelThe quantum level at which this WittLevelBinding was verified.
universallyValidDatatypetruehttps://uor.foundation/op/Identityhttp://www.w3.org/2001/XMLSchema#booleanTrue iff this identity holds for all n ≥ 1 (proved symbolically by induction on the ring axioms, not just exhaustively at Q0). Identities that reference 8-bit-specific constants receive universallyValid = false.
enumVariantObjecttruehttps://uor.foundation/op/VerificationDomainhttps://uor.foundation/op/VerificationDomainThe canonical Rust enum variant name corresponding to this VerificationDomain individual. Provides formal alignment between the OWL individual and the generated Rust enum.
validityKindObjecttruehttps://uor.foundation/op/Identityhttps://uor.foundation/op/ValidityScopeKindThe structured validity scope of this identity, replacing the binary universallyValid flag. Required on all new Identity individuals.
validKMinDatatypetruehttps://uor.foundation/op/Identityhttp://www.w3.org/2001/XMLSchema#nonNegativeIntegerMinimum quantum level index k for ParametricLower and ParametricRange scopes.
validKMaxDatatypetruehttps://uor.foundation/op/Identityhttp://www.w3.org/2001/XMLSchema#nonNegativeIntegerMaximum quantum level index k (inclusive) for ParametricRange scope.
composedOfOpsObjectfalsehttps://uor.foundation/op/ComposedOperationhttps://uor.foundation/op/OperationReferences a constituent operation of a ComposedOperation. Non-functional: a composed operation may reference multiple constituent operations.
operatorSignatureAnnotationtruehttps://uor.foundation/op/ComposedOperationhttp://www.w3.org/2001/XMLSchema#stringHuman-readable type signature describing the domain and codomain of a composed operation (e.g., 'Query × Registry → Resolver').
dispatchSourceObjecttruehttps://uor.foundation/op/DispatchOperationhttps://uor.foundation/op/OperationThe source selector for a dispatch operation.
dispatchTargetObjecttruehttps://uor.foundation/op/DispatchOperationhttps://uor.foundation/op/OperationThe target resolver for a dispatch operation.
inferenceSourceObjecttruehttps://uor.foundation/op/InferenceOperationhttps://uor.foundation/op/OperationThe source data for an inference operation.
inferenceTargetObjecttruehttps://uor.foundation/op/InferenceOperationhttps://uor.foundation/op/OperationThe target type for an inference operation.
inferencePipelineObjecttruehttps://uor.foundation/op/InferenceOperationhttps://uor.foundation/op/OperationThe pipeline through which inference is performed.
accumulationBaseObjecttruehttps://uor.foundation/op/AccumulationOperationhttps://uor.foundation/schema/TermExpressionThe base value for an accumulation operation.
accumulationBindingObjecttruehttps://uor.foundation/op/AccumulationOperationhttps://uor.foundation/schema/TermExpressionThe binding accumulator for an accumulation operation.
leaseSourceObjecttruehttps://uor.foundation/op/LeasePartitionOperationhttps://uor.foundation/op/OperationThe source context for a lease partition operation.
leaseFactorObjecttruehttps://uor.foundation/op/LeasePartitionOperationhttps://uor.foundation/op/OperationThe partition factor for a lease partition operation.
leasePartitionCountDatatypetruehttps://uor.foundation/op/LeasePartitionOperationhttp://www.w3.org/2001/XMLSchema#nonNegativeIntegerThe number of partitions in a lease partition operation.
compositionLeftSessionObjecttruehttps://uor.foundation/op/SessionCompositionOperationhttps://uor.foundation/op/OperationThe left session in a session composition operation.
compositionRightSessionObjecttruehttps://uor.foundation/op/SessionCompositionOperationhttps://uor.foundation/op/OperationThe right session in a session composition operation.
operatorDomainTypeObjecttruehttps://uor.foundation/op/ComposedOperationhttps://uor.foundation/type/TypeDefinitionThe domain type of a composed operation.
operatorRangeTypeObjecttruehttps://uor.foundation/op/ComposedOperationhttps://uor.foundation/type/TypeDefinitionThe range type of a composed operation.
operatorComplexityDatatypetruehttps://uor.foundation/op/ComposedOperationhttp://www.w3.org/2001/XMLSchema#stringThe computational complexity class of a composed operation.
operatorIdempotentDatatypetruehttps://uor.foundation/op/ComposedOperationhttp://www.w3.org/2001/XMLSchema#booleanWhether this composed operation is idempotent.
composedOperatorCountDatatypetruehttps://uor.foundation/op/ComposedOperationhttp://www.w3.org/2001/XMLSchema#nonNegativeIntegerThe number of constituent operations in a composed operation.
isInvolutoryDatatypetruehttps://uor.foundation/op/ComposedOperationhttp://www.w3.org/2001/XMLSchema#booleanWhether applying this operation twice yields the identity.
convergenceGuaranteeObjecttruehttps://uor.foundation/op/ComposedOperationhttps://uor.foundation/schema/TermExpressionDescription of the convergence guarantee for this operation.

Named Individuals

NameTypePropertiesComment
Enumerativehttps://uor.foundation/op/VerificationDomain
  • enumVariant: https://uor.foundation/op/Enumerative
Established by exhaustive traversal of R_n. Valid for all identities where the ring is finite.
Algebraichttps://uor.foundation/op/VerificationDomain
  • enumVariant: https://uor.foundation/op/Algebraic
Established by equational reasoning from ring or group axioms. Covers derivations via associativity, commutativity, inverse laws, and group presentations.
Geometrichttps://uor.foundation/op/VerificationDomain
  • enumVariant: https://uor.foundation/op/Geometric
Established by isometry, symmetry, or GeometricCharacter arguments. Covers dihedral actions, fixed-point analysis, automorphism groups, and affine embeddings.
Analyticalhttps://uor.foundation/op/VerificationDomain
  • enumVariant: https://uor.foundation/op/Analytical
Established via discrete differential calculus or metric analysis. Covers ring/Hamming derivatives (DC_), metric divergence (AM_), and adiabatic scheduling (AR_).
Thermodynamichttps://uor.foundation/op/VerificationDomain
  • enumVariant: https://uor.foundation/op/Thermodynamic
Established via entropy, Landauer bounds, or Boltzmann distributions. Covers site entropy (TH_), reversible computation (RC_), and phase transitions.
Topologicalhttps://uor.foundation/op/VerificationDomain
  • enumVariant: https://uor.foundation/op/Topological
Established via simplicial homology, cohomology, or constraint nerve analysis. Covers homological algebra (HA_) and ψ-pipeline identities.
Pipelinehttps://uor.foundation/op/VerificationDomain
  • enumVariant: https://uor.foundation/op/Pipeline
Established by the inter-algebra map structure of the resolution pipeline. Covers φ-maps (phi_1–phi_6) and ψ-maps (psi_1–psi_6).
IndexTheoretichttps://uor.foundation/op/VerificationDomain
  • enumVariant: https://uor.foundation/op/IndexTheoretic
Established by the composition of Analytical and Topological reasoning. The only domain requiring multiple op:verificationDomain assertions. Covers the UOR Index Theorem (IT_7a–IT_7d).
SuperpositionDomainhttps://uor.foundation/op/VerificationDomain
  • enumVariant: https://uor.foundation/op/SuperpositionDomain
Established by superposition analysis of site states. Covers identities involving superposed (non-classical) site assignments where sites carry complex amplitudes.
QuantumThermodynamichttps://uor.foundation/op/VerificationDomain
  • enumVariant: https://uor.foundation/op/QuantumThermodynamic
Established by the intersection of quantum superposition analysis and classical thermodynamic reasoning. Covers identities relating von Neumann entropy of superposed states to Landauer costs of projective collapse (QM_).
ArithmeticValuationhttps://uor.foundation/op/VerificationDomain
  • enumVariant: https://uor.foundation/op/ArithmeticValuation
Established by number-theoretic valuation arguments including p-adic absolute values, the Ostrowski product formula, and the arithmetic of global fields. Covers identities grounded in the product formula |x|_p · |x|_∞ = 1 and the Witt–Ostrowski derivation chain.
ComposedAlgebraichttps://uor.foundation/op/VerificationDomain
  • enumVariant: https://uor.foundation/op/ComposedAlgebraic
Verification domain for composed operation identities — algebraic properties of operator compositions including dispatch, inference, accumulation, lease, and session composition operations.
Universalhttps://uor.foundation/op/ValidityScopeKind
  • enumVariant: https://uor.foundation/op/Universal
Holds for all k in N. No minimum k constraint.
ParametricLowerhttps://uor.foundation/op/ValidityScopeKind
  • enumVariant: https://uor.foundation/op/ParametricLower
Holds for all k >= k_min, where k_min is given by validKMin.
ParametricRangehttps://uor.foundation/op/ValidityScopeKind
  • enumVariant: https://uor.foundation/op/ParametricRange
Holds for k_min <= k <= k_max. Both validKMin and validKMax required.
LevelSpecifichttps://uor.foundation/op/ValidityScopeKind
  • enumVariant: https://uor.foundation/op/LevelSpecific
Holds only at exactly one level, given by a WittLevelBinding.
RingReflectionhttps://uor.foundation/op/GeometricCharacter—Reflection through the origin of the additive ring: neg(x) = -x mod 2^n. One of the two generators of D_{2^n}.
HypercubeReflectionhttps://uor.foundation/op/GeometricCharacter—Reflection through the centre of the hypercube: bnot(x) = (2^n-1) ⊕ x. The second generator of D_{2^n}.
Rotationhttps://uor.foundation/op/GeometricCharacter—Rotation by one step: succ(x) = (x+1) mod 2^n. The composition of the two reflections.
RotationInversehttps://uor.foundation/op/GeometricCharacter—Rotation by one step in the reverse direction: pred(x) = (x-1) mod 2^n.
Translationhttps://uor.foundation/op/GeometricCharacter—Translation along the ring axis: add(x,y), sub(x,y). Preserves Hamming distance locally.
Scalinghttps://uor.foundation/op/GeometricCharacter—Scaling along the ring axis: mul(x,y) = (x×y) mod 2^n.
HypercubeTranslationhttps://uor.foundation/op/GeometricCharacter—Translation along the hypercube axis: xor(x,y) = x ⊕ y. Preserves ring distance locally.
HypercubeProjectionhttps://uor.foundation/op/GeometricCharacter—Projection onto a hypercube face: and(x,y) = x ∧ y. Idempotent; collapses dimensions.
HypercubeJoinhttps://uor.foundation/op/GeometricCharacter—Join on the hypercube lattice: or(x,y) = x ∨ y. Idempotent; dual to projection.
ConstraintSelectionhttps://uor.foundation/op/GeometricCharacter—Geometric character of dispatch: constraint-guided selection over the resolver registry lattice.
ResolutionTraversalhttps://uor.foundation/op/GeometricCharacter—Geometric character of inference: traversal through the φ-pipeline resolution graph P ∘ Π ∘ G.
SiteBindinghttps://uor.foundation/op/GeometricCharacter—Geometric character of accumulation: progressive pinning of site states in the context lattice.
SitePartitionhttps://uor.foundation/op/GeometricCharacter—Geometric character of lease partition: splitting a shared context into disjoint site-set leases.
SessionMergehttps://uor.foundation/op/GeometricCharacter—Geometric character of session composition: merging disjoint lease sessions into a unified resolution context.
neghttps://uor.foundation/op/Involution
  • arity: 1
  • hasGeometricCharacter: https://uor.foundation/op/RingReflection
Ring reflection: neg(x) = (-x) mod 2^n. One of the two generators of the dihedral group D_{2^n}. neg(neg(x)) = x (involution property).
bnothttps://uor.foundation/op/Involution
  • arity: 1
  • hasGeometricCharacter: https://uor.foundation/op/HypercubeReflection
Hypercube reflection: bnot(x) = (2^n - 1) ⊕ x (bitwise complement). The second generator of D_{2^n}. bnot(bnot(x)) = x.
succhttps://uor.foundation/op/UnaryOp
  • arity: 1
  • hasGeometricCharacter: https://uor.foundation/op/Rotation
  • composedOf: [https://uor.foundation/op/neg, https://uor.foundation/op/bnot]
  • inverse: https://uor.foundation/op/pred
Successor: succ(x) = neg(bnot(x)) = (x + 1) mod 2^n. The critical identity: succ is the composition neg ∘ bnot.
predhttps://uor.foundation/op/UnaryOp
  • arity: 1
  • hasGeometricCharacter: https://uor.foundation/op/RotationInverse
  • composedOf: [https://uor.foundation/op/bnot, https://uor.foundation/op/neg]
  • inverse: https://uor.foundation/op/succ
Predecessor: pred(x) = bnot(neg(x)) = (x - 1) mod 2^n. The inverse of succ. pred is the composition bnot ∘ neg.
addhttps://uor.foundation/op/BinaryOp
  • arity: 2
  • hasGeometricCharacter: https://uor.foundation/op/Translation
  • commutative: true
  • associative: true
  • identity: 0
  • inverse: https://uor.foundation/op/sub
Ring addition: add(x, y) = (x + y) mod 2^n. Commutative, associative; identity element is 0.
subhttps://uor.foundation/op/BinaryOp
  • arity: 2
  • hasGeometricCharacter: https://uor.foundation/op/Translation
  • commutative: false
  • associative: false
Ring subtraction: sub(x, y) = (x - y) mod 2^n. Not commutative, not associative.
mulhttps://uor.foundation/op/BinaryOp
  • arity: 2
  • hasGeometricCharacter: https://uor.foundation/op/Scaling
  • commutative: true
  • associative: true
  • identity: 1
Ring multiplication: mul(x, y) = (x × y) mod 2^n. Commutative, associative; identity element is 1.
xorhttps://uor.foundation/op/BinaryOp
  • arity: 2
  • hasGeometricCharacter: https://uor.foundation/op/HypercubeTranslation
  • commutative: true
  • associative: true
  • identity: 0
Bitwise exclusive or: xor(x, y) = x ⊕ y. Commutative, associative; identity element is 0.
andhttps://uor.foundation/op/BinaryOp
  • arity: 2
  • hasGeometricCharacter: https://uor.foundation/op/HypercubeProjection
  • commutative: true
  • associative: true
Bitwise and: and(x, y) = x ∧ y. Commutative, associative.
orhttps://uor.foundation/op/BinaryOp
  • arity: 2
  • hasGeometricCharacter: https://uor.foundation/op/HypercubeJoin
  • commutative: true
  • associative: true
Bitwise or: or(x, y) = x ∨ y. Commutative, associative.
dispatchhttps://uor.foundation/op/DispatchOperation
  • arity: 2
  • hasGeometricCharacter: https://uor.foundation/op/ConstraintSelection
  • commutative: false
  • associative: false
  • operatorSignature: Query × ResolverRegistry → Resolver
δ(q, R) = R(q): dispatches a query to the matching resolver in the registry. Non-commutative, non-associative.
inferhttps://uor.foundation/op/InferenceOperation
  • arity: 2
  • hasGeometricCharacter: https://uor.foundation/op/ResolutionTraversal
  • commutative: false
  • associative: false
  • operatorSignature: Symbol × Context → ResolvedType
ι(s, C) = P(Π(G(s, C))): the φ-pipeline composed into a single inference step. Non-commutative, non-associative.
accumulatehttps://uor.foundation/op/AccumulationOperation
  • arity: 2
  • hasGeometricCharacter: https://uor.foundation/op/SiteBinding
  • commutative: false
  • associative: true
  • operatorSignature: Binding × Context → Context
α(b, C) = C': accumulates a binding into a resolution context, pinning a site. Non-commutative, associative at convergence (SR_10).
partition_ophttps://uor.foundation/op/LeasePartitionOperation
  • arity: 2
  • hasGeometricCharacter: https://uor.foundation/op/SitePartition
  • commutative: false
  • associative: false
  • operatorSignature: SharedContext × ℕ → ContextLease^k
λ(S, k) = (L₁, …, Lₖ): partitions a shared context into k disjoint leases. Non-commutative, non-associative.
compose_ophttps://uor.foundation/op/SessionCompositionOperation
  • arity: 2
  • hasGeometricCharacter: https://uor.foundation/op/SessionMerge
  • commutative: true
  • associative: true
  • operatorSignature: Session × Session → Session
κ(S₁, S₂) = S₁ ∪ S₂: composes two sessions with disjoint leases into one. Commutative, associative (SR_8).
Critical Identityhttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/op/succ
  • rhs: [https://uor.foundation/op/neg, https://uor.foundation/op/bnot]
  • forAll: https://uor.foundation/schema/term_criticalIdentity_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
The foundational theorem of the UOR kernel: neg(bnot(x)) = succ(x) for all x in R_n. This identity links the two involutions (neg and bnot) to the successor operation, making succ derivable from neg and bnot.
R_A1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_R_A1_lhs
  • rhs: https://uor.foundation/schema/term_R_A1_rhs
  • forAll: https://uor.foundation/schema/term_R_A1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Additive associativity: add(x, add(y, z)) = add(add(x, y), z).
R_A2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_R_A2_lhs
  • rhs: https://uor.foundation/schema/term_R_A2_rhs
  • forAll: https://uor.foundation/schema/term_R_A2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Additive identity: add(x, 0) = x.
R_A3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_R_A3_lhs
  • rhs: https://uor.foundation/schema/term_R_A3_rhs
  • forAll: https://uor.foundation/schema/term_R_A3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Additive inverse: add(x, neg(x)) = 0.
R_A4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_R_A4_lhs
  • rhs: https://uor.foundation/schema/term_R_A4_rhs
  • forAll: https://uor.foundation/schema/term_R_A4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Additive commutativity: add(x, y) = add(y, x).
R_A5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_R_A5_lhs
  • rhs: https://uor.foundation/schema/term_R_A5_rhs
  • forAll: https://uor.foundation/schema/term_R_A5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Subtraction definition: sub(x, y) = add(x, neg(y)).
R_A6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_R_A6_lhs
  • rhs: https://uor.foundation/schema/term_R_A6_rhs
  • forAll: https://uor.foundation/schema/term_R_A6_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Negation involution: neg(neg(x)) = x.
R_M1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_R_M1_lhs
  • rhs: https://uor.foundation/schema/term_R_M1_rhs
  • forAll: https://uor.foundation/schema/term_R_M1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Multiplicative associativity: mul(x, mul(y, z)) = mul(mul(x, y), z).
R_M2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_R_M2_lhs
  • rhs: https://uor.foundation/schema/term_R_M2_rhs
  • forAll: https://uor.foundation/schema/term_R_M2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Multiplicative identity: mul(x, 1) = x.
R_M3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_R_M3_lhs
  • rhs: https://uor.foundation/schema/term_R_M3_rhs
  • forAll: https://uor.foundation/schema/term_R_M3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Multiplicative commutativity: mul(x, y) = mul(y, x).
R_M4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_R_M4_lhs
  • rhs: https://uor.foundation/schema/term_R_M4_rhs
  • forAll: https://uor.foundation/schema/term_R_M4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Distributivity: mul(x, add(y, z)) = add(mul(x, y), mul(x, z)).
R_M5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_R_M5_lhs
  • rhs: https://uor.foundation/schema/term_R_M5_rhs
  • forAll: https://uor.foundation/schema/term_R_M5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Annihilation: mul(x, 0) = 0.
B_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_B_1_lhs
  • rhs: https://uor.foundation/schema/term_B_1_rhs
  • forAll: https://uor.foundation/schema/term_B_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
XOR associativity: xor(x, xor(y, z)) = xor(xor(x, y), z).
B_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_B_2_lhs
  • rhs: https://uor.foundation/schema/term_B_2_rhs
  • forAll: https://uor.foundation/schema/term_B_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
XOR identity: xor(x, 0) = x.
B_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_B_3_lhs
  • rhs: https://uor.foundation/schema/term_B_3_rhs
  • forAll: https://uor.foundation/schema/term_B_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
XOR self-inverse: xor(x, x) = 0.
B_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_B_4_lhs
  • rhs: https://uor.foundation/schema/term_B_4_rhs
  • forAll: https://uor.foundation/schema/term_B_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
AND associativity: and(x, and(y, z)) = and(and(x, y), z).
B_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_B_5_lhs
  • rhs: https://uor.foundation/schema/term_B_5_rhs
  • forAll: https://uor.foundation/schema/term_B_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
AND identity: and(x, 2^n - 1) = x.
B_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_B_6_lhs
  • rhs: https://uor.foundation/schema/term_B_6_rhs
  • forAll: https://uor.foundation/schema/term_B_6_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
AND annihilation: and(x, 0) = 0.
B_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_B_7_lhs
  • rhs: https://uor.foundation/schema/term_B_7_rhs
  • forAll: https://uor.foundation/schema/term_B_7_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
OR associativity: or(x, or(y, z)) = or(or(x, y), z).
B_8https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_B_8_lhs
  • rhs: https://uor.foundation/schema/term_B_8_rhs
  • forAll: https://uor.foundation/schema/term_B_8_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
OR identity: or(x, 0) = x.
B_9https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_B_9_lhs
  • rhs: https://uor.foundation/schema/term_B_9_rhs
  • forAll: https://uor.foundation/schema/term_B_9_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Absorption: and(x, or(x, y)) = x.
B_10https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_B_10_lhs
  • rhs: https://uor.foundation/schema/term_B_10_rhs
  • forAll: https://uor.foundation/schema/term_B_10_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
AND distributes over OR: and(x, or(y, z)) = or(and(x, y), and(x, z)).
B_11https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_B_11_lhs
  • rhs: https://uor.foundation/schema/term_B_11_rhs
  • forAll: https://uor.foundation/schema/term_B_11_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
De Morgan 1: bnot(and(x, y)) = or(bnot(x), bnot(y)).
B_12https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_B_12_lhs
  • rhs: https://uor.foundation/schema/term_B_12_rhs
  • forAll: https://uor.foundation/schema/term_B_12_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
De Morgan 2: bnot(or(x, y)) = and(bnot(x), bnot(y)).
B_13https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_B_13_lhs
  • rhs: https://uor.foundation/schema/term_B_13_rhs
  • forAll: https://uor.foundation/schema/term_B_13_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Bnot involution: bnot(bnot(x)) = x.
X_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_X_1_lhs
  • rhs: https://uor.foundation/schema/term_X_1_rhs
  • forAll: https://uor.foundation/schema/term_X_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Neg via subtraction: neg(x) = sub(0, x).
X_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_X_2_lhs
  • rhs: https://uor.foundation/schema/term_X_2_rhs
  • forAll: https://uor.foundation/schema/term_X_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Complement via XOR: bnot(x) = xor(x, 2^n - 1).
X_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_X_3_lhs
  • rhs: https://uor.foundation/schema/term_X_3_rhs
  • forAll: https://uor.foundation/schema/term_X_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Succ via addition: succ(x) = add(x, 1).
X_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_X_4_lhs
  • rhs: https://uor.foundation/schema/term_X_4_rhs
  • forAll: https://uor.foundation/schema/term_X_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Pred via subtraction: pred(x) = sub(x, 1).
X_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_X_5_lhs
  • rhs: https://uor.foundation/schema/term_X_5_rhs
  • forAll: https://uor.foundation/schema/term_X_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Neg-bnot bridge: neg(x) = add(bnot(x), 1).
X_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_X_6_lhs
  • rhs: https://uor.foundation/schema/term_X_6_rhs
  • forAll: https://uor.foundation/schema/term_X_6_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Complement predecessor: bnot(x) = pred(neg(x)).
X_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_X_7_lhs
  • rhs: https://uor.foundation/schema/term_X_7_rhs
  • forAll: https://uor.foundation/schema/term_X_7_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
XOR-add bridge: xor(x, y) = add(x, y) - 2 * and(x, y) (in Z before mod).
D_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_D_1_lhs
  • rhs: https://uor.foundation/schema/term_D_1_rhs
  • forAll: https://uor.foundation/schema/term_D_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Rotation order: succ^[2^n](x) = x.
D_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_D_3_lhs
  • rhs: https://uor.foundation/schema/term_D_3_rhs
  • forAll: https://uor.foundation/schema/term_D_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Conjugation: neg(succ(neg(x))) = pred(x).
D_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_D_4_lhs
  • rhs: https://uor.foundation/schema/term_D_4_rhs
  • forAll: https://uor.foundation/schema/term_D_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Reverse composition: bnot(neg(x)) = pred(x).
D_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_D_5_lhs
  • rhs: https://uor.foundation/schema/term_D_5_rhs
  • forAll: https://uor.foundation/schema/term_D_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Group closure: D_[2^n] = [succ^k, neg ∘ succ^k : 0 ≤ k < 2^n].
U_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_U_1_lhs
  • rhs: https://uor.foundation/schema/term_U_1_rhs
  • forAll: https://uor.foundation/schema/term_U_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Unit group decomposition: R_n× ≅ Z/2 × Z/2^[n-2] for n ≥ 3.
U_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_U_2_lhs
  • rhs: https://uor.foundation/schema/term_U_2_rhs
  • forAll: https://uor.foundation/schema/term_U_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Unit group special cases: R_1× ≅ [1]; R_2× ≅ Z/2.
U_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_U_3_lhs
  • rhs: https://uor.foundation/schema/term_U_3_rhs
  • forAll: https://uor.foundation/schema/term_U_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Multiplicative order: ord(u) = lcm(ord((-1)^a), ord(3^b)).
U_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_U_4_lhs
  • rhs: https://uor.foundation/schema/term_U_4_rhs
  • forAll: https://uor.foundation/schema/term_U_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Resonance period: ord_g(2) divides φ(g).
U_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_U_5_lhs
  • rhs: https://uor.foundation/schema/term_U_5_rhs
  • forAll: https://uor.foundation/schema/term_U_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Step formula derivation: step_g = 2 * ((g - (2^n mod g)) mod g) + 1.
AG_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AG_1_lhs
  • rhs: https://uor.foundation/schema/term_AG_1_rhs
  • forAll: https://uor.foundation/schema/term_AG_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Scaling not dihedral: μ_u ∉ D_[2^n] for u ≠ ±1.
AG_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AG_2_lhs
  • rhs: https://uor.foundation/schema/term_AG_2_rhs
  • forAll: https://uor.foundation/schema/term_AG_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Affine group: Aff(R_n) = R_n× ⋉ R_n.
AG_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AG_3_lhs
  • rhs: https://uor.foundation/schema/term_AG_3_rhs
  • forAll: https://uor.foundation/schema/term_AG_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Affine group order: |Aff(R_n)| = 2^[2n-1].
AG_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AG_4_lhs
  • rhs: https://uor.foundation/schema/term_AG_4_rhs
  • forAll: https://uor.foundation/schema/term_AG_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Subgroup inclusion: D_[2^n] ⊂ Aff(R_n) with u ∈ [±1].
CA_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CA_1_lhs
  • rhs: https://uor.foundation/schema/term_CA_1_rhs
  • forAll: https://uor.foundation/schema/term_CA_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Addition decomposition: add(x,y)_k = xor(x_k, xor(y_k, c_k(x,y))).
CA_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CA_2_lhs
  • rhs: https://uor.foundation/schema/term_CA_2_rhs
  • forAll: https://uor.foundation/schema/term_CA_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Carry recurrence: c_[k+1](x,y) = or(and(x_k,y_k), and(xor(x_k,y_k), c_k)).
CA_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CA_3_lhs
  • rhs: https://uor.foundation/schema/term_CA_3_rhs
  • forAll: https://uor.foundation/schema/term_CA_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Carry commutativity: c(x, y) = c(y, x).
CA_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CA_4_lhs
  • rhs: https://uor.foundation/schema/term_CA_4_rhs
  • forAll: https://uor.foundation/schema/term_CA_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Zero carry: c(x, 0) = 0 at all positions.
CA_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CA_5_lhs
  • rhs: https://uor.foundation/schema/term_CA_5_rhs
  • forAll: https://uor.foundation/schema/term_CA_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Negation carry: c(x, neg(x))_k = 1 for k > v_2(x).
CA_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CA_6_lhs
  • rhs: https://uor.foundation/schema/term_CA_6_rhs
  • forAll: https://uor.foundation/schema/term_CA_6_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Carry-incompatibility link: d_Δ(x, y) > 0 iff ∃ k : c_k(x,y) = 1.
C_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_C_1_lhs
  • rhs: https://uor.foundation/schema/term_C_1_rhs
  • forAll: https://uor.foundation/schema/term_C_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Constraint pin union: pins of a composite constraint equal the union of component pins.
C_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_C_2_lhs
  • rhs: https://uor.foundation/schema/term_C_2_rhs
  • forAll: https://uor.foundation/schema/term_C_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Constraint composition commutativity.
C_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_C_3_lhs
  • rhs: https://uor.foundation/schema/term_C_3_rhs
  • forAll: https://uor.foundation/schema/term_C_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Constraint composition associativity.
C_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_C_4_lhs
  • rhs: https://uor.foundation/schema/term_C_4_rhs
  • forAll: https://uor.foundation/schema/term_C_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Constraint composition idempotence.
C_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_C_5_lhs
  • rhs: https://uor.foundation/schema/term_C_5_rhs
  • forAll: https://uor.foundation/schema/term_C_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Constraint composition identity element.
C_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_C_6_lhs
  • rhs: https://uor.foundation/schema/term_C_6_rhs
  • forAll: https://uor.foundation/schema/term_C_6_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Constraint composition annihilator.
CDIhttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CDI_lhs
  • rhs: https://uor.foundation/schema/term_CDI_rhs
  • forAll: https://uor.foundation/schema/term_CDI_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Constraint-depth invariant: carry complexity of the residue representation equals the type depth.
CL_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CL_1_lhs
  • rhs: https://uor.foundation/schema/term_CL_1_rhs
  • forAll: https://uor.foundation/schema/term_CL_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Constraint quotient lattice isomorphism to power set.
CL_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CL_2_lhs
  • rhs: https://uor.foundation/schema/term_CL_2_rhs
  • forAll: https://uor.foundation/schema/term_CL_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Lattice join equals constraint composition.
CL_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CL_3_lhs
  • rhs: https://uor.foundation/schema/term_CL_3_rhs
  • forAll: https://uor.foundation/schema/term_CL_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Lattice meet pins the intersection of component pins.
CL_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CL_4_lhs
  • rhs: https://uor.foundation/schema/term_CL_4_rhs
  • forAll: https://uor.foundation/schema/term_CL_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Constraint lattice distributivity.
CL_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CL_5_lhs
  • rhs: https://uor.foundation/schema/term_CL_5_rhs
  • forAll: https://uor.foundation/schema/term_CL_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Constraint lattice complement existence.
CM_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CM_1_lhs
  • rhs: https://uor.foundation/schema/term_CM_1_rhs
  • forAll: https://uor.foundation/schema/term_CM_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Constraint redundancy criterion.
CM_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CM_2_lhs
  • rhs: https://uor.foundation/schema/term_CM_2_rhs
  • forAll: https://uor.foundation/schema/term_CM_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Minimal cover via greedy irredundant removal.
CM_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CM_3_lhs
  • rhs: https://uor.foundation/schema/term_CM_3_rhs
  • forAll: https://uor.foundation/schema/term_CM_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Minimum constraint count to cover n sites.
CR_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CR_1_lhs
  • rhs: https://uor.foundation/schema/term_CR_1_rhs
  • forAll: https://uor.foundation/schema/term_CR_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Residue constraint cost is the step formula.
CR_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CR_2_lhs
  • rhs: https://uor.foundation/schema/term_CR_2_rhs
  • forAll: https://uor.foundation/schema/term_CR_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Carry constraint cost is the popcount of the pattern.
CR_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CR_3_lhs
  • rhs: https://uor.foundation/schema/term_CR_3_rhs
  • forAll: https://uor.foundation/schema/term_CR_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Depth constraint cost is sum of residue and carry costs.
CR_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CR_4_lhs
  • rhs: https://uor.foundation/schema/term_CR_4_rhs
  • forAll: https://uor.foundation/schema/term_CR_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Composite constraint cost is subadditive.
CR_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CR_5_lhs
  • rhs: https://uor.foundation/schema/term_CR_5_rhs
  • forAll: https://uor.foundation/schema/term_CR_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Optimal resolution order is increasing cost.
F_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_F_1_lhs
  • rhs: https://uor.foundation/schema/term_F_1_rhs
  • forAll: https://uor.foundation/schema/term_F_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Site monotonicity: a pinned site cannot be unpinned.
F_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_F_2_lhs
  • rhs: https://uor.foundation/schema/term_F_2_rhs
  • forAll: https://uor.foundation/schema/term_F_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Site budget upper bound: at most n pin operations to close.
F_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_F_3_lhs
  • rhs: https://uor.foundation/schema/term_F_3_rhs
  • forAll: https://uor.foundation/schema/term_F_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Site budget conservation: pinned + free = total sites.
F_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_F_4_lhs
  • rhs: https://uor.foundation/schema/term_F_4_rhs
  • forAll: https://uor.foundation/schema/term_F_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Site budget closure: closed iff all sites pinned.
FL_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FL_1_lhs
  • rhs: https://uor.foundation/schema/term_FL_1_rhs
  • forAll: https://uor.foundation/schema/term_FL_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Site lattice bottom: all sites free.
FL_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FL_2_lhs
  • rhs: https://uor.foundation/schema/term_FL_2_rhs
  • forAll: https://uor.foundation/schema/term_FL_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Site lattice top: all sites pinned.
FL_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FL_3_lhs
  • rhs: https://uor.foundation/schema/term_FL_3_rhs
  • forAll: https://uor.foundation/schema/term_FL_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Site lattice join is union of pinnings.
FL_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FL_4_lhs
  • rhs: https://uor.foundation/schema/term_FL_4_rhs
  • forAll: https://uor.foundation/schema/term_FL_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Site lattice height equals n.
FPM_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FPM_1_lhs
  • rhs: https://uor.foundation/schema/term_FPM_1_rhs
  • forAll: https://uor.foundation/schema/term_FPM_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Unit partition membership: x is a unit iff site_0(x) = 1 (x is odd).
FPM_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FPM_2_lhs
  • rhs: https://uor.foundation/schema/term_FPM_2_rhs
  • forAll: https://uor.foundation/schema/term_FPM_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Exterior partition membership: x is exterior iff x is not in the carrier of T.
FPM_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FPM_3_lhs
  • rhs: https://uor.foundation/schema/term_FPM_3_rhs
  • forAll: https://uor.foundation/schema/term_FPM_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Irreducible partition membership: x is irreducible iff x is not a unit, exterior, or reducible.
FPM_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FPM_4_lhs
  • rhs: https://uor.foundation/schema/term_FPM_4_rhs
  • forAll: https://uor.foundation/schema/term_FPM_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Reducible partition membership: x is reducible iff x is not a unit, exterior, or irreducible.
FPM_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FPM_5_lhs
  • rhs: https://uor.foundation/schema/term_FPM_5_rhs
  • forAll: https://uor.foundation/schema/term_FPM_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
2-adic decomposition: every element factors as 2^{v(x)} times an odd unit.
FPM_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FPM_6_lhs
  • rhs: https://uor.foundation/schema/term_FPM_6_rhs
  • forAll: https://uor.foundation/schema/term_FPM_6_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Stratum size formula.
FPM_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FPM_7_lhs
  • rhs: https://uor.foundation/schema/term_FPM_7_rhs
  • forAll: https://uor.foundation/schema/term_FPM_7_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Base type partition cardinalities.
FS_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FS_1_lhs
  • rhs: https://uor.foundation/schema/term_FS_1_rhs
  • forAll: https://uor.foundation/schema/term_FS_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Site extraction: site_k(x) is the k-th bit of x.
FS_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FS_2_lhs
  • rhs: https://uor.foundation/schema/term_FS_2_rhs
  • forAll: https://uor.foundation/schema/term_FS_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Site 0 is parity.
FS_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FS_3_lhs
  • rhs: https://uor.foundation/schema/term_FS_3_rhs
  • forAll: https://uor.foundation/schema/term_FS_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Progressive site determination: site_k given lower sites determines x mod 2^{k+1}.
FS_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FS_4_lhs
  • rhs: https://uor.foundation/schema/term_FS_4_rhs
  • forAll: https://uor.foundation/schema/term_FS_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Cumulative site determination: sites 0..k together determine x mod 2^{k+1}.
FS_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FS_5_lhs
  • rhs: https://uor.foundation/schema/term_FS_5_rhs
  • forAll: https://uor.foundation/schema/term_FS_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Complete site determination: all n sites determine x uniquely.
FS_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FS_6_lhs
  • rhs: https://uor.foundation/schema/term_FS_6_rhs
  • forAll: https://uor.foundation/schema/term_FS_6_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Stratum from sites: v_2(x) is the minimum k where site_k(x) = 1.
FS_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FS_7_lhs
  • rhs: https://uor.foundation/schema/term_FS_7_rhs
  • forAll: https://uor.foundation/schema/term_FS_7_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Depth bound: depth(x) ≤ v_2(x) for irreducible elements.
RE_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_RE_1_lhs
  • rhs: https://uor.foundation/schema/term_RE_1_rhs
  • forAll: https://uor.foundation/schema/term_RE_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Resolution strategy equivalence: dihedral, canonical-form, and evaluation resolvers all compute the same partition.
IR_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IR_1_lhs
  • rhs: https://uor.foundation/schema/term_IR_1_rhs
  • forAll: https://uor.foundation/schema/term_IR_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Resolution monotonicity: pinned count never decreases.
IR_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IR_2_lhs
  • rhs: https://uor.foundation/schema/term_IR_2_rhs
  • forAll: https://uor.foundation/schema/term_IR_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Resolution convergence bound: at most n iterations.
IR_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IR_3_lhs
  • rhs: https://uor.foundation/schema/term_IR_3_rhs
  • forAll: https://uor.foundation/schema/term_IR_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Convergence rate definition.
IR_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IR_4_lhs
  • rhs: https://uor.foundation/schema/term_IR_4_rhs
  • forAll: https://uor.foundation/schema/term_IR_4_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Resolution termination: loop terminates if constraint set spans all sites.
SF_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SF_1_lhs
  • rhs: https://uor.foundation/schema/term_SF_1_rhs
  • forAll: https://uor.foundation/schema/term_SF_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Optimal resolution level for a factor: n ≡ 0 (mod ord_g(2)).
SF_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SF_2_lhs
  • rhs: https://uor.foundation/schema/term_SF_2_rhs
  • forAll: https://uor.foundation/schema/term_SF_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Constraint ordering by step cost: smaller step_g first.
RD_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_RD_1_lhs
  • rhs: https://uor.foundation/schema/term_RD_1_rhs
  • forAll: https://uor.foundation/schema/term_RD_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Resolution determinism: same type and constraint sequence yield unique partition.
RD_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_RD_2_lhs
  • rhs: https://uor.foundation/schema/term_RD_2_rhs
  • forAll: https://uor.foundation/schema/term_RD_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Order independence: complete constraint sets yield the same partition regardless of order.
SE_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SE_1_lhs
  • rhs: https://uor.foundation/schema/term_SE_1_rhs
  • forAll: https://uor.foundation/schema/term_SE_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Evaluation resolver directly computes the set-theoretic partition.
SE_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SE_2_lhs
  • rhs: https://uor.foundation/schema/term_SE_2_rhs
  • forAll: https://uor.foundation/schema/term_SE_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Dihedral factorization resolver yields the same partition via orbit decomposition.
SE_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SE_3_lhs
  • rhs: https://uor.foundation/schema/term_SE_3_rhs
  • forAll: https://uor.foundation/schema/term_SE_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Canonical form resolver yields the same partition via confluent rewrite.
SE_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SE_4_lhs
  • rhs: https://uor.foundation/schema/term_SE_4_rhs
  • forAll: https://uor.foundation/schema/term_SE_4_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
All three strategies compute the same set-theoretic partition.
OO_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OO_1_lhs
  • rhs: https://uor.foundation/schema/term_OO_1_rhs
  • forAll: https://uor.foundation/schema/term_OO_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Benefit of a constraint is the number of new pins it provides.
OO_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OO_2_lhs
  • rhs: https://uor.foundation/schema/term_OO_2_rhs
  • forAll: https://uor.foundation/schema/term_OO_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Constraint cost is step or popcount depending on type.
OO_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OO_3_lhs
  • rhs: https://uor.foundation/schema/term_OO_3_rhs
  • forAll: https://uor.foundation/schema/term_OO_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Greedy selection maximizes benefit-to-cost ratio.
OO_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OO_4_lhs
  • rhs: https://uor.foundation/schema/term_OO_4_rhs
  • forAll: https://uor.foundation/schema/term_OO_4_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Greedy approximation achieves (1 − 1/e) ≈ 63% of optimal.
OO_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OO_5_lhs
  • rhs: https://uor.foundation/schema/term_OO_5_rhs
  • forAll: https://uor.foundation/schema/term_OO_5_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Tiebreaker: prefer vertical (residue) before horizontal (carry).
CB_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CB_1_lhs
  • rhs: https://uor.foundation/schema/term_CB_1_rhs
  • forAll: https://uor.foundation/schema/term_CB_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Minimum convergence rate: 1 site per iteration (worst case).
CB_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CB_2_lhs
  • rhs: https://uor.foundation/schema/term_CB_2_rhs
  • forAll: https://uor.foundation/schema/term_CB_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Maximum convergence rate: n sites in 1 iteration (best case).
CB_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CB_3_lhs
  • rhs: https://uor.foundation/schema/term_CB_3_rhs
  • forAll: https://uor.foundation/schema/term_CB_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Expected residue constraint rate: ⌊log_2(m)⌋ sites per constraint.
CB_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CB_4_lhs
  • rhs: https://uor.foundation/schema/term_CB_4_rhs
  • forAll: https://uor.foundation/schema/term_CB_4_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Stall detection: convergenceRate < 1 for 2 iterations suggests insufficiency.
CB_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CB_5_lhs
  • rhs: https://uor.foundation/schema/term_CB_5_rhs
  • forAll: https://uor.foundation/schema/term_CB_5_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Sufficiency criterion: pin union covers all site positions.
CB_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CB_6_lhs
  • rhs: https://uor.foundation/schema/term_CB_6_rhs
  • forAll: https://uor.foundation/schema/term_CB_6_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Iteration bound for k constraints: at most min(k, n) iterations.
OB_M1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OB_M1_lhs
  • rhs: https://uor.foundation/schema/term_OB_M1_rhs
  • forAll: https://uor.foundation/schema/term_OB_M1_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Ring metric triangle inequality.
OB_M2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OB_M2_lhs
  • rhs: https://uor.foundation/schema/term_OB_M2_rhs
  • forAll: https://uor.foundation/schema/term_OB_M2_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Hamming metric triangle inequality.
OB_M3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OB_M3_lhs
  • rhs: https://uor.foundation/schema/term_OB_M3_rhs
  • forAll: https://uor.foundation/schema/term_OB_M3_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Incompatibility metric is the absolute difference of ring and Hamming metrics.
OB_M4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OB_M4_lhs
  • rhs: https://uor.foundation/schema/term_OB_M4_rhs
  • forAll: https://uor.foundation/schema/term_OB_M4_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Negation preserves ring metric.
OB_M5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OB_M5_lhs
  • rhs: https://uor.foundation/schema/term_OB_M5_rhs
  • forAll: https://uor.foundation/schema/term_OB_M5_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Bitwise complement preserves Hamming metric.
OB_M6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OB_M6_lhs
  • rhs: https://uor.foundation/schema/term_OB_M6_rhs
  • forAll: https://uor.foundation/schema/term_OB_M6_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Successor preserves ring metric but may change Hamming metric.
OB_C1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OB_C1_lhs
  • rhs: https://uor.foundation/schema/term_OB_C1_rhs
  • forAll: https://uor.foundation/schema/term_OB_C1_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Negation-complement commutator is constant 2.
OB_C2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OB_C2_lhs
  • rhs: https://uor.foundation/schema/term_OB_C2_rhs
  • forAll: https://uor.foundation/schema/term_OB_C2_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Negation-translation commutator.
OB_C3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OB_C3_lhs
  • rhs: https://uor.foundation/schema/term_OB_C3_rhs
  • forAll: https://uor.foundation/schema/term_OB_C3_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Complement-XOR commutator is trivial.
OB_H1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OB_H1_lhs
  • rhs: https://uor.foundation/schema/term_OB_H1_rhs
  • forAll: https://uor.foundation/schema/term_OB_H1_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Additive paths have trivial monodromy (abelian ⇒ path-independent).
OB_H2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OB_H2_lhs
  • rhs: https://uor.foundation/schema/term_OB_H2_rhs
  • forAll: https://uor.foundation/schema/term_OB_H2_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Dihedral generator paths have monodromy in D_{2^n}.
OB_H3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OB_H3_lhs
  • rhs: https://uor.foundation/schema/term_OB_H3_rhs
  • forAll: https://uor.foundation/schema/term_OB_H3_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Successor-only closed path winding number.
OB_P1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OB_P1_lhs
  • rhs: https://uor.foundation/schema/term_OB_P1_rhs
  • forAll: https://uor.foundation/schema/term_OB_P1_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Path length is additive under concatenation.
OB_P2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OB_P2_lhs
  • rhs: https://uor.foundation/schema/term_OB_P2_rhs
  • forAll: https://uor.foundation/schema/term_OB_P2_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Total variation is subadditive under concatenation.
OB_P3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OB_P3_lhs
  • rhs: https://uor.foundation/schema/term_OB_P3_rhs
  • forAll: https://uor.foundation/schema/term_OB_P3_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Reduction length is additive under sequential composition.
CT_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CT_1_lhs
  • rhs: https://uor.foundation/schema/term_CT_1_rhs
  • forAll: https://uor.foundation/schema/term_CT_1_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Catastrophe boundaries are powers of 2.
CT_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CT_2_lhs
  • rhs: https://uor.foundation/schema/term_CT_2_rhs
  • forAll: https://uor.foundation/schema/term_CT_2_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Odd prime catastrophe transitions visibility via residue constraints.
CT_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CT_3_lhs
  • rhs: https://uor.foundation/schema/term_CT_3_rhs
  • forAll: https://uor.foundation/schema/term_CT_3_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Catastrophe threshold is normalized step cost.
CT_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CT_4_lhs
  • rhs: https://uor.foundation/schema/term_CT_4_rhs
  • forAll: https://uor.foundation/schema/term_CT_4_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Composite catastrophe threshold is max of component thresholds.
CF_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CF_1_lhs
  • rhs: https://uor.foundation/schema/term_CF_1_rhs
  • forAll: https://uor.foundation/schema/term_CF_1_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Curvature flux is the sum of incompatibility along a path.
CF_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CF_2_lhs
  • rhs: https://uor.foundation/schema/term_CF_2_rhs
  • forAll: https://uor.foundation/schema/term_CF_2_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Resolution cost is bounded below by curvature flux of optimal path.
CF_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CF_3_lhs
  • rhs: https://uor.foundation/schema/term_CF_3_rhs
  • forAll: https://uor.foundation/schema/term_CF_3_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Successor curvature flux: trailing_ones(x) for most x, n−1 at maximum.
CF_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CF_4_lhs
  • rhs: https://uor.foundation/schema/term_CF_4_rhs
  • forAll: https://uor.foundation/schema/term_CF_4_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Total successor curvature flux over R_n equals 2^n − 2.
HG_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HG_1_lhs
  • rhs: https://uor.foundation/schema/term_HG_1_rhs
  • forAll: https://uor.foundation/schema/term_HG_1_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Additive holonomy is trivial (abelian group).
HG_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HG_2_lhs
  • rhs: https://uor.foundation/schema/term_HG_2_rhs
  • forAll: https://uor.foundation/schema/term_HG_2_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Dihedral generator holonomy group is D_{2^n}.
HG_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HG_3_lhs
  • rhs: https://uor.foundation/schema/term_HG_3_rhs
  • forAll: https://uor.foundation/schema/term_HG_3_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Unit multiplication holonomy equals the unit group.
HG_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HG_4_lhs
  • rhs: https://uor.foundation/schema/term_HG_4_rhs
  • forAll: https://uor.foundation/schema/term_HG_4_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Full holonomy group is the affine group.
HG_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HG_5_lhs
  • rhs: https://uor.foundation/schema/term_HG_5_rhs
  • forAll: https://uor.foundation/schema/term_HG_5_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Holonomy group decomposition into dihedral and non-trivial units.
T_C1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_T_C1_lhs
  • rhs: https://uor.foundation/schema/term_T_C1_rhs
  • forAll: https://uor.foundation/schema/term_T_C1_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Category left identity: compose(id, f) = f.
T_C2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_T_C2_lhs
  • rhs: https://uor.foundation/schema/term_T_C2_rhs
  • forAll: https://uor.foundation/schema/term_T_C2_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Category right identity: compose(f, id) = f.
T_C3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_T_C3_lhs
  • rhs: https://uor.foundation/schema/term_T_C3_rhs
  • forAll: https://uor.foundation/schema/term_T_C3_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Category associativity of transform composition.
T_C4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_T_C4_lhs
  • rhs: https://uor.foundation/schema/term_T_C4_rhs
  • forAll: https://uor.foundation/schema/term_T_C4_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Composability condition: f composesWith g iff target(f) = source(g).
T_I1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_T_I1_lhs
  • rhs: https://uor.foundation/schema/term_T_I1_rhs
  • forAll: https://uor.foundation/schema/term_T_I1_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Negation is a ring-metric isometry.
T_I2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_T_I2_lhs
  • rhs: https://uor.foundation/schema/term_T_I2_rhs
  • forAll: https://uor.foundation/schema/term_T_I2_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Bitwise complement is a Hamming-metric isometry.
T_I3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_T_I3_lhs
  • rhs: https://uor.foundation/schema/term_T_I3_rhs
  • forAll: https://uor.foundation/schema/term_T_I3_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Successor as composed isometries: succ = neg ∘ bnot preserves d_R but not d_H.
T_I4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_T_I4_lhs
  • rhs: https://uor.foundation/schema/term_T_I4_rhs
  • forAll: https://uor.foundation/schema/term_T_I4_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Ring isometries form a group under composition.
T_I5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_T_I5_lhs
  • rhs: https://uor.foundation/schema/term_T_I5_rhs
  • forAll: https://uor.foundation/schema/term_T_I5_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
CurvatureObservable measures failure of ring isometry to be Hamming isometry.
T_E1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_T_E1_lhs
  • rhs: https://uor.foundation/schema/term_T_E1_rhs
  • forAll: https://uor.foundation/schema/term_T_E1_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Embedding injectivity.
T_E2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_T_E2_lhs
  • rhs: https://uor.foundation/schema/term_T_E2_rhs
  • forAll: https://uor.foundation/schema/term_T_E2_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Embedding is a ring homomorphism.
T_E3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_T_E3_lhs
  • rhs: https://uor.foundation/schema/term_T_E3_rhs
  • forAll: https://uor.foundation/schema/term_T_E3_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Embedding transitivity: composition of embeddings is an embedding.
T_E4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_T_E4_lhs
  • rhs: https://uor.foundation/schema/term_T_E4_rhs
  • forAll: https://uor.foundation/schema/term_T_E4_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Embedding address coherence: glyph ∘ ι ∘ addresses is well-defined.
T_A1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_T_A1_lhs
  • rhs: https://uor.foundation/schema/term_T_A1_rhs
  • forAll: https://uor.foundation/schema/term_T_A1_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Dihedral group acts on constraints by transforming them.
T_A2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_T_A2_lhs
  • rhs: https://uor.foundation/schema/term_T_A2_rhs
  • forAll: https://uor.foundation/schema/term_T_A2_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Dihedral group action on partitions permutes components.
T_A3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_T_A3_lhs
  • rhs: https://uor.foundation/schema/term_T_A3_rhs
  • forAll: https://uor.foundation/schema/term_T_A3_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Dihedral orbits determine irreducibility boundaries.
T_A4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_T_A4_lhs
  • rhs: https://uor.foundation/schema/term_T_A4_rhs
  • forAll: https://uor.foundation/schema/term_T_A4_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Fixed points of negation are {0, 2^{n−1}}; bnot has no fixed points.
AU_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AU_1_lhs
  • rhs: https://uor.foundation/schema/term_AU_1_rhs
  • forAll: https://uor.foundation/schema/term_AU_1_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Automorphism group consists of unit multiplications.
AU_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AU_2_lhs
  • rhs: https://uor.foundation/schema/term_AU_2_rhs
  • forAll: https://uor.foundation/schema/term_AU_2_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Automorphism group is isomorphic to the unit group.
AU_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AU_3_lhs
  • rhs: https://uor.foundation/schema/term_AU_3_rhs
  • forAll: https://uor.foundation/schema/term_AU_3_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Automorphism group order is 2^{n−1}.
AU_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AU_4_lhs
  • rhs: https://uor.foundation/schema/term_AU_4_rhs
  • forAll: https://uor.foundation/schema/term_AU_4_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Intersection of automorphism group with dihedral group is {id, neg}.
AU_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AU_5_lhs
  • rhs: https://uor.foundation/schema/term_AU_5_rhs
  • forAll: https://uor.foundation/schema/term_AU_5_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Affine group is generated by D_{2^n} and μ_3.
EF_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EF_1_lhs
  • rhs: https://uor.foundation/schema/term_EF_1_rhs
  • forAll: https://uor.foundation/schema/term_EF_1_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Embedding functor action on morphisms.
EF_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EF_2_lhs
  • rhs: https://uor.foundation/schema/term_EF_2_rhs
  • forAll: https://uor.foundation/schema/term_EF_2_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Embedding functor preserves composition.
EF_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EF_3_lhs
  • rhs: https://uor.foundation/schema/term_EF_3_rhs
  • forAll: https://uor.foundation/schema/term_EF_3_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Embedding functor preserves identities.
EF_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EF_4_lhs
  • rhs: https://uor.foundation/schema/term_EF_4_rhs
  • forAll: https://uor.foundation/schema/term_EF_4_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Embedding functor composition is functorial.
EF_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EF_5_lhs
  • rhs: https://uor.foundation/schema/term_EF_5_rhs
  • forAll: https://uor.foundation/schema/term_EF_5_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Embedding functor preserves ring isometries.
EF_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EF_6_lhs
  • rhs: https://uor.foundation/schema/term_EF_6_rhs
  • forAll: https://uor.foundation/schema/term_EF_6_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Embedding functor maps dihedral subgroup into target dihedral group.
EF_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EF_7_lhs
  • rhs: https://uor.foundation/schema/term_EF_7_rhs
  • forAll: https://uor.foundation/schema/term_EF_7_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
Embedding functor maps unit group into target unit group.
AA_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AA_1_lhs
  • rhs: https://uor.foundation/schema/term_AA_1_rhs
  • forAll: https://uor.foundation/schema/term_AA_1_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Braille glyph encoding: 6-bit blocks to Braille characters.
AA_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AA_2_lhs
  • rhs: https://uor.foundation/schema/term_AA_2_rhs
  • forAll: https://uor.foundation/schema/term_AA_2_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Braille XOR homomorphism: Braille encoding commutes with XOR.
AA_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AA_3_lhs
  • rhs: https://uor.foundation/schema/term_AA_3_rhs
  • forAll: https://uor.foundation/schema/term_AA_3_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Braille complement: glyph of bnot(x) is character-wise complement of glyph(x).
AA_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AA_4_lhs
  • rhs: https://uor.foundation/schema/term_AA_4_rhs
  • forAll: https://uor.foundation/schema/term_AA_4_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Addition does not lift to address space: no glyph homomorphism for add.
AA_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AA_5_lhs
  • rhs: https://uor.foundation/schema/term_AA_5_rhs
  • forAll: https://uor.foundation/schema/term_AA_5_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Liftable operations are exactly the Boolean operations.
AA_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AA_6_lhs
  • rhs: https://uor.foundation/schema/term_AA_6_rhs
  • forAll: https://uor.foundation/schema/term_AA_6_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Negation decomposes into liftable bnot and non-liftable succ.
AM_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AM_1_lhs
  • rhs: https://uor.foundation/schema/term_AM_1_rhs
  • forAll: https://uor.foundation/schema/term_AM_1_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Address metric is sum of per-character Hamming distances.
AM_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AM_2_lhs
  • rhs: https://uor.foundation/schema/term_AM_2_rhs
  • forAll: https://uor.foundation/schema/term_AM_2_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Address metric equals Hamming metric on ring elements.
AM_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AM_3_lhs
  • rhs: https://uor.foundation/schema/term_AM_3_rhs
  • forAll: https://uor.foundation/schema/term_AM_3_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Address metric does not preserve ring metric in general.
AM_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AM_4_lhs
  • rhs: https://uor.foundation/schema/term_AM_4_rhs
  • forAll: https://uor.foundation/schema/term_AM_4_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Address incompatibility metric.
TH_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TH_1_lhs
  • rhs: https://uor.foundation/schema/term_TH_1_rhs
  • forAll: https://uor.foundation/schema/term_TH_1_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Entropy of a site budget state.
TH_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TH_2_lhs
  • rhs: https://uor.foundation/schema/term_TH_2_rhs
  • forAll: https://uor.foundation/schema/term_TH_2_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Maximum entropy: unconstrained state has S = n × ln 2.
TH_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TH_3_lhs
  • rhs: https://uor.foundation/schema/term_TH_3_rhs
  • forAll: https://uor.foundation/schema/term_TH_3_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Zero entropy: fully resolved state has S = 0.
TH_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TH_4_lhs
  • rhs: https://uor.foundation/schema/term_TH_4_rhs
  • forAll: https://uor.foundation/schema/term_TH_4_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Landauer bound on total resolution cost.
TH_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TH_5_lhs
  • rhs: https://uor.foundation/schema/term_TH_5_rhs
  • forAll: https://uor.foundation/schema/term_TH_5_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Critical inverse temperature for UOR site system.
TH_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TH_6_lhs
  • rhs: https://uor.foundation/schema/term_TH_6_rhs
  • forAll: https://uor.foundation/schema/term_TH_6_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Constraint application removes entropy; convergence rate equals cooling rate.
TH_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TH_7_lhs
  • rhs: https://uor.foundation/schema/term_TH_7_rhs
  • forAll: https://uor.foundation/schema/term_TH_7_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
CatastropheThreshold is the temperature of a partition phase transition.
TH_8https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TH_8_lhs
  • rhs: https://uor.foundation/schema/term_TH_8_rhs
  • forAll: https://uor.foundation/schema/term_TH_8_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Step formula as free-energy cost of a constraint boundary.
TH_9https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TH_9_lhs
  • rhs: https://uor.foundation/schema/term_TH_9_rhs
  • forAll: https://uor.foundation/schema/term_TH_9_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Computational hardness maps to type incompleteness (high temperature).
TH_10https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TH_10_lhs
  • rhs: https://uor.foundation/schema/term_TH_10_rhs
  • forAll: https://uor.foundation/schema/term_TH_10_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Type resolution is measurement; cost ≥ entropy removed.
AR_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AR_1_lhs
  • rhs: https://uor.foundation/schema/term_AR_1_rhs
  • forAll: https://uor.foundation/schema/term_AR_1_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Adiabatic schedule: decreasing freeRank, cost-per-site ordering.
AR_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AR_2_lhs
  • rhs: https://uor.foundation/schema/term_AR_2_rhs
  • forAll: https://uor.foundation/schema/term_AR_2_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Adiabatic cost is sum of constraint costs in optimal order.
AR_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AR_3_lhs
  • rhs: https://uor.foundation/schema/term_AR_3_rhs
  • forAll: https://uor.foundation/schema/term_AR_3_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Adiabatic cost satisfies Landauer bound.
AR_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AR_4_lhs
  • rhs: https://uor.foundation/schema/term_AR_4_rhs
  • forAll: https://uor.foundation/schema/term_AR_4_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Adiabatic efficiency η ≤ 1.
AR_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AR_5_lhs
  • rhs: https://uor.foundation/schema/term_AR_5_rhs
  • forAll: https://uor.foundation/schema/term_AR_5_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Greedy vs adiabatic cost difference: ≤ 5% for n ≤ 16.
PD_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PD_1_lhs
  • rhs: https://uor.foundation/schema/term_PD_1_rhs
  • forAll: https://uor.foundation/schema/term_PD_1_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Phase space definition.
PD_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PD_2_lhs
  • rhs: https://uor.foundation/schema/term_PD_2_rhs
  • forAll: https://uor.foundation/schema/term_PD_2_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Phase boundaries occur where g divides 2^n − 1 or g is a power of 2.
PD_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PD_3_lhs
  • rhs: https://uor.foundation/schema/term_PD_3_rhs
  • forAll: https://uor.foundation/schema/term_PD_3_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Parity boundary divides R_n into equal halves.
PD_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PD_4_lhs
  • rhs: https://uor.foundation/schema/term_PD_4_rhs
  • forAll: https://uor.foundation/schema/term_PD_4_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Resonance lines in the phase diagram.
PD_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PD_5_lhs
  • rhs: https://uor.foundation/schema/term_PD_5_rhs
  • forAll: https://uor.foundation/schema/term_PD_5_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Phase count at level n is at most 2^n (typically O(n)).
RC_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_RC_1_lhs
  • rhs: https://uor.foundation/schema/term_RC_1_rhs
  • forAll: https://uor.foundation/schema/term_RC_1_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Reversible pinning stores prior state in ancilla site.
RC_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_RC_2_lhs
  • rhs: https://uor.foundation/schema/term_RC_2_rhs
  • forAll: https://uor.foundation/schema/term_RC_2_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Reversible pinning has zero total entropy change.
RC_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_RC_3_lhs
  • rhs: https://uor.foundation/schema/term_RC_3_rhs
  • forAll: https://uor.foundation/schema/term_RC_3_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Deferred Landauer cost at ancilla erasure.
RC_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_RC_4_lhs
  • rhs: https://uor.foundation/schema/term_RC_4_rhs
  • forAll: https://uor.foundation/schema/term_RC_4_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Reversible total cost equals irreversible total cost (redistributed).
RC_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_RC_5_lhs
  • rhs: https://uor.foundation/schema/term_RC_5_rhs
  • forAll: https://uor.foundation/schema/term_RC_5_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Quantum UOR: superposed sites, cost proportional to winning path.
DC_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DC_1_lhs
  • rhs: https://uor.foundation/schema/term_DC_1_rhs
  • forAll: https://uor.foundation/schema/term_DC_1_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Ring derivative: ∂_R f(x) = f(succ(x)) - f(x).
DC_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DC_2_lhs
  • rhs: https://uor.foundation/schema/term_DC_2_rhs
  • forAll: https://uor.foundation/schema/term_DC_2_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Hamming derivative: ∂_H f(x) = f(bnot(x)) - f(x).
DC_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DC_3_lhs
  • rhs: https://uor.foundation/schema/term_DC_3_rhs
  • forAll: https://uor.foundation/schema/term_DC_3_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Hamming derivative of identity: ∂_H id(x) = -(2x + 1) mod 2^n.
DC_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DC_4_lhs
  • rhs: https://uor.foundation/schema/term_DC_4_rhs
  • forAll: https://uor.foundation/schema/term_DC_4_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Commutator from derivatives: [neg, bnot](x) = ∂_R neg(x) - ∂_H neg(x).
DC_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DC_5_lhs
  • rhs: https://uor.foundation/schema/term_DC_5_rhs
  • forAll: https://uor.foundation/schema/term_DC_5_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Carry dependence: the difference ∂_R f - ∂_H f decomposes into carry contributions.
DC_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DC_6_lhs
  • rhs: https://uor.foundation/schema/term_DC_6_rhs
  • forAll: https://uor.foundation/schema/term_DC_6_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Jacobian definition: J_k(x) = ∂_R f_k(x) where f_k = site_k.
DC_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DC_7_lhs
  • rhs: https://uor.foundation/schema/term_DC_7_rhs
  • forAll: https://uor.foundation/schema/term_DC_7_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Top-site anomaly: J_{n-1}(x) may differ from lower sites.
DC_8https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DC_8_lhs
  • rhs: https://uor.foundation/schema/term_DC_8_rhs
  • forAll: https://uor.foundation/schema/term_DC_8_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Rank-curvature identity: rank(J(x)) = d_H(x, succ(x)) - 1 for generic x.
DC_9https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DC_9_lhs
  • rhs: https://uor.foundation/schema/term_DC_9_rhs
  • forAll: https://uor.foundation/schema/term_DC_9_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Total curvature from Jacobian: κ(x) = Σ_k J_k(x).
DC_10https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DC_10_lhs
  • rhs: https://uor.foundation/schema/term_DC_10_rhs
  • forAll: https://uor.foundation/schema/term_DC_10_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Curvature-weighted ordering: optimal next constraint maximizes J_k over free sites.
DC_11https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DC_11_lhs
  • rhs: https://uor.foundation/schema/term_DC_11_rhs
  • forAll: https://uor.foundation/schema/term_DC_11_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Curvature equipartition: Σ_{x} J_k(x) ≈ (2^n - 2)/n for each k.
HA_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HA_1_lhs
  • rhs: https://uor.foundation/schema/term_HA_1_rhs
  • forAll: https://uor.foundation/schema/term_HA_1_forAll
  • verificationDomain: https://uor.foundation/op/Topological
Constraint nerve: N(C) is the simplicial complex on constraints.
HA_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HA_2_lhs
  • rhs: https://uor.foundation/schema/term_HA_2_rhs
  • forAll: https://uor.foundation/schema/term_HA_2_forAll
  • verificationDomain: https://uor.foundation/op/Topological
Stall iff non-trivial homology: resolution stalls ⟺ H_k(N(C)) ≠ 0 for some k > 0.
HA_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HA_3_lhs
  • rhs: https://uor.foundation/schema/term_HA_3_rhs
  • forAll: https://uor.foundation/schema/term_HA_3_forAll
  • verificationDomain: https://uor.foundation/op/Topological
Betti-entropy theorem: S_residual ≥ Σ_k β_k × ln 2.
IT_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IT_2_lhs
  • rhs: https://uor.foundation/schema/term_IT_2_rhs
  • forAll: https://uor.foundation/schema/term_IT_2_forAll
  • verificationDomain: https://uor.foundation/op/Topological
Euler-Poincaré formula for constraint nerve.
IT_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IT_3_lhs
  • rhs: https://uor.foundation/schema/term_IT_3_rhs
  • forAll: https://uor.foundation/schema/term_IT_3_forAll
  • verificationDomain: https://uor.foundation/op/Topological
Spectral Euler characteristic.
IT_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IT_6_lhs
  • rhs: https://uor.foundation/schema/term_IT_6_rhs
  • forAll: https://uor.foundation/schema/term_IT_6_forAll
  • verificationDomain: https://uor.foundation/op/Topological
Spectral gap bounds convergence rate from below.
IT_7ahttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IT_7a_lhs
  • rhs: https://uor.foundation/schema/term_IT_7a_rhs
  • forAll: https://uor.foundation/schema/term_IT_7a_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • verificationDomain: https://uor.foundation/op/Analytical
  • verificationDomain: https://uor.foundation/op/Topological
UOR index theorem (topological form): total curvature minus Euler characteristic equals residual entropy in bits.
IT_7bhttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IT_7b_lhs
  • rhs: https://uor.foundation/schema/term_IT_7b_rhs
  • forAll: https://uor.foundation/schema/term_IT_7b_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • verificationDomain: https://uor.foundation/op/Analytical
  • verificationDomain: https://uor.foundation/op/Topological
UOR index theorem (entropy-topology duality).
IT_7chttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IT_7c_lhs
  • rhs: https://uor.foundation/schema/term_IT_7c_rhs
  • forAll: https://uor.foundation/schema/term_IT_7c_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • verificationDomain: https://uor.foundation/op/Analytical
  • verificationDomain: https://uor.foundation/op/Topological
UOR index theorem (spectral cost bound): resolution cost ≥ n - χ(N(C)).
IT_7dhttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IT_7d_lhs
  • rhs: https://uor.foundation/schema/term_IT_7d_rhs
  • forAll: https://uor.foundation/schema/term_IT_7d_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • verificationDomain: https://uor.foundation/op/Analytical
  • verificationDomain: https://uor.foundation/op/Topological
UOR index theorem (completeness criterion): resolution is complete iff χ(N(C)) = n and all Betti numbers vanish.
phi_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_phi_1_lhs
  • rhs: https://uor.foundation/schema/term_phi_1_rhs
  • forAll: https://uor.foundation/schema/term_phi_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Ring → Constraints map: negation transforms a residue constraint.
phi_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_phi_2_lhs
  • rhs: https://uor.foundation/schema/term_phi_2_rhs
  • forAll: https://uor.foundation/schema/term_phi_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Constraints → Sites map: composition maps to union of site pinnings.
phi_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_phi_3_lhs
  • rhs: https://uor.foundation/schema/term_phi_3_rhs
  • forAll: https://uor.foundation/schema/term_phi_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Sites → Partition map: a closed site state determines a unique 4-component partition.
phi_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_phi_4_lhs
  • rhs: https://uor.foundation/schema/term_phi_4_rhs
  • forAll: https://uor.foundation/schema/term_phi_4_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Resolution pipeline: φ₄ = φ₃ ∘ φ₂ ∘ φ₁ is the composite resolution map.
phi_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_phi_5_lhs
  • rhs: https://uor.foundation/schema/term_phi_5_rhs
  • forAll: https://uor.foundation/schema/term_phi_5_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Operations → Observables map: negation preserves d_R, may change d_H.
phi_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_phi_6_lhs
  • rhs: https://uor.foundation/schema/term_phi_6_rhs
  • forAll: https://uor.foundation/schema/term_phi_6_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Observables → Refinement map: observables on a state yield a refinement suggestion.
psi_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_psi_1_lhs
  • rhs: https://uor.foundation/schema/term_psi_1_rhs
  • forAll: https://uor.foundation/schema/term_psi_1_forAll
  • verificationDomain: https://uor.foundation/op/Topological
ψ_1: Constraints → SimplicialComplex (nerve construction). Maps a set of constraints to its nerve simplicial complex.
psi_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_psi_2_lhs
  • rhs: https://uor.foundation/schema/term_psi_2_rhs
  • forAll: https://uor.foundation/schema/term_psi_2_forAll
  • verificationDomain: https://uor.foundation/op/Topological
ψ_2: SimplicialComplex → ChainComplex (chain functor). Maps a simplicial complex to its chain complex.
psi_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_psi_3_lhs
  • rhs: https://uor.foundation/schema/term_psi_3_rhs
  • forAll: https://uor.foundation/schema/term_psi_3_forAll
  • verificationDomain: https://uor.foundation/op/Topological
ψ_3: ChainComplex → HomologyGroups (homology functor). Computes homology groups from a chain complex.
psi_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_psi_5_lhs
  • rhs: https://uor.foundation/schema/term_psi_5_rhs
  • forAll: https://uor.foundation/schema/term_psi_5_forAll
  • verificationDomain: https://uor.foundation/op/Topological
ψ_5: ChainComplex → CochainComplex (dualization functor). Dualizes a chain complex to obtain a cochain complex.
psi_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_psi_6_lhs
  • rhs: https://uor.foundation/schema/term_psi_6_rhs
  • forAll: https://uor.foundation/schema/term_psi_6_forAll
  • verificationDomain: https://uor.foundation/op/Topological
ψ_6: CochainComplex → CohomologyGroups (cohomology functor). Computes cohomology groups from a cochain complex.
D_{2^n}https://uor.foundation/op/DihedralGroup
  • generatedBy: https://uor.foundation/op/neg
  • generatedBy: https://uor.foundation/op/bnot
  • presentation: ⟨r, s | r^{2^n} = s² = e, srs = r⁻¹⟩
The dihedral group of order 2^(n+1), generated by neg (ring reflection) and bnot (hypercube reflection). Every element of this group acts as an isometry on the type space 𝒯_n.
Surface Symmetryhttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_surfaceSymmetry_lhs
  • rhs: https://uor.foundation/schema/term_surfaceSymmetry_rhs
  • forAll: https://uor.foundation/schema/term_surfaceSymmetry_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
The Surface Symmetry Theorem: the composite P∘Π∘G is a well-typed morphism iff G and P share the same state:Frame F. When the shared-frame condition holds, the output lands in the type-equivalent neighbourhood of the source symbol.
CC_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CC_1_lhs
  • rhs: https://uor.foundation/schema/term_CC_1_rhs
  • forAll: https://uor.foundation/schema/term_CC_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Completeness implies O(1) resolution: a CompleteType T satisfies ∀ x ∈ R_n, resolution(x, T) terminates in O(1).
CC_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CC_2_lhs
  • rhs: https://uor.foundation/schema/term_CC_2_rhs
  • forAll: https://uor.foundation/schema/term_CC_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Completeness is monotone: if T ⊆ T' (T' has more constraints), then completeness(T) implies completeness(T').
CC_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CC_3_lhs
  • rhs: https://uor.foundation/schema/term_CC_3_rhs
  • forAll: https://uor.foundation/schema/term_CC_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Witness composition: concat(W₁, W₂) is a valid audit trail iff W₁.sitesClosed + W₂.sitesClosed = n.
CC_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CC_4_lhs
  • rhs: https://uor.foundation/schema/term_CC_4_rhs
  • forAll: https://uor.foundation/schema/term_CC_4_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
The CompletenessResolver is the unique fixed point of the ψ-pipeline applied to a CompletenessCandidate.
CC_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CC_5_lhs
  • rhs: https://uor.foundation/schema/term_CC_5_rhs
  • forAll: https://uor.foundation/schema/term_CC_5_forAll
  • verificationDomain: https://uor.foundation/op/Topological
CompletenessCertificate soundness: cert.verified = true implies χ(N(C)) = n and for all k: β_k = 0.
QL_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_QL_1_lhs
  • rhs: https://uor.foundation/schema/term_QL_1_rhs
  • forAll: https://uor.foundation/schema/term_QL_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
neg(bnot(x)) = succ(x) holds in Z/(2ⁿ)Z for all n ≥ 1. Universal form of the Critical Identity across all quantum levels.
QL_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_QL_2_lhs
  • rhs: https://uor.foundation/schema/term_QL_2_rhs
  • forAll: https://uor.foundation/schema/term_QL_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
The dihedral group D_{2ⁿ} generated by neg and bnot has order 2ⁿ⁺¹ for all n ≥ 1.
QL_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_QL_3_lhs
  • rhs: https://uor.foundation/schema/term_QL_3_rhs
  • forAll: https://uor.foundation/schema/term_QL_3_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
The reduction distribution P(j) = 2^{-j} is the Boltzmann distribution at β* = ln 2 for all n ≥ 1.
QL_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_QL_4_lhs
  • rhs: https://uor.foundation/schema/term_QL_4_rhs
  • forAll: https://uor.foundation/schema/term_QL_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
The site budget of a PrimitiveType at quantum level n is exactly n (one site per bit).
QL_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_QL_5_lhs
  • rhs: https://uor.foundation/schema/term_QL_5_rhs
  • forAll: https://uor.foundation/schema/term_QL_5_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Resolution complexity for a CompleteType is O(1) for all n ≥ 1.
QL_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_QL_6_lhs
  • rhs: https://uor.foundation/schema/term_QL_6_rhs
  • forAll: https://uor.foundation/schema/term_QL_6_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Content addressing is a bijection for all n ≥ 1 (AD_1/AD_2 universality).
QL_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_QL_7_lhs
  • rhs: https://uor.foundation/schema/term_QL_7_rhs
  • forAll: https://uor.foundation/schema/term_QL_7_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
The ψ-pipeline produces a valid ChainComplex for any ConstrainedType at any quantum level n ≥ 1.
GR_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GR_1_lhs
  • rhs: https://uor.foundation/schema/term_GR_1_rhs
  • forAll: https://uor.foundation/schema/term_GR_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Binding monotonicity: freeRank(B_{i+1}) ≤ freeRank(B_i) for all i in a Session.
GR_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GR_2_lhs
  • rhs: https://uor.foundation/schema/term_GR_2_rhs
  • forAll: https://uor.foundation/schema/term_GR_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Binding soundness: a Binding b is sound iff b.datum resolves under b.constraint in O(1).
GR_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GR_3_lhs
  • rhs: https://uor.foundation/schema/term_GR_3_rhs
  • forAll: https://uor.foundation/schema/term_GR_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Session convergence: a Session S converges iff there exists i such that freeRank(B_i) = 0.
GR_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GR_4_lhs
  • rhs: https://uor.foundation/schema/term_GR_4_rhs
  • forAll: https://uor.foundation/schema/term_GR_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Context reset isolation: bindings in C_fresh are independent of bindings in C_prior after a SessionBoundary.
GR_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GR_5_lhs
  • rhs: https://uor.foundation/schema/term_GR_5_rhs
  • forAll: https://uor.foundation/schema/term_GR_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Contradiction detection: ContradictionBoundary fires iff there exist bindings b, b' with the same address, different datum, under the same constraint.
TS_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TS_1_lhs
  • rhs: https://uor.foundation/schema/term_TS_1_rhs
  • forAll: https://uor.foundation/schema/term_TS_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Nerve realisability: for any target (χ*, β₀* = 1, β_k* = 0 for k ≥ 1) with χ* ≤ n, there exists a ConstrainedType T over R_n whose constraint nerve realises the target.
TS_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TS_2_lhs
  • rhs: https://uor.foundation/schema/term_TS_2_rhs
  • forAll: https://uor.foundation/schema/term_TS_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Minimal basis bound: for the IT_7d target (χ* = n, all β* = 0), the MinimalConstraintBasis has size exactly n (one constraint per site position). No redundant constraints exist in the minimal basis.
TS_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TS_3_lhs
  • rhs: https://uor.foundation/schema/term_TS_3_rhs
  • forAll: https://uor.foundation/schema/term_TS_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Synthesis monotonicity: adding a constraint to a synthesis candidate never decreases the Euler characteristic of the resulting nerve (χ is monotone non-decreasing under constraint addition).
TS_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TS_4_lhs
  • rhs: https://uor.foundation/schema/term_TS_4_rhs
  • forAll: https://uor.foundation/schema/term_TS_4_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Synthesis convergence: the TypeSynthesisResolver terminates for any realisable target in at most n constraint additions (for n-site types).
TS_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TS_5_lhs
  • rhs: https://uor.foundation/schema/term_TS_5_rhs
  • forAll: https://uor.foundation/schema/term_TS_5_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Synthesis–certification duality: a SynthesizedType T achieves the IT_7d target if and only if the CompletenessResolver certifies T as a CompleteType. The forward ψ-pipeline and the inverse TypeSynthesisResolver are dual computations.
TS_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TS_6_lhs
  • rhs: https://uor.foundation/schema/term_TS_6_rhs
  • forAll: https://uor.foundation/schema/term_TS_6_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Jacobian-guided synthesis efficiency: using the Jacobian (DC_10) to select the next constraint reduces the expected number of synthesis steps from O(n²) (uninformed) to O(n log n) (Jacobian-guided).
TS_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TS_7_lhs
  • rhs: https://uor.foundation/schema/term_TS_7_rhs
  • forAll: https://uor.foundation/schema/term_TS_7_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Unreachable signatures: a Betti profile with β₀ = 0 is unreachable by any non-empty ConstrainedType — the nerve of a non-empty constraint set is always connected (β₀ ≥ 1).
WLS_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WLS_1_lhs
  • rhs: https://uor.foundation/schema/term_WLS_1_rhs
  • forAll: https://uor.foundation/schema/term_WLS_1_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Lift unobstructedness criterion: WittLift T' is a CompleteType iff the spectral sequence E_r^{p,q} collapses at E_2 (d_2 = 0 and all higher differentials zero).
WLS_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WLS_2_lhs
  • rhs: https://uor.foundation/schema/term_WLS_2_rhs
  • forAll: https://uor.foundation/schema/term_WLS_2_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Obstruction localisation: a non-trivial LiftObstruction is localised to a specific site at bit position n+1. The obstruction class lives in H²(N(C(T))) and is killed by adding one constraint involving the new site.
WLS_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WLS_3_lhs
  • rhs: https://uor.foundation/schema/term_WLS_3_rhs
  • forAll: https://uor.foundation/schema/term_WLS_3_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Monotone lifting for trivially obstructed types: if T is a CompleteType at Q_n and its constraint set is closed under the Q_{n+1} extension map, then T' is a CompleteType at Q_{n+1} with basisSize(T') = basisSize(T) + 1.
WLS_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WLS_4_lhs
  • rhs: https://uor.foundation/schema/term_WLS_4_rhs
  • forAll: https://uor.foundation/schema/term_WLS_4_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Spectral sequence convergence bound: for constraint configurations of homological depth d (H_k(N(C(T))) = 0 for k > d), the spectral sequence converges by page E_{d+2}.
WLS_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WLS_5_lhs
  • rhs: https://uor.foundation/schema/term_WLS_5_rhs
  • forAll: https://uor.foundation/schema/term_WLS_5_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Universal identity preservation: every op:universallyValid identity holds in ℤ/(2^{n+1})ℤ with the lifted constraint set. The lift does not invalidate any certified universal identity.
WLS_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WLS_6_lhs
  • rhs: https://uor.foundation/schema/term_WLS_6_rhs
  • forAll: https://uor.foundation/schema/term_WLS_6_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
ψ-pipeline universality for quantum lifts: the ψ-pipeline produces a valid ChainComplex for any WittLift T' — the chain complex of T' restricts to the chain complex of T on the base nerve, and the extension is well-formed by construction.
MN_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MN_1_lhs
  • rhs: https://uor.foundation/schema/term_MN_1_rhs
  • forAll: https://uor.foundation/schema/term_MN_1_forAll
  • verificationDomain: https://uor.foundation/op/Topological
Holonomy group containment: HolonomyGroup(T) ≤ D_{2^n} for all ConstrainedTypes T over R_n. The holonomy group is always a subgroup of the full dihedral group.
MN_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MN_2_lhs
  • rhs: https://uor.foundation/schema/term_MN_2_rhs
  • forAll: https://uor.foundation/schema/term_MN_2_forAll
  • verificationDomain: https://uor.foundation/op/Topological
Additive flatness (extends OB_H1): if all constraints in T are additive (ResidueConstraint or DepthConstraint type), then HolonomyGroup(T) = {id} — T is a FlatType.
MN_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MN_3_lhs
  • rhs: https://uor.foundation/schema/term_MN_3_rhs
  • forAll: https://uor.foundation/schema/term_MN_3_forAll
  • verificationDomain: https://uor.foundation/op/Topological
Dihedral generation: if T contains both a neg-related and a bnot-related constraint in a common closed path, then HolonomyGroup(T) = D_{2^n} — T has full dihedral holonomy.
MN_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MN_4_lhs
  • rhs: https://uor.foundation/schema/term_MN_4_rhs
  • forAll: https://uor.foundation/schema/term_MN_4_forAll
  • verificationDomain: https://uor.foundation/op/Topological
Holonomy-Betti implication: HolonomyGroup(T) ≠ {id} ⟹ β₁(N(C(T))) ≥ 1. Non-trivial monodromy requires a topological loop. (Converse is false: β₁ ≥ 1 does not imply non-trivial holonomy.)
MN_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MN_5_lhs
  • rhs: https://uor.foundation/schema/term_MN_5_rhs
  • forAll: https://uor.foundation/schema/term_MN_5_forAll
  • verificationDomain: https://uor.foundation/op/Topological
CompleteType holonomy: a CompleteType (IT_7d: χ = n, all β = 0) has trivial holonomy. IT_7d implies FlatType because IT_7d requires β₁ = 0, which by MN_4 implies trivial monodromy.
MN_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MN_6_lhs
  • rhs: https://uor.foundation/schema/term_MN_6_rhs
  • forAll: https://uor.foundation/schema/term_MN_6_forAll
  • verificationDomain: https://uor.foundation/op/Topological
Monodromy composition: if p₁ and p₂ are closed constraint paths, then monodromy(p₁ · p₂) = monodromy(p₁) · monodromy(p₂) in D_{2^n} (group homomorphism from loops to dihedral elements).
MN_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MN_7_lhs
  • rhs: https://uor.foundation/schema/term_MN_7_rhs
  • forAll: https://uor.foundation/schema/term_MN_7_forAll
  • verificationDomain: https://uor.foundation/op/Topological
TwistedType obstruction class: the monodromy of a TwistedType contributes a non-zero class to H²(N(C(T')); ℤ/2ℤ) where T' is any WittLift of T. TwistedTypes always have non-trivial lift obstructions.
PT_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PT_1_lhs
  • rhs: https://uor.foundation/schema/term_PT_1_rhs
  • forAll: https://uor.foundation/schema/term_PT_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Product type site additivity: siteBudget(A × B) = siteBudget(A) + siteBudget(B).
PT_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PT_2_lhs
  • rhs: https://uor.foundation/schema/term_PT_2_rhs
  • forAll: https://uor.foundation/schema/term_PT_2_forAll
  • verificationDomain: https://uor.foundation/op/Topological
Product type partition product: partition(A × B) = partition(A) ⊗ partition(B).
PT_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PT_3_lhs
  • rhs: https://uor.foundation/schema/term_PT_3_rhs
  • forAll: https://uor.foundation/schema/term_PT_3_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
Product type Euler additivity: χ(N(C(A × B))) = χ(N(C(A))) + χ(N(C(B))).
PT_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PT_4_lhs
  • rhs: https://uor.foundation/schema/term_PT_4_rhs
  • forAll: https://uor.foundation/schema/term_PT_4_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Product type entropy additivity: S(A × B) = S(A) + S(B).
ST_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_ST_1_lhs
  • rhs: https://uor.foundation/schema/term_ST_1_rhs
  • forAll: https://uor.foundation/schema/term_ST_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Sum type site budget: siteBudget(A + B) = max(siteBudget(A), siteBudget(B)).
ST_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_ST_2_lhs
  • rhs: https://uor.foundation/schema/term_ST_2_rhs
  • forAll: https://uor.foundation/schema/term_ST_2_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Sum type entropy: S(A + B) = ln 2 + max(S(A), S(B)).
GS_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GS_1_lhs
  • rhs: https://uor.foundation/schema/term_GS_1_rhs
  • forAll: https://uor.foundation/schema/term_GS_1_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Context temperature: T_ctx(C) = freeRank(C) × ln 2 / n.
GS_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GS_2_lhs
  • rhs: https://uor.foundation/schema/term_GS_2_rhs
  • forAll: https://uor.foundation/schema/term_GS_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Grounding degree: σ(C) = (n − freeRank(C)) / n.
GS_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GS_3_lhs
  • rhs: https://uor.foundation/schema/term_GS_3_rhs
  • forAll: https://uor.foundation/schema/term_GS_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Grounding monotonicity: σ(B_{i+1}) ≥ σ(B_i) for all i in a Session.
GS_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GS_4_lhs
  • rhs: https://uor.foundation/schema/term_GS_4_rhs
  • forAll: https://uor.foundation/schema/term_GS_4_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Ground state equivalence: σ(C) = 1 ↔ freeRank(C) = 0 ↔ S(C) = 0 ↔ T_ctx(C) = 0.
GS_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GS_5_lhs
  • rhs: https://uor.foundation/schema/term_GS_5_rhs
  • forAll: https://uor.foundation/schema/term_GS_5_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
O(1) resolution guarantee: freeRank(C) = 0 ∧ q.address ∈ bindings(C) → stepCount(q, C) = 0.
GS_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GS_6_lhs
  • rhs: https://uor.foundation/schema/term_GS_6_rhs
  • forAll: https://uor.foundation/schema/term_GS_6_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Pre-reduction of effective budget: effectiveBudget(q, C) = max(0, siteBudget(q.type) − |pinnedSites(C) ∩ q.siteSet|).
GS_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GS_7_lhs
  • rhs: https://uor.foundation/schema/term_GS_7_rhs
  • forAll: https://uor.foundation/schema/term_GS_7_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Thermodynamic cooling cost: Cost_saturation(C) = n × k_B T × ln 2.
MS_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MS_1_lhs
  • rhs: https://uor.foundation/schema/term_MS_1_rhs
  • forAll: https://uor.foundation/schema/term_MS_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Connectivity lower bound: β₀(N(C)) ≥ 1 for all non-empty C.
MS_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MS_2_lhs
  • rhs: https://uor.foundation/schema/term_MS_2_rhs
  • forAll: https://uor.foundation/schema/term_MS_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Euler capacity ceiling: χ(N(C)) ≤ n for all C at quantum level n.
MS_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MS_3_lhs
  • rhs: https://uor.foundation/schema/term_MS_3_rhs
  • forAll: https://uor.foundation/schema/term_MS_3_forAll
  • verificationDomain: https://uor.foundation/op/Topological
Betti monotonicity under addition: χ(N(C + c)) ≥ χ(N(C)) for any constraint c added to C.
MS_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MS_4_lhs
  • rhs: https://uor.foundation/schema/term_MS_4_rhs
  • forAll: https://uor.foundation/schema/term_MS_4_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Level-relative achievability: a signature achievable at quantum level n remains achievable at level n+1.
MS_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MS_5_lhs
  • rhs: https://uor.foundation/schema/term_MS_5_rhs
  • forAll: https://uor.foundation/schema/term_MS_5_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Empirical completeness convergence: verified SynthesisSignature individuals converge to the exact morphospace boundary.
GD_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GD_1_lhs
  • rhs: https://uor.foundation/schema/term_GD_1_rhs
  • forAll: https://uor.foundation/schema/term_GD_1_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Geodesic condition: a ComputationTrace is a geodesic iff its steps are AR_1-ordered and each step selects the constraint maximising J_k over free sites (DC_10).
GD_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GD_2_lhs
  • rhs: https://uor.foundation/schema/term_GD_2_rhs
  • forAll: https://uor.foundation/schema/term_GD_2_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Geodesic entropy bound: ΔS_step(i) = ln 2 for every step i of a geodesic trace.
GD_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GD_3_lhs
  • rhs: https://uor.foundation/schema/term_GD_3_rhs
  • forAll: https://uor.foundation/schema/term_GD_3_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
Total geodesic cost: Cost_geodesic(T) = freeRank_initial × k_B T ln 2 = TH_4.
GD_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GD_4_lhs
  • rhs: https://uor.foundation/schema/term_GD_4_rhs
  • forAll: https://uor.foundation/schema/term_GD_4_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
Geodesic uniqueness up to step-order equivalence: all geodesics for the same ConstrainedType share stepCount and constraint set.
GD_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GD_5_lhs
  • rhs: https://uor.foundation/schema/term_GD_5_rhs
  • forAll: https://uor.foundation/schema/term_GD_5_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
Subgeodesic detectability: a trace is sub-geodesic iff ∃ step i where J_k(step_i) < max_{free sites} J_k(state_i).
QM_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_QM_1_lhs
  • rhs: https://uor.foundation/schema/term_QM_1_rhs
  • forAll: https://uor.foundation/schema/term_QM_1_forAll
  • verificationDomain: https://uor.foundation/op/QuantumThermodynamic
Von Neumann–Landauer bridge: S_vonNeumann(ψ) = Cost_Landauer(collapse(ψ)).
QM_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_QM_2_lhs
  • rhs: https://uor.foundation/schema/term_QM_2_rhs
  • forAll: https://uor.foundation/schema/term_QM_2_forAll
  • verificationDomain: https://uor.foundation/op/Topological
Measurement as site topology change: projective collapse on a SuperposedSiteState is topologically equivalent to applying a ResidueConstraint that pins the collapsed site.
QM_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_QM_3_lhs
  • rhs: https://uor.foundation/schema/term_QM_3_rhs
  • forAll: https://uor.foundation/schema/term_QM_3_forAll
  • verificationDomain: https://uor.foundation/op/QuantumThermodynamic
Superposition entropy bound: 0 ≤ S_vN(ψ) ≤ ln 2 for any single-site SuperposedSiteState.
QM_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_QM_4_lhs
  • rhs: https://uor.foundation/schema/term_QM_4_rhs
  • forAll: https://uor.foundation/schema/term_QM_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
Collapse idempotence: collapse(collapse(ψ)) = collapse(ψ). Measurement on an already-collapsed state is a no-op.
QM_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_QM_5_lhs
  • rhs: https://uor.foundation/schema/term_QM_5_rhs
  • forAll: https://uor.foundation/schema/term_QM_5_forAll
  • verificationDomain: https://uor.foundation/op/QuantumThermodynamic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Amplitude normalization (Born rule): the sum of squared amplitudes equals 1 for any well-formed SuperposedSiteState.
RC_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_RC_6_lhs
  • rhs: https://uor.foundation/schema/term_RC_6_rhs
  • forAll: https://uor.foundation/schema/term_RC_6_forAll
  • verificationDomain: https://uor.foundation/op/SuperpositionDomain
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Amplitude renormalization: a SuperposedSiteState can always be normalized to satisfy QM_5.
FPM_8https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FPM_8_lhs
  • rhs: https://uor.foundation/schema/term_FPM_8_rhs
  • forAll: https://uor.foundation/schema/term_FPM_8_forAll
  • verificationDomain: https://uor.foundation/op/Enumerative
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Partition exhaustiveness: the four component cardinalities sum to the ring size.
FPM_9https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FPM_9_lhs
  • rhs: https://uor.foundation/schema/term_FPM_9_rhs
  • forAll: https://uor.foundation/schema/term_FPM_9_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Exterior membership criterion: x is exterior iff x is not in the carrier of T.
MN_8https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MN_8_lhs
  • rhs: https://uor.foundation/schema/term_MN_8_rhs
  • forAll: https://uor.foundation/schema/term_MN_8_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Holonomy classification covering: every ConstrainedType with a computed holonomy group is either flat or twisted, not both.
QL_8https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_QL_8_lhs
  • rhs: https://uor.foundation/schema/term_QL_8_rhs
  • forAll: https://uor.foundation/schema/term_QL_8_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Witt level chain inverse: wittLevelPredecessor is the left inverse of nextWittLevel.
D_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_D_7_lhs
  • rhs: https://uor.foundation/schema/term_D_7_rhs
  • forAll: https://uor.foundation/schema/term_D_7_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Dihedral composition rule: (rᵃ sᵖ)(rᵇ sᵠ) = r^(a + (-1)ᵖ b mod 2ⁿ) s^(p xor q).
SP_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SP_1_lhs
  • rhs: https://uor.foundation/schema/term_SP_1_rhs
  • forAll: https://uor.foundation/schema/term_SP_1_forAll
  • verificationDomain: https://uor.foundation/op/SuperpositionDomain
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Classical embedding: superposition resolution of a classical (non-superposed) datum reduces to classical resolution.
SP_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SP_2_lhs
  • rhs: https://uor.foundation/schema/term_SP_2_rhs
  • forAll: https://uor.foundation/schema/term_SP_2_forAll
  • verificationDomain: https://uor.foundation/op/QuantumThermodynamic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Collapse–resolve commutativity: collapsing then resolving classically equals resolving in superposition then collapsing.
SP_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SP_3_lhs
  • rhs: https://uor.foundation/schema/term_SP_3_rhs
  • forAll: https://uor.foundation/schema/term_SP_3_forAll
  • verificationDomain: https://uor.foundation/op/SuperpositionDomain
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Amplitude preservation: the SuperpositionResolver preserves the normalized amplitude vector during ψ-pipeline traversal.
SP_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SP_4_lhs
  • rhs: https://uor.foundation/schema/term_SP_4_rhs
  • forAll: https://uor.foundation/schema/term_SP_4_forAll
  • verificationDomain: https://uor.foundation/op/QuantumThermodynamic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Born rule outcome probability: the probability of collapsing to site k equals the squared amplitude of that site.
PT_2ahttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PT_2a_lhs
  • rhs: https://uor.foundation/schema/term_PT_2a_rhs
  • forAll: https://uor.foundation/schema/term_PT_2a_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Product type partition tensor: the partition of a product type is the tensor product of the component partitions.
PT_2bhttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PT_2b_lhs
  • rhs: https://uor.foundation/schema/term_PT_2b_rhs
  • forAll: https://uor.foundation/schema/term_PT_2b_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Sum type partition coproduct: the partition of a sum type is the coproduct of the variant partitions.
GD_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GD_6_lhs
  • rhs: https://uor.foundation/schema/term_GD_6_rhs
  • forAll: https://uor.foundation/schema/term_GD_6_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Geodesic predicate decomposition: a trace is geodesic iff it is both AR_1-ordered and DC_10-selected.
WT_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WT_1_lhs
  • rhs: https://uor.foundation/schema/term_WT_1_rhs
  • forAll: https://uor.foundation/schema/term_WT_1_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
LiftChain(Q_j, Q_k) is valid CompleteType tower iff every chainStep WittLift has trivial or resolved LiftObstruction.
WT_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WT_2_lhs
  • rhs: https://uor.foundation/schema/term_WT_2_rhs
  • forAll: https://uor.foundation/schema/term_WT_2_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Obstruction count bound: the number of non-trivial LiftObstructions in a chain is at most the chain length.
WT_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WT_3_lhs
  • rhs: https://uor.foundation/schema/term_WT_3_rhs
  • forAll: https://uor.foundation/schema/term_WT_3_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Resolved basis size formula: the basis size at Q_k equals basisSize(Q_j) + chainLength + obstructionResolutionCost.
WT_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WT_4_lhs
  • rhs: https://uor.foundation/schema/term_WT_4_rhs
  • forAll: https://uor.foundation/schema/term_WT_4_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Flat tower characterization: isFlat(chain) iff obstructionCount = 0 iff HolonomyGroup trivial at every step.
WT_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WT_5_lhs
  • rhs: https://uor.foundation/schema/term_WT_5_rhs
  • forAll: https://uor.foundation/schema/term_WT_5_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
LiftChainCertificate existence: a CompleteType at Q_k satisfies IT_7d with a witness chain.
WT_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WT_6_lhs
  • rhs: https://uor.foundation/schema/term_WT_6_rhs
  • forAll: https://uor.foundation/schema/term_WT_6_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Single-step reduction: QT_3 with chainLength=1 and cost=0 reduces to QLS_3.
WT_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WT_7_lhs
  • rhs: https://uor.foundation/schema/term_WT_7_rhs
  • forAll: https://uor.foundation/schema/term_WT_7_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Flat chain basis size: for flat chains, resolvedBasisSize(Q_k) = basisSize(Q_j) + (k - j).
CC_PINShttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CC_PINS_lhs
  • rhs: https://uor.foundation/schema/term_CC_PINS_rhs
  • forAll: https://uor.foundation/schema/term_CC_PINS_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Carry-constraint site-pinning map: pinsSites(CarryConstraint(p)) equals the set of bit positions where p has a 1 plus the first-zero stopping position.
CC_COST_SITEhttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CC_COST_SITE_lhs
  • rhs: https://uor.foundation/schema/term_CC_COST_SITE_rhs
  • forAll: https://uor.foundation/schema/term_CC_COST_SITE_forAll
  • verificationDomain: https://uor.foundation/op/Enumerative
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Carry-constraint cost-to-site count: the number of sites pinned by a CarryConstraint equals popcount plus one for the stopping position.
jsat_RRhttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_jsat_RR_lhs
  • rhs: https://uor.foundation/schema/term_jsat_RR_rhs
  • forAll: https://uor.foundation/schema/term_jsat_RR_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
CRT joint satisfiability: two ResidueConstraints are jointly satisfiable iff the gcd of their moduli divides the difference of their residues.
jsat_CRhttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_jsat_CR_lhs
  • rhs: https://uor.foundation/schema/term_jsat_CR_rhs
  • forAll: https://uor.foundation/schema/term_jsat_CR_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Carry-residue joint satisfiability: a CarryConstraint and ResidueConstraint are jointly satisfiable iff the carry-pinned sites are compatible with the residue class.
jsat_CChttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_jsat_CC_lhs
  • rhs: https://uor.foundation/schema/term_jsat_CC_rhs
  • forAll: https://uor.foundation/schema/term_jsat_CC_forAll
  • verificationDomain: https://uor.foundation/op/Enumerative
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Carry-carry joint satisfiability: two CarryConstraints are jointly satisfiable iff their bit-patterns have no conflicting positions.
D_8https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_D_8_lhs
  • rhs: https://uor.foundation/schema/term_D_8_rhs
  • forAll: https://uor.foundation/schema/term_D_8_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Dihedral inverse formula: the inverse of r^a s^p in D_(2^n) is r^(-(−1)^p a mod 2^n) s^p.
D_9https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_D_9_lhs
  • rhs: https://uor.foundation/schema/term_D_9_rhs
  • forAll: https://uor.foundation/schema/term_D_9_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Dihedral reflection order: every reflection element r^k s^1 in D_(2^n) has order 2.
EXP_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EXP_1_lhs
  • rhs: https://uor.foundation/schema/term_EXP_1_rhs
  • forAll: https://uor.foundation/schema/term_EXP_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Monotone carrier characterization: a ConstrainedType has an upward-closed carrier iff every ResidueConstraint has residue = modulus - 1 and no CarryConstraint or DepthConstraint appears.
EXP_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EXP_2_lhs
  • rhs: https://uor.foundation/schema/term_EXP_2_rhs
  • forAll: https://uor.foundation/schema/term_EXP_2_forAll
  • verificationDomain: https://uor.foundation/op/Enumerative
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Monotone constraint count: the number of expressible monotone ConstrainedTypes at quantum level Q_n is 2^n, corresponding to the principal filter count.
EXP_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EXP_3_lhs
  • rhs: https://uor.foundation/schema/term_EXP_3_rhs
  • forAll: https://uor.foundation/schema/term_EXP_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
SumType carrier semantics: the carrier of a SumType is the coproduct (disjoint union) of component carriers, not the set-theoretic union.
ST_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_ST_3_lhs
  • rhs: https://uor.foundation/schema/term_ST_3_rhs
  • forAll: https://uor.foundation/schema/term_ST_3_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
SumType Euler characteristic additivity: for a SumType with topologically disjoint component nerves, the Euler characteristic is additive.
ST_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_ST_4_lhs
  • rhs: https://uor.foundation/schema/term_ST_4_rhs
  • forAll: https://uor.foundation/schema/term_ST_4_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
SumType Betti number additivity: for disjoint component nerves, all Betti numbers are additive.
ST_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_ST_5_lhs
  • rhs: https://uor.foundation/schema/term_ST_5_rhs
  • forAll: https://uor.foundation/schema/term_ST_5_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
SumType completeness transfer: a SumType A+B is CompleteType iff both A and B are CompleteType and they have equal quantum levels.
TS_8https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TS_8_lhs
  • rhs: https://uor.foundation/schema/term_TS_8_rhs
  • forAll: https://uor.foundation/schema/term_TS_8_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Betti-1 minimum constraint count: the minimum number of constraints needed to achieve first Betti number beta_1 = k in the constraint nerve is 2k + 1.
TS_9https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TS_9_lhs
  • rhs: https://uor.foundation/schema/term_TS_9_rhs
  • forAll: https://uor.foundation/schema/term_TS_9_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
TypeSynthesisResolver termination: the resolver terminates in at most 2^n steps for any target signature at quantum level Q_n, returning either a ConstrainedType or a ForbiddenSignature certificate.
TS_10https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TS_10_lhs
  • rhs: https://uor.foundation/schema/term_TS_10_rhs
  • forAll: https://uor.foundation/schema/term_TS_10_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
ForbiddenSignature membership criterion: a topological signature is a ForbiddenSignature iff no ConstrainedType with at most n constraints realises it at quantum level Q_n.
WT_8https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WT_8_lhs
  • rhs: https://uor.foundation/schema/term_WT_8_rhs
  • forAll: https://uor.foundation/schema/term_WT_8_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
ObstructionChain length bound: the length of the ObstructionChain from Q_j to Q_k is at most (k-j) times C(basisSize(Q_j), 3).
WT_9https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WT_9_lhs
  • rhs: https://uor.foundation/schema/term_WT_9_rhs
  • forAll: https://uor.foundation/schema/term_WT_9_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
TowerCompletenessResolver termination: the resolver terminates for any finite LiftChain within the QT_8 bound, producing a CompleteType certificate or a bounded ObstructionChain.
COEFF_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_COEFF_1_lhs
  • rhs: https://uor.foundation/schema/term_COEFF_1_rhs
  • forAll: https://uor.foundation/schema/term_COEFF_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Standard coefficient ring: the coefficient ring for all psi-pipeline cohomology computations in uor.foundation is Z/2Z, consistent with MN_7.
GO_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GO_1_lhs
  • rhs: https://uor.foundation/schema/term_GO_1_rhs
  • forAll: https://uor.foundation/schema/term_GO_1_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
GluingObstruction feedback: given a GluingObstruction class in H^1(N(C)), the killing RefinementSuggestion adds a constraint whose pinned sites contain the intersection of the cycle-generating pair.
GR_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GR_6_lhs
  • rhs: https://uor.foundation/schema/term_GR_6_rhs
  • forAll: https://uor.foundation/schema/term_GR_6_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Grounding re-entry free rank: for a session at full grounding, a new query q has freeRank equal to the number of q's site coordinates not already bound.
GR_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GR_7_lhs
  • rhs: https://uor.foundation/schema/term_GR_7_rhs
  • forAll: https://uor.foundation/schema/term_GR_7_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Grounding degree degradation: after re-entry with query q, the grounding degree becomes min(current sigma, 1 - freeRank(q)/n).
QM_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_QM_6_lhs
  • rhs: https://uor.foundation/schema/term_QM_6_rhs
  • forAll: https://uor.foundation/schema/term_QM_6_forAll
  • verificationDomain: https://uor.foundation/op/SuperpositionDomain
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Amplitude index set characterization: the amplitude index set of a SuperposedSiteState over ConstrainedType T at Q_n is the set of monotone pinning trajectories consistent with T's constraints.
CIC_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CIC_1_lhs
  • rhs: https://uor.foundation/schema/term_CIC_1_rhs
  • forAll: https://uor.foundation/schema/term_CIC_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Certificate issuance: every valid Transform admits a TransformCertificate attesting correct source-to-target mapping.
CIC_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CIC_2_lhs
  • rhs: https://uor.foundation/schema/term_CIC_2_rhs
  • forAll: https://uor.foundation/schema/term_CIC_2_forAll
  • verificationDomain: https://uor.foundation/op/Geometric
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Certificate issuance: every metric-preserving Transform admits an IsometryCertificate attesting distance preservation.
CIC_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CIC_3_lhs
  • rhs: https://uor.foundation/schema/term_CIC_3_rhs
  • forAll: https://uor.foundation/schema/term_CIC_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Certificate issuance: every involutive operation f where f(f(x)) = x admits an InvolutionCertificate.
CIC_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CIC_4_lhs
  • rhs: https://uor.foundation/schema/term_CIC_4_rhs
  • forAll: https://uor.foundation/schema/term_CIC_4_forAll
  • verificationDomain: https://uor.foundation/op/Thermodynamic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Certificate issuance: full saturation (σ = 1, freeRank = 0) admits a GroundingCertificate.
CIC_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CIC_5_lhs
  • rhs: https://uor.foundation/schema/term_CIC_5_rhs
  • forAll: https://uor.foundation/schema/term_CIC_5_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Certificate issuance: an AR_1-ordered and DC_10-selected trace admits a GeodesicCertificate.
CIC_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CIC_6_lhs
  • rhs: https://uor.foundation/schema/term_CIC_6_rhs
  • forAll: https://uor.foundation/schema/term_CIC_6_forAll
  • verificationDomain: https://uor.foundation/op/QuantumThermodynamic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Certificate issuance: a MeasurementEvent verifying the von Neumann–Landauer bridge at β* = ln 2 admits a MeasurementCertificate.
CIC_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CIC_7_lhs
  • rhs: https://uor.foundation/schema/term_CIC_7_rhs
  • forAll: https://uor.foundation/schema/term_CIC_7_forAll
  • verificationDomain: https://uor.foundation/op/QuantumThermodynamic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Certificate issuance: a MeasurementEvent verifying P(outcome k) = |α_k|² admits a BornRuleVerification certificate.
GC_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GC_1_lhs
  • rhs: https://uor.foundation/schema/term_GC_1_rhs
  • forAll: https://uor.foundation/schema/term_GC_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Certificate issuance: shared-frame grounding that lands in the type-equivalent neighbourhood admits a GroundingCertificate.
GR_8https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GR_8_lhs
  • rhs: https://uor.foundation/schema/term_GR_8_rhs
  • forAll: https://uor.foundation/schema/term_GR_8_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: false
  • validityKind: https://uor.foundation/op/ParametricLower
  • validKMin: 0
Session composition validity: compose(S_A, S_B) is valid at Q_k iff all pinned-site intersections agree at every tower level Q_0 through Q_k.
GR_9https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GR_9_lhs
  • rhs: https://uor.foundation/schema/term_GR_9_rhs
  • forAll: https://uor.foundation/schema/term_GR_9_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
ContextLease disjointness: two distinct leases on the same SharedContext have non-overlapping site sets.
GR_10https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GR_10_lhs
  • rhs: https://uor.foundation/schema/term_GR_10_rhs
  • forAll: https://uor.foundation/schema/term_GR_10_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
ExecutionPolicy confluence: different execution policies on the same pending query set produce the same final resolved state (Church-Rosser for session resolution).
MC_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MC_1_lhs
  • rhs: https://uor.foundation/schema/term_MC_1_rhs
  • forAll: https://uor.foundation/schema/term_MC_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Lease partition conserves total budget: the sum of freeRank over all leases equals the SharedContext freeRank.
MC_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MC_2_lhs
  • rhs: https://uor.foundation/schema/term_MC_2_rhs
  • forAll: https://uor.foundation/schema/term_MC_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Per-lease binding monotonicity: within a leased sub-domain, freeRank decreases monotonically (SR_1 restricted to lease).
MC_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MC_3_lhs
  • rhs: https://uor.foundation/schema/term_MC_3_rhs
  • forAll: https://uor.foundation/schema/term_MC_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
General composition freeRank via inclusion-exclusion.
MC_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MC_4_lhs
  • rhs: https://uor.foundation/schema/term_MC_4_rhs
  • forAll: https://uor.foundation/schema/term_MC_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Disjoint-lease composition is additive: the intersection term vanishes when leases are site-disjoint (SR_9).
MC_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MC_5_lhs
  • rhs: https://uor.foundation/schema/term_MC_5_rhs
  • forAll: https://uor.foundation/schema/term_MC_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Policy-invariant final binding set: different execution policies produce identical SiteBinding records.
MC_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MC_6_lhs
  • rhs: https://uor.foundation/schema/term_MC_6_rhs
  • forAll: https://uor.foundation/schema/term_MC_6_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Full lease coverage implies composed saturation: k sessions on disjoint covering leases, each locally converged, produce a GroundedContext via composition.
MC_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MC_7_lhs
  • rhs: https://uor.foundation/schema/term_MC_7_rhs
  • forAll: https://uor.foundation/schema/term_MC_7_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Distributed O(1) resolution: a query against a composed GroundedContext resolves in zero steps.
MC_8https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MC_8_lhs
  • rhs: https://uor.foundation/schema/term_MC_8_rhs
  • forAll: https://uor.foundation/schema/term_MC_8_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Parallelism bound: per-session resolution work is bounded by lease size, not by total site count n.
WC_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WC_1_lhs
  • rhs: https://uor.foundation/schema/term_WC_1_rhs
  • forAll: https://uor.foundation/schema/term_WC_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Witt coordinate identification: the bit coordinates (x_0, …, x_[n−1]) of x ∈ Z/(2ⁿ)Z are exactly its Witt coordinates under the canonical isomorphism W_n(F_2) ≅ Z/(2ⁿ)Z.
WC_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WC_2_lhs
  • rhs: https://uor.foundation/schema/term_WC_2_rhs
  • forAll: https://uor.foundation/schema/term_WC_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Witt sum correction equals carry: the k-th Witt addition polynomial correction term S_k − x_k − y_k (mod 2) is exactly the carry c_k(x,y).
WC_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WC_3_lhs
  • rhs: https://uor.foundation/schema/term_WC_3_rhs
  • forAll: https://uor.foundation/schema/term_WC_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Carry recurrence is the Witt polynomial recurrence: CA_2 implements the ghost equation for S_[k+1] at p=2.
WC_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WC_4_lhs
  • rhs: https://uor.foundation/schema/term_WC_4_rhs
  • forAll: https://uor.foundation/schema/term_WC_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
The δ-correction at level k equals the single-level carry c_[k+1](x,y). Each application of δ divides by 2, consuming one unit of 2-adic valuation.
WC_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WC_5_lhs
  • rhs: https://uor.foundation/schema/term_WC_5_rhs
  • forAll: https://uor.foundation/schema/term_WC_5_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
LiftObstruction is equivalent to δ-nonvanishing: a nontrivial LiftObstruction at Q_[k+1] means δ_k ≠ 0 for some element pair.
WC_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WC_6_lhs
  • rhs: https://uor.foundation/schema/term_WC_6_rhs
  • forAll: https://uor.foundation/schema/term_WC_6_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Metric discrepancy equals Witt defect: d_Δ(x,y) > 0 iff the ghost map correction (carry) is nonzero.
WC_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WC_7_lhs
  • rhs: https://uor.foundation/schema/term_WC_7_rhs
  • forAll: https://uor.foundation/schema/term_WC_7_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
D_1 is the Witt truncation order relation: succ^[2ⁿ](x) = x is the group relation r^[2ⁿ] = 1 in the Witt-Burnside ring of D_[2∞].
WC_8https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WC_8_lhs
  • rhs: https://uor.foundation/schema/term_WC_8_rhs
  • forAll: https://uor.foundation/schema/term_WC_8_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
D_3 is the Witt-Burnside conjugation relation: neg(succ(neg(x))) = pred(x) is srs = r⁻¹ in the pro-dihedral group.
WC_9https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WC_9_lhs
  • rhs: https://uor.foundation/schema/term_WC_9_rhs
  • forAll: https://uor.foundation/schema/term_WC_9_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
D_4 is a Witt-Burnside reflection composition: bnot(neg(x)) = pred(x) is the product of two reflections yielding inverse rotation.
WC_10https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WC_10_lhs
  • rhs: https://uor.foundation/schema/term_WC_10_rhs
  • forAll: https://uor.foundation/schema/term_WC_10_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
The δ-ring Frobenius lift on W_n(F_2) is the identity map because F_2 is a perfect field of characteristic 2 (a² = a for a ∈ F_2).
WC_11https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WC_11_lhs
  • rhs: https://uor.foundation/schema/term_WC_11_rhs
  • forAll: https://uor.foundation/schema/term_WC_11_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
The Verschiebung on W_n(F_2) is multiplication by 2: V(x) = 2x = add(x,x). This is a coordinate shift with zero Witt defect.
WC_12https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_WC_12_lhs
  • rhs: https://uor.foundation/schema/term_WC_12_rhs
  • forAll: https://uor.foundation/schema/term_WC_12_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
The δ-operator on W_n(F_2) is the squaring defect divided by 2: δ(x) = (x − mul(x,x)) / 2. Expressible entirely in existing op/ primitives (sub, mul, arithmetic right shift).
OA_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OA_1_lhs
  • rhs: https://uor.foundation/schema/term_OA_1_rhs
  • forAll: https://uor.foundation/schema/term_OA_1_forAll
  • verificationDomain: https://uor.foundation/op/ArithmeticValuation
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Ostrowski product formula at p=2: |2|_2 · |2|_∞ = 1. The 2-adic and Archimedean absolute values of 2 are multiplicative inverses.
OA_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OA_2_lhs
  • rhs: https://uor.foundation/schema/term_OA_2_rhs
  • forAll: https://uor.foundation/schema/term_OA_2_forAll
  • verificationDomain: https://uor.foundation/op/ArithmeticValuation
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Crossing cost equals ln 2: the Archimedean image of one unit of 2-adic valuation, under the product formula, is ln 2 nats.
OA_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OA_3_lhs
  • rhs: https://uor.foundation/schema/term_OA_3_rhs
  • forAll: https://uor.foundation/schema/term_OA_3_forAll
  • verificationDomain: https://uor.foundation/op/ArithmeticValuation
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
QM_1 grounding: the Landauer cost β* = ln 2 is the crossing cost from OA_2, derived from the prime p=2 that structures the Witt tower.
OA_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OA_4_lhs
  • rhs: https://uor.foundation/schema/term_OA_4_rhs
  • forAll: https://uor.foundation/schema/term_OA_4_forAll
  • verificationDomain: https://uor.foundation/op/ArithmeticValuation
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Born rule bridge (conditional on amplitude rationality): P(outcome k) = |α_k|_∞², where |·|_∞ is the Archimedean image of the 2-adic amplitude via the product formula.
OA_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OA_5_lhs
  • rhs: https://uor.foundation/schema/term_OA_5_rhs
  • forAll: https://uor.foundation/schema/term_OA_5_forAll
  • verificationDomain: https://uor.foundation/op/ArithmeticValuation
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Entropy per δ-level equals the crossing cost: each application of the δ-operator (division by 2) costs ln 2 nats in the Archimedean completion, which is the per-bit Landauer cost.
HT_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HT_1_lhs
  • rhs: https://uor.foundation/schema/term_HT_1_rhs
  • forAll: https://uor.foundation/schema/term_HT_1_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
KanComplex(N(C)) — the constraint nerve satisfies the Kan extension condition for all horns of dimension ≤ d where d is the maximum simplex dimension of N(C).
HT_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HT_2_lhs
  • rhs: https://uor.foundation/schema/term_HT_2_rhs
  • forAll: https://uor.foundation/schema/term_HT_2_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Path components of nerve recover β₀: π₀(N(C)) ≅ Z^{β₀} counts the connected components of the constraint configuration.
HT_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HT_3_lhs
  • rhs: https://uor.foundation/schema/term_HT_3_rhs
  • forAll: https://uor.foundation/schema/term_HT_3_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
MN_6 monodromy is abelianisation of full π₁: the fundamental group π₁(N(C)) surjects onto the HolonomyGroup D_{2^n} via abelianisation.
HT_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HT_4_lhs
  • rhs: https://uor.foundation/schema/term_HT_4_rhs
  • forAll: https://uor.foundation/schema/term_HT_4_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Higher homotopy groups vanish above nerve dimension: π_k(N(C)) = 0 for all k > dim(N(C)), because the nerve is a finite CW-complex.
HT_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HT_5_lhs
  • rhs: https://uor.foundation/schema/term_HT_5_rhs
  • forAll: https://uor.foundation/schema/term_HT_5_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
1-truncation determines flat/twisted classification: τ_{≤1}(N(C)) captures the holonomy action that distinguishes FlatType from TwistedType.
HT_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HT_6_lhs
  • rhs: https://uor.foundation/schema/term_HT_6_rhs
  • forAll: https://uor.foundation/schema/term_HT_6_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Trivial k-invariants beyond depth d imply spectral collapse: if κ_k is trivial for all k > d then the spectral sequence collapses at E_{d+2}.
HT_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HT_7_lhs
  • rhs: https://uor.foundation/schema/term_HT_7_rhs
  • forAll: https://uor.foundation/schema/term_HT_7_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Non-trivial Whitehead product implies lift obstruction: [α, β] ≠ 0 in π_{p+q−1} implies a non-trivial LiftObstruction that Betti numbers alone cannot detect.
HT_8https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HT_8_lhs
  • rhs: https://uor.foundation/schema/term_HT_8_rhs
  • forAll: https://uor.foundation/schema/term_HT_8_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Hurewicz isomorphism for first non-vanishing group: π_k(N(C)) ⊗ Z ≅ H_k(N(C); Z) for the smallest k with π_k ≠ 0, linking homotopy invariants to homology.
psi_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_psi_7_lhs
  • rhs: https://uor.foundation/schema/term_psi_7_rhs
  • forAll: https://uor.foundation/schema/term_psi_7_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
ψ_7: KanComplex → PostnikovTower — compute the Postnikov truncations τ_{≤k} for k = 0, 1, …, dim(N(C)).
psi_8https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_psi_8_lhs
  • rhs: https://uor.foundation/schema/term_psi_8_rhs
  • forAll: https://uor.foundation/schema/term_psi_8_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
ψ_8: PostnikovTower → HomotopyGroups — extract the homotopy groups π_k from each truncation stage.
psi_9https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_psi_9_lhs
  • rhs: https://uor.foundation/schema/term_psi_9_rhs
  • forAll: https://uor.foundation/schema/term_psi_9_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
ψ_9: HomotopyGroups → KInvariants — compute the k-invariants κ_k classifying the Postnikov tower.
HP_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HP_1_lhs
  • rhs: https://uor.foundation/schema/term_HP_1_rhs
  • forAll: https://uor.foundation/schema/term_HP_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Pipeline composition: nerve construction + Kan promotion = ψ_7 ∘ ψ_1.
HP_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HP_2_lhs
  • rhs: https://uor.foundation/schema/term_HP_2_rhs
  • forAll: https://uor.foundation/schema/term_HP_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Homotopy extraction agrees with homology on k-skeleton.
HP_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HP_3_lhs
  • rhs: https://uor.foundation/schema/term_HP_3_rhs
  • forAll: https://uor.foundation/schema/term_HP_3_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
k-invariant computation detects QLS_4 convergence.
HP_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HP_4_lhs
  • rhs: https://uor.foundation/schema/term_HP_4_rhs
  • forAll: https://uor.foundation/schema/term_HP_4_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Complexity bound for homotopy type computation.
MD_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MD_1_lhs
  • rhs: https://uor.foundation/schema/term_MD_1_rhs
  • forAll: https://uor.foundation/schema/term_MD_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Moduli space dimension equals basis size of any contained type.
MD_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MD_2_lhs
  • rhs: https://uor.foundation/schema/term_MD_2_rhs
  • forAll: https://uor.foundation/schema/term_MD_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Zeroth deformation cohomology = automorphism group intersected with dihedral group.
MD_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MD_3_lhs
  • rhs: https://uor.foundation/schema/term_MD_3_rhs
  • forAll: https://uor.foundation/schema/term_MD_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
First deformation cohomology = tangent space to the moduli space at T.
MD_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MD_4_lhs
  • rhs: https://uor.foundation/schema/term_MD_4_rhs
  • forAll: https://uor.foundation/schema/term_MD_4_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Second deformation cohomology = LiftObstruction space.
MD_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MD_5_lhs
  • rhs: https://uor.foundation/schema/term_MD_5_rhs
  • forAll: https://uor.foundation/schema/term_MD_5_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
FlatType stratum has codimension zero in the moduli space.
MD_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MD_6_lhs
  • rhs: https://uor.foundation/schema/term_MD_6_rhs
  • forAll: https://uor.foundation/schema/term_MD_6_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
TwistedType stratum has codimension at least 1.
MD_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MD_7_lhs
  • rhs: https://uor.foundation/schema/term_MD_7_rhs
  • forAll: https://uor.foundation/schema/term_MD_7_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
VersalDeformation existence is guaranteed when the obstruction space H² vanishes.
MD_8https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MD_8_lhs
  • rhs: https://uor.foundation/schema/term_MD_8_rhs
  • forAll: https://uor.foundation/schema/term_MD_8_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
A deformation family preserves completeness iff H²(Def(T_t)) = 0 along the entire path.
MD_9https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MD_9_lhs
  • rhs: https://uor.foundation/schema/term_MD_9_rhs
  • forAll: https://uor.foundation/schema/term_MD_9_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
The site of a ModuliTowerMap at T has dimension 1 when the obstruction is trivial.
MD_10https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MD_10_lhs
  • rhs: https://uor.foundation/schema/term_MD_10_rhs
  • forAll: https://uor.foundation/schema/term_MD_10_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
The site of a ModuliTowerMap at T is empty iff T is a TwistedType at every level.
MR_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MR_1_lhs
  • rhs: https://uor.foundation/schema/term_MR_1_rhs
  • forAll: https://uor.foundation/schema/term_MR_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
ModuliResolver boundary agrees with MorphospaceBoundary.
MR_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MR_2_lhs
  • rhs: https://uor.foundation/schema/term_MR_2_rhs
  • forAll: https://uor.foundation/schema/term_MR_2_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
StratificationRecord covers every CompleteType in exactly one stratum.
MR_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MR_3_lhs
  • rhs: https://uor.foundation/schema/term_MR_3_rhs
  • forAll: https://uor.foundation/schema/term_MR_3_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
ModuliResolver complexity bound.
MR_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MR_4_lhs
  • rhs: https://uor.foundation/schema/term_MR_4_rhs
  • forAll: https://uor.foundation/schema/term_MR_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Achievable signatures correspond to membership in some HolonomyStratum.
CY_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CY_1_lhs
  • rhs: https://uor.foundation/schema/term_CY_1_rhs
  • forAll: https://uor.foundation/schema/term_CY_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Carry generates at site k iff and(x_k, y_k) = 1. Extends CA_1 (addition decomposition) and WC_2 (Witt sum correction).
CY_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CY_2_lhs
  • rhs: https://uor.foundation/schema/term_CY_2_rhs
  • forAll: https://uor.foundation/schema/term_CY_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Carry propagates at site k iff xor(x_k, y_k) = 1 and c_k = 1. Extends CA_2 (carry recurrence) and WC_3 (Witt polynomial recurrence).
CY_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CY_3_lhs
  • rhs: https://uor.foundation/schema/term_CY_3_rhs
  • forAll: https://uor.foundation/schema/term_CY_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Carry kills at site k iff and(x_k, y_k) = 0 and xor(x_k, y_k) = 0. Complement of CY_1 and CY_2.
CY_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CY_4_lhs
  • rhs: https://uor.foundation/schema/term_CY_4_rhs
  • forAll: https://uor.foundation/schema/term_CY_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
d_Δ(x,y) = |carryCount(x+y) − hammingDistance(x,y)|. The metric incompatibility IS the discrepancy between carry count and Hamming distance. Strengthens WC_6.
CY_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CY_5_lhs
  • rhs: https://uor.foundation/schema/term_CY_5_rhs
  • forAll: https://uor.foundation/schema/term_CY_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Optimal encoding theorem: the encoding that minimizes Σ d_Δ over observed pairs is the one where the carry chain’s significance hierarchy matches the domain’s dependency structure.
CY_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CY_6_lhs
  • rhs: https://uor.foundation/schema/term_CY_6_rhs
  • forAll: https://uor.foundation/schema/term_CY_6_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Site ordering theorem: d_Δ is minimized when high-significance sites (upstream in the carry chain) encode the most structurally informative observables.
CY_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CY_7_lhs
  • rhs: https://uor.foundation/schema/term_CY_7_rhs
  • forAll: https://uor.foundation/schema/term_CY_7_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Carry lookahead: the carry chain for n sites is computable in O(log n) using prefix computation on generate/propagate pairs.
BM_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_BM_1_lhs
  • rhs: https://uor.foundation/schema/term_BM_1_rhs
  • forAll: https://uor.foundation/schema/term_BM_1_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
σ(C) = (n − freeRank(C)) / n. The saturation metric is the complement of free site ratio. Derives from SC_2.
BM_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_BM_2_lhs
  • rhs: https://uor.foundation/schema/term_BM_2_rhs
  • forAll: https://uor.foundation/schema/term_BM_2_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
χ = Σ(−1)^k β_k. The Euler characteristic of the constraint nerve. Derives from IT_2.
BM_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_BM_3_lhs
  • rhs: https://uor.foundation/schema/term_BM_3_rhs
  • forAll: https://uor.foundation/schema/term_BM_3_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Index theorem: Σκ_k − χ = S_residual / ln 2. Links all six metrics. Derives from IT_7a.
BM_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_BM_4_lhs
  • rhs: https://uor.foundation/schema/term_BM_4_rhs
  • forAll: https://uor.foundation/schema/term_BM_4_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
J_k = 0 for pinned sites. The Jacobian vanishes on resolved sites.
BM_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_BM_5_lhs
  • rhs: https://uor.foundation/schema/term_BM_5_rhs
  • forAll: https://uor.foundation/schema/term_BM_5_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
d_Δ > 0 iff carry ≠ 0. The metric discrepancy equals the Witt defect. Derives from WC_6.
BM_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_BM_6_lhs
  • rhs: https://uor.foundation/schema/term_BM_6_rhs
  • forAll: https://uor.foundation/schema/term_BM_6_forAll
  • verificationDomain: https://uor.foundation/op/IndexTheoretic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Metric composition tower: d_Δ → {σ, J_k} → β_k → χ → r. Each metric derives from previous ones.
GL_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GL_1_lhs
  • rhs: https://uor.foundation/schema/term_GL_1_rhs
  • forAll: https://uor.foundation/schema/term_GL_1_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
σ = lower adjoint evaluated at current type. The saturation metric is the lower adjoint of the Galois connection. Derives from SC_2.
GL_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GL_2_lhs
  • rhs: https://uor.foundation/schema/term_GL_2_rhs
  • forAll: https://uor.foundation/schema/term_GL_2_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
r = complement of upper adjoint image. The residual freedom is what the type closure does not reach.
GL_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GL_3_lhs
  • rhs: https://uor.foundation/schema/term_GL_3_rhs
  • forAll: https://uor.foundation/schema/term_GL_3_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
CompleteType = fixpoint of Galois connection, σ=1, r=0. Derives from IT_7d.
GL_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_GL_4_lhs
  • rhs: https://uor.foundation/schema/term_GL_4_rhs
  • forAll: https://uor.foundation/schema/term_GL_4_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Type refinement = ascending in type lattice = descending in site freedom. The Galois connection reverses order.
NV_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_NV_1_lhs
  • rhs: https://uor.foundation/schema/term_NV_1_rhs
  • forAll: https://uor.foundation/schema/term_NV_1_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
nerve(C₁ ∪ C₂) = nerve(C₁) ∪ nerve(C₂) for disjoint constraint domains.
NV_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_NV_2_lhs
  • rhs: https://uor.foundation/schema/term_NV_2_rhs
  • forAll: https://uor.foundation/schema/term_NV_2_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Mayer–Vietoris: β_k(C₁ ∪ C₂) computable from parts and intersection.
NV_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_NV_3_lhs
  • rhs: https://uor.foundation/schema/term_NV_3_rhs
  • forAll: https://uor.foundation/schema/term_NV_3_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Single constraint addition: Δβ_k ∈ {−1, 0, +1} per dimension.
NV_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_NV_4_lhs
  • rhs: https://uor.foundation/schema/term_NV_4_rhs
  • forAll: https://uor.foundation/schema/term_NV_4_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Constraint accumulation monotonicity: β_k non-increasing under SR_1. Derives from SR_1.
SD_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SD_1_lhs
  • rhs: https://uor.foundation/schema/term_SD_1_rhs
  • forAll: https://uor.foundation/schema/term_SD_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
ScalarType grounding: quantize(value, range, bits) produces ring element where d_R reflects value proximity.
SD_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SD_2_lhs
  • rhs: https://uor.foundation/schema/term_SD_2_rhs
  • forAll: https://uor.foundation/schema/term_SD_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
SymbolType grounding: argmin_{encoding} Σ d_Δ over observed pairs (CY_5).
SD_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SD_3_lhs
  • rhs: https://uor.foundation/schema/term_SD_3_rhs
  • forAll: https://uor.foundation/schema/term_SD_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
SequenceType = free monoid on element type with backbone constraint.
SD_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SD_4_lhs
  • rhs: https://uor.foundation/schema/term_SD_4_rhs
  • forAll: https://uor.foundation/schema/term_SD_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
TupleType site count = Σ field site counts, site ordering follows CY_6.
SD_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SD_5_lhs
  • rhs: https://uor.foundation/schema/term_SD_5_rhs
  • forAll: https://uor.foundation/schema/term_SD_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
GraphType constraint nerve = graph nerve, β_k equality.
SD_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SD_6_lhs
  • rhs: https://uor.foundation/schema/term_SD_6_rhs
  • forAll: https://uor.foundation/schema/term_SD_6_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
SetType d_Δ invariant under element permutation, D_{2n} symmetry.
SD_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SD_7_lhs
  • rhs: https://uor.foundation/schema/term_SD_7_rhs
  • forAll: https://uor.foundation/schema/term_SD_7_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
TreeType β_1=0, β_0=1 topological constraints.
SD_8https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SD_8_lhs
  • rhs: https://uor.foundation/schema/term_SD_8_rhs
  • forAll: https://uor.foundation/schema/term_SD_8_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
TableType = SequenceType(TupleType(S)), functorial decomposition.
DD_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DD_1_lhs
  • rhs: https://uor.foundation/schema/term_DD_1_rhs
  • forAll: https://uor.foundation/schema/term_DD_1_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Dispatch determinism: same query and same registry always yield the same resolver.
DD_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DD_2_lhs
  • rhs: https://uor.foundation/schema/term_DD_2_rhs
  • forAll: https://uor.foundation/schema/term_DD_2_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Dispatch coverage: every query in the registry domain has a matching resolver.
PI_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PI_1_lhs
  • rhs: https://uor.foundation/schema/term_PI_1_rhs
  • forAll: https://uor.foundation/schema/term_PI_1_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Inference idempotence: ι(ι(s,C),C) = ι(s,C) on GroundedContext.
PI_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PI_2_lhs
  • rhs: https://uor.foundation/schema/term_PI_2_rhs
  • forAll: https://uor.foundation/schema/term_PI_2_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Inference soundness: ι(s,C) resolves to a type consistent with C.
PI_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PI_3_lhs
  • rhs: https://uor.foundation/schema/term_PI_3_rhs
  • forAll: https://uor.foundation/schema/term_PI_3_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Inference composition: ι = P ∘ Π ∘ G (references phi_4).
PI_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PI_4_lhs
  • rhs: https://uor.foundation/schema/term_PI_4_rhs
  • forAll: https://uor.foundation/schema/term_PI_4_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Inference complexity: O(n) worst case, O(1) on CompleteType.
PI_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PI_5_lhs
  • rhs: https://uor.foundation/schema/term_PI_5_rhs
  • forAll: https://uor.foundation/schema/term_PI_5_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Inference coherence: roundTrip(P(Π(G(s)))) = s.
PA_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PA_1_lhs
  • rhs: https://uor.foundation/schema/term_PA_1_rhs
  • forAll: https://uor.foundation/schema/term_PA_1_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Accumulation permutation invariance: accumulating bindings in any order yields the same saturated context (derives from SR_10).
PA_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PA_2_lhs
  • rhs: https://uor.foundation/schema/term_PA_2_rhs
  • forAll: https://uor.foundation/schema/term_PA_2_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Accumulation monotonicity: α(b,C) ⊇ C (the context only grows, never loses bindings). Derives from SR_1.
PA_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PA_3_lhs
  • rhs: https://uor.foundation/schema/term_PA_3_rhs
  • forAll: https://uor.foundation/schema/term_PA_3_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Accumulation soundness: α(b,C) preserves all previously satisfied constraints. Derives from SR_2.
PA_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PA_4_lhs
  • rhs: https://uor.foundation/schema/term_PA_4_rhs
  • forAll: https://uor.foundation/schema/term_PA_4_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Accumulation base preservation: α does not modify previously pinned sites.
PA_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PA_5_lhs
  • rhs: https://uor.foundation/schema/term_PA_5_rhs
  • forAll: https://uor.foundation/schema/term_PA_5_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Accumulation identity: α(∅, C) = C.
PL_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PL_1_lhs
  • rhs: https://uor.foundation/schema/term_PL_1_rhs
  • forAll: https://uor.foundation/schema/term_PL_1_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Lease disjointness: partitioned leases have pairwise disjoint site sets (derives from SR_9).
PL_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PL_2_lhs
  • rhs: https://uor.foundation/schema/term_PL_2_rhs
  • forAll: https://uor.foundation/schema/term_PL_2_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Lease conservation: union of all leases equals the original shared context (derives from MC_1).
PL_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PL_3_lhs
  • rhs: https://uor.foundation/schema/term_PL_3_rhs
  • forAll: https://uor.foundation/schema/term_PL_3_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Lease coverage: every site in the shared context appears in exactly one lease (derives from MC_6).
PK_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PK_1_lhs
  • rhs: https://uor.foundation/schema/term_PK_1_rhs
  • forAll: https://uor.foundation/schema/term_PK_1_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Composition validity: κ(S₁,S₂) is a valid session if S₁,S₂ have disjoint leases (derives from SR_8).
PK_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PK_2_lhs
  • rhs: https://uor.foundation/schema/term_PK_2_rhs
  • forAll: https://uor.foundation/schema/term_PK_2_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Distributed resolution: resolving in κ(S₁,S₂) equals resolving in S₁ or S₂ independently (derives from MC_7).
PP_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PP_1_lhs
  • rhs: https://uor.foundation/schema/term_PP_1_rhs
  • forAll: https://uor.foundation/schema/term_PP_1_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Pipeline unification: κ(λₖ(α*(ι(s,·))),C) = resolve(s,C). The full composed pipeline equals the top-level resolution function.
PE_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PE_1_lhs
  • rhs: https://uor.foundation/schema/term_PE_1_rhs
  • forAll: https://uor.foundation/schema/term_PE_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Stage 0 initializes state vector to 1.
PE_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PE_2_lhs
  • rhs: https://uor.foundation/schema/term_PE_2_rhs
  • forAll: https://uor.foundation/schema/term_PE_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Stage 1 dispatches resolver (δ selects).
PE_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PE_3_lhs
  • rhs: https://uor.foundation/schema/term_PE_3_rhs
  • forAll: https://uor.foundation/schema/term_PE_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Stage 2 produces valid ring address (G grounds).
PE_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PE_4_lhs
  • rhs: https://uor.foundation/schema/term_PE_4_rhs
  • forAll: https://uor.foundation/schema/term_PE_4_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Stage 3 resolves constraints (Π terminates).
PE_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PE_5_lhs
  • rhs: https://uor.foundation/schema/term_PE_5_rhs
  • forAll: https://uor.foundation/schema/term_PE_5_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Stage 4 accumulates without contradiction (α consistent).
PE_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PE_6_lhs
  • rhs: https://uor.foundation/schema/term_PE_6_rhs
  • forAll: https://uor.foundation/schema/term_PE_6_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Stage 5 extracts coherent output (P projects).
PE_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PE_7_lhs
  • rhs: https://uor.foundation/schema/term_PE_7_rhs
  • forAll: https://uor.foundation/schema/term_PE_7_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Full pipeline is the composition PE_6 ∘ … ∘ PE_1.
PM_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PM_1_lhs
  • rhs: https://uor.foundation/schema/term_PM_1_rhs
  • forAll: https://uor.foundation/schema/term_PM_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Phase rotation Ω^k at stage k.
PM_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PM_2_lhs
  • rhs: https://uor.foundation/schema/term_PM_2_rhs
  • forAll: https://uor.foundation/schema/term_PM_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Phase gate checks Ω^k at boundary.
PM_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PM_3_lhs
  • rhs: https://uor.foundation/schema/term_PM_3_rhs
  • forAll: https://uor.foundation/schema/term_PM_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Gate failure triggers complex conjugate rollback.
PM_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PM_4_lhs
  • rhs: https://uor.foundation/schema/term_PM_4_rhs
  • forAll: https://uor.foundation/schema/term_PM_4_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Rollback is involutory: (z̄)̄ = z.
PM_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PM_5_lhs
  • rhs: https://uor.foundation/schema/term_PM_5_rhs
  • forAll: https://uor.foundation/schema/term_PM_5_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Epoch boundary preserves saturation.
PM_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PM_6_lhs
  • rhs: https://uor.foundation/schema/term_PM_6_rhs
  • forAll: https://uor.foundation/schema/term_PM_6_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Service window provides base context.
PM_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PM_7_lhs
  • rhs: https://uor.foundation/schema/term_PM_7_rhs
  • forAll: https://uor.foundation/schema/term_PM_7_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Machine is deterministic given initial state.
ER_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_ER_1_lhs
  • rhs: https://uor.foundation/schema/term_ER_1_rhs
  • forAll: https://uor.foundation/schema/term_ER_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Stage transition requires guard satisfaction.
ER_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_ER_2_lhs
  • rhs: https://uor.foundation/schema/term_ER_2_rhs
  • forAll: https://uor.foundation/schema/term_ER_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Effect application is atomic.
ER_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_ER_3_lhs
  • rhs: https://uor.foundation/schema/term_ER_3_rhs
  • forAll: https://uor.foundation/schema/term_ER_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Guard evaluation is side-effect-free.
ER_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_ER_4_lhs
  • rhs: https://uor.foundation/schema/term_ER_4_rhs
  • forAll: https://uor.foundation/schema/term_ER_4_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Effect composition is order-independent within a stage.
EA_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EA_1_lhs
  • rhs: https://uor.foundation/schema/term_EA_1_rhs
  • forAll: https://uor.foundation/schema/term_EA_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Epoch boundary resets free sites.
EA_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EA_2_lhs
  • rhs: https://uor.foundation/schema/term_EA_2_rhs
  • forAll: https://uor.foundation/schema/term_EA_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Grounding carries across epochs.
EA_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EA_3_lhs
  • rhs: https://uor.foundation/schema/term_EA_3_rhs
  • forAll: https://uor.foundation/schema/term_EA_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Service window bounds context size.
EA_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EA_4_lhs
  • rhs: https://uor.foundation/schema/term_EA_4_rhs
  • forAll: https://uor.foundation/schema/term_EA_4_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Epoch admits one datum or one refinement pass.
OE_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OE_1_lhs
  • rhs: https://uor.foundation/schema/term_OE_1_rhs
  • forAll: https://uor.foundation/schema/term_OE_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Adjacent stages with compatible guards may fuse.
OE_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OE_2_lhs
  • rhs: https://uor.foundation/schema/term_OE_2_rhs
  • forAll: https://uor.foundation/schema/term_OE_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Independent effects commute.
OE_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OE_3_lhs
  • rhs: https://uor.foundation/schema/term_OE_3_rhs
  • forAll: https://uor.foundation/schema/term_OE_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Disjoint leases parallelize.
OE_4ahttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OE_4a_lhs
  • rhs: https://uor.foundation/schema/term_OE_4a_rhs
  • forAll: https://uor.foundation/schema/term_OE_4a_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Stage fusion preserves semantics.
OE_4bhttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OE_4b_lhs
  • rhs: https://uor.foundation/schema/term_OE_4b_rhs
  • forAll: https://uor.foundation/schema/term_OE_4b_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Effect commutation preserves outcome.
OE_4chttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OE_4c_lhs
  • rhs: https://uor.foundation/schema/term_OE_4c_rhs
  • forAll: https://uor.foundation/schema/term_OE_4c_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Lease parallelism preserves coverage.
CS_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CS_1_lhs
  • rhs: https://uor.foundation/schema/term_CS_1_rhs
  • forAll: https://uor.foundation/schema/term_CS_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Each stage has bounded cost.
CS_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CS_2_lhs
  • rhs: https://uor.foundation/schema/term_CS_2_rhs
  • forAll: https://uor.foundation/schema/term_CS_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Pipeline cost = sum of stage costs.
CS_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CS_3_lhs
  • rhs: https://uor.foundation/schema/term_CS_3_rhs
  • forAll: https://uor.foundation/schema/term_CS_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Rollback cost is at most forward cost.
CS_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CS_4_lhs
  • rhs: https://uor.foundation/schema/term_CS_4_rhs
  • forAll: https://uor.foundation/schema/term_CS_4_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Preflight cost is O(1).
CS_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CS_5_lhs
  • rhs: https://uor.foundation/schema/term_CS_5_rhs
  • forAll: https://uor.foundation/schema/term_CS_5_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Total reduction cost bounded by n × stage_max_cost.
CS_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CS_6_lhs
  • rhs: https://uor.foundation/schema/term_CS_6_rhs
  • forAll: https://uor.foundation/schema/term_CS_6_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Budget solvency rejection: a CompileUnit whose declared thermodynamicBudget is strictly less than the Landauer minimum (bitsWidth(Q_k) × ln 2) is rejected at the BudgetSolvencyCheck preflight.
CS_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CS_7_lhs
  • rhs: https://uor.foundation/schema/term_CS_7_rhs
  • forAll: https://uor.foundation/schema/term_CS_7_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Unit address identity: the unitAddress of a CompileUnit is the u:Element computed by hashing the canonical byte serialization of the root term’s transitive closure.
FA_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FA_1_lhs
  • rhs: https://uor.foundation/schema/term_FA_1_rhs
  • forAll: https://uor.foundation/schema/term_FA_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Every pending query eventually reaches a stage gate.
FA_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FA_2_lhs
  • rhs: https://uor.foundation/schema/term_FA_2_rhs
  • forAll: https://uor.foundation/schema/term_FA_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
No starvation under bounded epoch admission.
FA_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FA_3_lhs
  • rhs: https://uor.foundation/schema/term_FA_3_rhs
  • forAll: https://uor.foundation/schema/term_FA_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Fair lease allocation under disjoint composition.
SW_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SW_1_lhs
  • rhs: https://uor.foundation/schema/term_SW_1_rhs
  • forAll: https://uor.foundation/schema/term_SW_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Service window bounds context memory.
SW_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SW_2_lhs
  • rhs: https://uor.foundation/schema/term_SW_2_rhs
  • forAll: https://uor.foundation/schema/term_SW_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Window slide preserves saturation invariant.
SW_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SW_3_lhs
  • rhs: https://uor.foundation/schema/term_SW_3_rhs
  • forAll: https://uor.foundation/schema/term_SW_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Evicted epochs release lease resources.
SW_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SW_4_lhs
  • rhs: https://uor.foundation/schema/term_SW_4_rhs
  • forAll: https://uor.foundation/schema/term_SW_4_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Window size ≥ 1 (non-empty).
LS_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_LS_1_lhs
  • rhs: https://uor.foundation/schema/term_LS_1_rhs
  • forAll: https://uor.foundation/schema/term_LS_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Suspended lease preserves pinned state.
LS_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_LS_2_lhs
  • rhs: https://uor.foundation/schema/term_LS_2_rhs
  • forAll: https://uor.foundation/schema/term_LS_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Lease expiry triggers resource release.
LS_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_LS_3_lhs
  • rhs: https://uor.foundation/schema/term_LS_3_rhs
  • forAll: https://uor.foundation/schema/term_LS_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Checkpoint restore is idempotent.
LS_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_LS_4_lhs
  • rhs: https://uor.foundation/schema/term_LS_4_rhs
  • forAll: https://uor.foundation/schema/term_LS_4_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Active → Suspended → Active round-trip preserves state.
TJ_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TJ_1_lhs
  • rhs: https://uor.foundation/schema/term_TJ_1_rhs
  • forAll: https://uor.foundation/schema/term_TJ_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
AllOrNothing transaction rolls back on any failure.
TJ_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TJ_2_lhs
  • rhs: https://uor.foundation/schema/term_TJ_2_rhs
  • forAll: https://uor.foundation/schema/term_TJ_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
BestEffort transaction commits partial results.
TJ_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_TJ_3_lhs
  • rhs: https://uor.foundation/schema/term_TJ_3_rhs
  • forAll: https://uor.foundation/schema/term_TJ_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Transaction atomicity within a single epoch.
AP_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AP_1_lhs
  • rhs: https://uor.foundation/schema/term_AP_1_rhs
  • forAll: https://uor.foundation/schema/term_AP_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Partial saturation is monotonically non-decreasing across stages.
AP_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AP_2_lhs
  • rhs: https://uor.foundation/schema/term_AP_2_rhs
  • forAll: https://uor.foundation/schema/term_AP_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Approximation quality improves with additional epochs.
AP_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AP_3_lhs
  • rhs: https://uor.foundation/schema/term_AP_3_rhs
  • forAll: https://uor.foundation/schema/term_AP_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Deferred queries are eventually processed or explicitly dropped.
EC_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EC_1_lhs
  • rhs: https://uor.foundation/schema/term_EC_1_rhs
  • forAll: https://uor.foundation/schema/term_EC_1_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Ω⁶ = −1: reduction converges in 6 stages (phase half-turn).
EC_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EC_2_lhs
  • rhs: https://uor.foundation/schema/term_EC_2_rhs
  • forAll: https://uor.foundation/schema/term_EC_2_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Complex conjugate rollback involutory: (z̄)̄ = z.
EC_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EC_3_lhs
  • rhs: https://uor.foundation/schema/term_EC_3_rhs
  • forAll: https://uor.foundation/schema/term_EC_3_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Pairwise convergence: commutator converges to identity.
EC_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EC_4_lhs
  • rhs: https://uor.foundation/schema/term_EC_4_rhs
  • forAll: https://uor.foundation/schema/term_EC_4_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Triple convergence: associator converges to zero.
EC_4ahttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EC_4a_lhs
  • rhs: https://uor.foundation/schema/term_EC_4a_rhs
  • forAll: https://uor.foundation/schema/term_EC_4a_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Associator monotonicity: associator norm non-increasing.
EC_4bhttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EC_4b_lhs
  • rhs: https://uor.foundation/schema/term_EC_4b_rhs
  • forAll: https://uor.foundation/schema/term_EC_4b_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Associator finiteness: reaches 0 in bounded steps.
EC_4chttps://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EC_4c_lhs
  • rhs: https://uor.foundation/schema/term_EC_4c_rhs
  • forAll: https://uor.foundation/schema/term_EC_4c_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Associator vanishing implies associativity on resolved site space.
EC_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_EC_5_lhs
  • rhs: https://uor.foundation/schema/term_EC_5_rhs
  • forAll: https://uor.foundation/schema/term_EC_5_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Adams termination: no convergence level beyond L3_Self.
DA_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DA_1_lhs
  • rhs: https://uor.foundation/schema/term_DA_1_rhs
  • forAll: https://uor.foundation/schema/term_DA_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Cayley-Dickson R→C: adjoin i with i²=−1, conjugation (a+bi)* = a−bi.
DA_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DA_2_lhs
  • rhs: https://uor.foundation/schema/term_DA_2_rhs
  • forAll: https://uor.foundation/schema/term_DA_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Cayley-Dickson C→H: adjoin j with j²=−1, ij=k, ji=−k, k²=−1.
DA_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DA_3_lhs
  • rhs: https://uor.foundation/schema/term_DA_3_rhs
  • forAll: https://uor.foundation/schema/term_DA_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Cayley-Dickson H→O: adjoin l, Fano plane products, associativity fails.
DA_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DA_4_lhs
  • rhs: https://uor.foundation/schema/term_DA_4_rhs
  • forAll: https://uor.foundation/schema/term_DA_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Adams theorem: no normed division algebra of dimension 16 exists.
DA_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DA_5_lhs
  • rhs: https://uor.foundation/schema/term_DA_5_rhs
  • forAll: https://uor.foundation/schema/term_DA_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Convergence level k lives in k-th division algebra: L0 in R, L1 in C, L2 in H, L3 in O.
DA_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DA_6_lhs
  • rhs: https://uor.foundation/schema/term_DA_6_rhs
  • forAll: https://uor.foundation/schema/term_DA_6_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Commutator vanishes iff algebra at that level is commutative.
DA_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DA_7_lhs
  • rhs: https://uor.foundation/schema/term_DA_7_rhs
  • forAll: https://uor.foundation/schema/term_DA_7_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Associator vanishes iff algebra at that level is associative.
IN_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IN_1_lhs
  • rhs: https://uor.foundation/schema/term_IN_1_rhs
  • forAll: https://uor.foundation/schema/term_IN_1_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
d_Δ as interaction cost between entities.
IN_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IN_2_lhs
  • rhs: https://uor.foundation/schema/term_IN_2_rhs
  • forAll: https://uor.foundation/schema/term_IN_2_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Disjoint leases imply commutator = 0.
IN_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IN_3_lhs
  • rhs: https://uor.foundation/schema/term_IN_3_rhs
  • forAll: https://uor.foundation/schema/term_IN_3_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Shared sites imply commutator > 0.
IN_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IN_4_lhs
  • rhs: https://uor.foundation/schema/term_IN_4_rhs
  • forAll: https://uor.foundation/schema/term_IN_4_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
SR_8 implies negotiation converges (commutator decreases monotonically).
IN_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IN_5_lhs
  • rhs: https://uor.foundation/schema/term_IN_5_rhs
  • forAll: https://uor.foundation/schema/term_IN_5_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Convergent negotiation selects U(1) ⊂ SU(2).
IN_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IN_6_lhs
  • rhs: https://uor.foundation/schema/term_IN_6_rhs
  • forAll: https://uor.foundation/schema/term_IN_6_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Outcome space of pairwise negotiation is S².
IN_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IN_7_lhs
  • rhs: https://uor.foundation/schema/term_IN_7_rhs
  • forAll: https://uor.foundation/schema/term_IN_7_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Mutual modeling selects H ⊂ O.
IN_8https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IN_8_lhs
  • rhs: https://uor.foundation/schema/term_IN_8_rhs
  • forAll: https://uor.foundation/schema/term_IN_8_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Interaction nerve β_k bounds coupling complexity at dimension k.
IN_9https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IN_9_lhs
  • rhs: https://uor.foundation/schema/term_IN_9_rhs
  • forAll: https://uor.foundation/schema/term_IN_9_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
β_2(nerve) × max_disagreement bounds associator norm.
AS_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AS_1_lhs
  • rhs: https://uor.foundation/schema/term_AS_1_rhs
  • forAll: https://uor.foundation/schema/term_AS_1_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
δ-ι-κ non-associativity: δ reads registry written by κ.
AS_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AS_2_lhs
  • rhs: https://uor.foundation/schema/term_AS_2_rhs
  • forAll: https://uor.foundation/schema/term_AS_2_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
ι-α-λ non-associativity: λ reads lease state written by α.
AS_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AS_3_lhs
  • rhs: https://uor.foundation/schema/term_AS_3_rhs
  • forAll: https://uor.foundation/schema/term_AS_3_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
λ-κ-δ non-associativity: δ reads state written by κ.
AS_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_AS_4_lhs
  • rhs: https://uor.foundation/schema/term_AS_4_rhs
  • forAll: https://uor.foundation/schema/term_AS_4_forAll
  • verificationDomain: https://uor.foundation/op/ComposedAlgebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Root cause: non-associativity from read-write interleaving through mediating entity.
MO_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MO_1_lhs
  • rhs: https://uor.foundation/schema/term_MO_1_rhs
  • forAll: https://uor.foundation/schema/term_MO_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Unit law: I ⊗ A ≅ A ≅ A ⊗ I.
MO_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MO_2_lhs
  • rhs: https://uor.foundation/schema/term_MO_2_rhs
  • forAll: https://uor.foundation/schema/term_MO_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Associativity: (A⊗B)⊗C ≅ A⊗(B⊗C).
MO_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MO_3_lhs
  • rhs: https://uor.foundation/schema/term_MO_3_rhs
  • forAll: https://uor.foundation/schema/term_MO_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Certificate composition: cert(A⊗B) contains cert(A) and cert(B).
MO_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MO_4_lhs
  • rhs: https://uor.foundation/schema/term_MO_4_rhs
  • forAll: https://uor.foundation/schema/term_MO_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
σ(A⊗B) ≥ max(σ(A), σ(B)): sequential composition does not lose saturation.
MO_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_MO_5_lhs
  • rhs: https://uor.foundation/schema/term_MO_5_rhs
  • forAll: https://uor.foundation/schema/term_MO_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
r(A⊗B) ≤ min(r(A), r(B)): residual can only shrink under sequential composition.
OP_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OP_1_lhs
  • rhs: https://uor.foundation/schema/term_OP_1_rhs
  • forAll: https://uor.foundation/schema/term_OP_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Site additivity: siteCount(F(G)) = F.sites + Σ_i G_i.sites.
OP_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OP_2_lhs
  • rhs: https://uor.foundation/schema/term_OP_2_rhs
  • forAll: https://uor.foundation/schema/term_OP_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Grounding distributivity: grounding(F(G(x))) = F.ground(G.ground(x)).
OP_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OP_3_lhs
  • rhs: https://uor.foundation/schema/term_OP_3_rhs
  • forAll: https://uor.foundation/schema/term_OP_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
d_Δ decomposition: d_Δ(F(G)) decomposes into outer + inner d_Δ.
OP_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OP_4_lhs
  • rhs: https://uor.foundation/schema/term_OP_4_rhs
  • forAll: https://uor.foundation/schema/term_OP_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Table(Tuple(fields)): standard tabular data structure decomposition.
OP_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_OP_5_lhs
  • rhs: https://uor.foundation/schema/term_OP_5_rhs
  • forAll: https://uor.foundation/schema/term_OP_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Tree(leaves): standard hierarchical data structure (AST, XML, JSON).
FX_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FX_1_lhs
  • rhs: https://uor.foundation/schema/term_FX_1_rhs
  • forAll: https://uor.foundation/schema/term_FX_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Pinning decrements free count by exactly 1.
FX_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FX_2_lhs
  • rhs: https://uor.foundation/schema/term_FX_2_rhs
  • forAll: https://uor.foundation/schema/term_FX_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Unbinding increments free count by exactly 1.
FX_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FX_3_lhs
  • rhs: https://uor.foundation/schema/term_FX_3_rhs
  • forAll: https://uor.foundation/schema/term_FX_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Phase effects preserve site budget.
FX_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FX_4_lhs
  • rhs: https://uor.foundation/schema/term_FX_4_rhs
  • forAll: https://uor.foundation/schema/term_FX_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Disjoint effects commute.
FX_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FX_5_lhs
  • rhs: https://uor.foundation/schema/term_FX_5_rhs
  • forAll: https://uor.foundation/schema/term_FX_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Composite free-count delta is additive.
FX_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FX_6_lhs
  • rhs: https://uor.foundation/schema/term_FX_6_rhs
  • forAll: https://uor.foundation/schema/term_FX_6_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Every ReversibleEffect has an inverse (PinningEffect⁻¹ = UnbindingEffect on same site, PhaseEffect⁻¹ = conjugate phase).
FX_7https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FX_7_lhs
  • rhs: https://uor.foundation/schema/term_FX_7_rhs
  • forAll: https://uor.foundation/schema/term_FX_7_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
External effects must match their declared shape.
PR_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PR_1_lhs
  • rhs: https://uor.foundation/schema/term_PR_1_rhs
  • forAll: https://uor.foundation/schema/term_PR_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Every predicate is total: evaluation terminates for all inputs.
PR_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PR_2_lhs
  • rhs: https://uor.foundation/schema/term_PR_2_rhs
  • forAll: https://uor.foundation/schema/term_PR_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Every predicate is pure: evaluation does not modify state.
PR_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PR_3_lhs
  • rhs: https://uor.foundation/schema/term_PR_3_rhs
  • forAll: https://uor.foundation/schema/term_PR_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Exhaustive + mutually exclusive dispatch is deterministic.
PR_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PR_4_lhs
  • rhs: https://uor.foundation/schema/term_PR_4_rhs
  • forAll: https://uor.foundation/schema/term_PR_4_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Match evaluation is deterministic given exhaustive, ordered arms.
PR_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PR_5_lhs
  • rhs: https://uor.foundation/schema/term_PR_5_rhs
  • forAll: https://uor.foundation/schema/term_PR_5_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Stage transition requires typed guard satisfaction.
CG_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CG_1_lhs
  • rhs: https://uor.foundation/schema/term_CG_1_rhs
  • forAll: https://uor.foundation/schema/term_CG_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Entry guard must be satisfied to enter a stage.
CG_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_CG_2_lhs
  • rhs: https://uor.foundation/schema/term_CG_2_rhs
  • forAll: https://uor.foundation/schema/term_CG_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Exit guard must be satisfied, then the stage effect is applied.
DIS_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DIS_1_lhs
  • rhs: https://uor.foundation/schema/term_DIS_1_rhs
  • forAll: https://uor.foundation/schema/term_DIS_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
The root resolver dispatch table is exhaustive and mutually exclusive over all TypeDefinitions.
DIS_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_DIS_2_lhs
  • rhs: https://uor.foundation/schema/term_DIS_2_rhs
  • forAll: https://uor.foundation/schema/term_DIS_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Resolver dispatch is deterministic for every type.
PAR_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PAR_1_lhs
  • rhs: https://uor.foundation/schema/term_PAR_1_rhs
  • forAll: https://uor.foundation/schema/term_PAR_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Disjoint parallel computations commute: A ⊗ B = B ⊗ A when site targets are disjoint.
PAR_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PAR_2_lhs
  • rhs: https://uor.foundation/schema/term_PAR_2_rhs
  • forAll: https://uor.foundation/schema/term_PAR_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Parallel free-count deltas are additive.
PAR_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PAR_3_lhs
  • rhs: https://uor.foundation/schema/term_PAR_3_rhs
  • forAll: https://uor.foundation/schema/term_PAR_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Partitioning is exhaustive: component cardinalities sum to total site budget.
PAR_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PAR_4_lhs
  • rhs: https://uor.foundation/schema/term_PAR_4_rhs
  • forAll: https://uor.foundation/schema/term_PAR_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
All interleavings of disjoint parallel computations yield the same final context.
PAR_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_PAR_5_lhs
  • rhs: https://uor.foundation/schema/term_PAR_5_rhs
  • forAll: https://uor.foundation/schema/term_PAR_5_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Parallel certificate is the conjunction of component certificates plus disjointness.
HO_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HO_1_lhs
  • rhs: https://uor.foundation/schema/term_HO_1_rhs
  • forAll: https://uor.foundation/schema/term_HO_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
A ComputationDatum’s ring value is the content hash of its certificate.
HO_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HO_2_lhs
  • rhs: https://uor.foundation/schema/term_HO_2_rhs
  • forAll: https://uor.foundation/schema/term_HO_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Application preserves certification.
HO_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HO_3_lhs
  • rhs: https://uor.foundation/schema/term_HO_3_rhs
  • forAll: https://uor.foundation/schema/term_HO_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Composition certification requires both components certified and type-compatible.
HO_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_HO_4_lhs
  • rhs: https://uor.foundation/schema/term_HO_4_rhs
  • forAll: https://uor.foundation/schema/term_HO_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Fully saturated partial application equals direct application.
STR_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_STR_1_lhs
  • rhs: https://uor.foundation/schema/term_STR_1_rhs
  • forAll: https://uor.foundation/schema/term_STR_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Every epoch terminates: the reduction within each epoch reaches convergence angle π.
STR_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_STR_2_lhs
  • rhs: https://uor.foundation/schema/term_STR_2_rhs
  • forAll: https://uor.foundation/schema/term_STR_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Grounding preservation across epoch boundaries.
STR_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_STR_3_lhs
  • rhs: https://uor.foundation/schema/term_STR_3_rhs
  • forAll: https://uor.foundation/schema/term_STR_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Every finite prefix computes in finite time.
STR_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_STR_4_lhs
  • rhs: https://uor.foundation/schema/term_STR_4_rhs
  • forAll: https://uor.foundation/schema/term_STR_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
The first epoch starts from the unfold seed context.
STR_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_STR_5_lhs
  • rhs: https://uor.foundation/schema/term_STR_5_rhs
  • forAll: https://uor.foundation/schema/term_STR_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Each subsequent epoch starts from the previous boundary’s continuation context.
STR_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_STR_6_lhs
  • rhs: https://uor.foundation/schema/term_STR_6_rhs
  • forAll: https://uor.foundation/schema/term_STR_6_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Lease expiry at an epoch boundary returns claimed sites to the next epoch’s linear budget.
FLR_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FLR_1_lhs
  • rhs: https://uor.foundation/schema/term_FLR_1_rhs
  • forAll: https://uor.foundation/schema/term_FLR_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Every partial computation produces exactly one of Success or Failure.
FLR_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FLR_2_lhs
  • rhs: https://uor.foundation/schema/term_FLR_2_rhs
  • forAll: https://uor.foundation/schema/term_FLR_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
A total computation always succeeds.
FLR_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FLR_3_lhs
  • rhs: https://uor.foundation/schema/term_FLR_3_rhs
  • forAll: https://uor.foundation/schema/term_FLR_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Sequential failure propagation: if A fails, B is not evaluated.
FLR_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FLR_4_lhs
  • rhs: https://uor.foundation/schema/term_FLR_4_rhs
  • forAll: https://uor.foundation/schema/term_FLR_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Parallel failure independence: one component’s failure does not prevent the other’s success.
FLR_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FLR_5_lhs
  • rhs: https://uor.foundation/schema/term_FLR_5_rhs
  • forAll: https://uor.foundation/schema/term_FLR_5_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Recovery produces a new ComputationResult.
FLR_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_FLR_6_lhs
  • rhs: https://uor.foundation/schema/term_FLR_6_rhs
  • forAll: https://uor.foundation/schema/term_FLR_6_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
The reduction’s existing rollback mechanism is a Recovery whose effect is the conjugate phase rotation.
LN_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_LN_1_lhs
  • rhs: https://uor.foundation/schema/term_LN_1_rhs
  • forAll: https://uor.foundation/schema/term_LN_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
In a linear trace, every site is targeted exactly once. Total effect count equals site budget.
LN_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_LN_2_lhs
  • rhs: https://uor.foundation/schema/term_LN_2_rhs
  • forAll: https://uor.foundation/schema/term_LN_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
After a LinearEffect, the target site is pinned.
LN_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_LN_3_lhs
  • rhs: https://uor.foundation/schema/term_LN_3_rhs
  • forAll: https://uor.foundation/schema/term_LN_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
A consumed LinearSite cannot be targeted again.
LN_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_LN_4_lhs
  • rhs: https://uor.foundation/schema/term_LN_4_rhs
  • forAll: https://uor.foundation/schema/term_LN_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Lease allocation decrements the linear budget by the lease cardinality.
LN_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_LN_5_lhs
  • rhs: https://uor.foundation/schema/term_LN_5_rhs
  • forAll: https://uor.foundation/schema/term_LN_5_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Lease expiry returns claimed sites to the budget.
LN_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_LN_6_lhs
  • rhs: https://uor.foundation/schema/term_LN_6_rhs
  • forAll: https://uor.foundation/schema/term_LN_6_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Every geodesic trace is a linear trace.
SB_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SB_1_lhs
  • rhs: https://uor.foundation/schema/term_SB_1_rhs
  • forAll: https://uor.foundation/schema/term_SB_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Subtyping is constraint superset: more constraints = more specific.
SB_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SB_2_lhs
  • rhs: https://uor.foundation/schema/term_SB_2_rhs
  • forAll: https://uor.foundation/schema/term_SB_2_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Subtype has fewer valid resolutions.
SB_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SB_3_lhs
  • rhs: https://uor.foundation/schema/term_SB_3_rhs
  • forAll: https://uor.foundation/schema/term_SB_3_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
The constraint nerve of the supertype is a sub-complex of the subtype’s nerve.
SB_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SB_4_lhs
  • rhs: https://uor.foundation/schema/term_SB_4_rhs
  • forAll: https://uor.foundation/schema/term_SB_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Covariance preserves inclusion.
SB_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SB_5_lhs
  • rhs: https://uor.foundation/schema/term_SB_5_rhs
  • forAll: https://uor.foundation/schema/term_SB_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Contravariance reverses inclusion.
SB_6https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_SB_6_lhs
  • rhs: https://uor.foundation/schema/term_SB_6_rhs
  • forAll: https://uor.foundation/schema/term_SB_6_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Lattice depth equals site budget.
BR_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_BR_1_lhs
  • rhs: https://uor.foundation/schema/term_BR_1_rhs
  • forAll: https://uor.foundation/schema/term_BR_1_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Every recursive step strictly decreases the descent measure.
BR_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_BR_2_lhs
  • rhs: https://uor.foundation/schema/term_BR_2_rhs
  • forAll: https://uor.foundation/schema/term_BR_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Recursion depth is bounded by the initial measure value.
BR_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_BR_3_lhs
  • rhs: https://uor.foundation/schema/term_BR_3_rhs
  • forAll: https://uor.foundation/schema/term_BR_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Every bounded recursion terminates.
BR_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_BR_4_lhs
  • rhs: https://uor.foundation/schema/term_BR_4_rhs
  • forAll: https://uor.foundation/schema/term_BR_4_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Structural recursion’s measure is the input type’s structural size.
BR_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_BR_5_lhs
  • rhs: https://uor.foundation/schema/term_BR_5_rhs
  • forAll: https://uor.foundation/schema/term_BR_5_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
The base predicate is satisfied exactly when the measure reaches zero.
RG_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_RG_1_lhs
  • rhs: https://uor.foundation/schema/term_RG_1_rhs
  • forAll: https://uor.foundation/schema/term_RG_1_forAll
  • verificationDomain: https://uor.foundation/op/Topological
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
The working set is determined by the constraint nerve and the stage’s site targets.
RG_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_RG_2_lhs
  • rhs: https://uor.foundation/schema/term_RG_2_rhs
  • forAll: https://uor.foundation/schema/term_RG_2_forAll
  • verificationDomain: https://uor.foundation/op/Analytical
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
All addresses within a region are within the region’s diameter under the chosen metric.
RG_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_RG_3_lhs
  • rhs: https://uor.foundation/schema/term_RG_3_rhs
  • forAll: https://uor.foundation/schema/term_RG_3_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Total working set size is bounded by the addressable space at the quantum level.
RG_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_RG_4_lhs
  • rhs: https://uor.foundation/schema/term_RG_4_rhs
  • forAll: https://uor.foundation/schema/term_RG_4_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
The resolver at stage k accesses only addresses within its working set.
IO_1https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IO_1_lhs
  • rhs: https://uor.foundation/schema/term_IO_1_rhs
  • forAll: https://uor.foundation/schema/term_IO_1_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Ingested data conforms to the source’s declared type.
IO_2https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IO_2_lhs
  • rhs: https://uor.foundation/schema/term_IO_2_rhs
  • forAll: https://uor.foundation/schema/term_IO_2_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Emitted data conforms to the sink’s declared type.
IO_3https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IO_3_lhs
  • rhs: https://uor.foundation/schema/term_IO_3_rhs
  • forAll: https://uor.foundation/schema/term_IO_3_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Every ingestion through a source produces a valid ring datum via grounding.
IO_4https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IO_4_lhs
  • rhs: https://uor.foundation/schema/term_IO_4_rhs
  • forAll: https://uor.foundation/schema/term_IO_4_forAll
  • verificationDomain: https://uor.foundation/op/Pipeline
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Every emission through a sink produces a valid surface symbol via projection.
IO_5https://uor.foundation/op/Identity
  • lhs: https://uor.foundation/schema/term_IO_5_lhs
  • rhs: https://uor.foundation/schema/term_IO_5_rhs
  • forAll: https://uor.foundation/schema/term_IO_5_forAll
  • verificationDomain: https://uor.foundation/op/Algebraic
  • universallyValid: true
  • validityKind: https://uor.foundation/op/Universal
Every boundary effect touches at least one site.